##
##  Type Instantiation of the Axiom of Choice with Hypothesis
##
##
##  Source: [Kubota 2018 (new)]
##
##  Copyright (c) 2018 Owl of Minerva Press GmbH. All rights reserved.
##  Written by Ken Kubota (<mail@kenkubota.de>).
##
##  This file is part of the publication of the mathematical logic R0.
##  For more information, visit: <http://doi.org/10.4444/100.10>
##

<< definitions1.r0.txt
<< K8005.r0.txt


##
##  Axiom of Choice
##
##  Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 236]
##

:= AC ((E{{{o,{o,\3{^}}},^}}_{t{^},{o,t{^}}}{^}){{o,{o,{t{^},{o,t{^}}}}}}_[\j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}.((A{{{o,{o,\3{^}}},^}}_{o,t{^}}{^}){{o,{o,{o,t{^}}}}}_[\p{{o,t{^}}}{{o,t{^}}}.((=>{{{o,o},o}}_((E{{{o,{o,\3{^}}},^}}_t{^}{^}){{o,{o,t{^}}}}_[\x{t{^}}{t{^}}.(p{{o,t{^}}}{{o,t{^}}}_x{t{^}}{t{^}}){o}]{{o,t{^}}}){o}){{o,o}}_(p{{o,t{^}}}{{o,t{^}}}_(j{{t{^},{o,t{^}}}}{{t{^},{o,t{^}}}}_p{{o,t{^}}}{{o,t{^}}}){t{^}}){o}){o}]{{o,{o,t{^}}}}){o}]{{o,{t{^},{o,t{^}}}}})


##
##  Quantified Axiom of Choice (without a free type variable)
##
##  Source: [Kubota 2018 (new)]
##

:= QAC ((A{{{o,{o,\3{^}}},^}}_^{^}){{o,{o,^}}}_[\t{^}{^}.AC{o}]{{o,^}})



## .1

%K8005

## use Proof Template A5221 (Sub):  B  -->  B [x/A]
:= $B5221 %0
:= $T5221 o
:= $X5221 x{$T5221}
:= $A5221 QAC
<< A5221.r0t.txt
:= $B5221; := $T5221; := $X5221; := $A5221
%0


## .2

## use Proof Template A5215H (ALL I):  H => ALL x: B  -->  H => B [x/a]
:= $T5215H ^
:= $X5215H t{$T5215H}
:= $A5215H o
:= $H5215H %0
<< A5215H.r0t.txt
:= $T5215H; := $X5215H; := $A5215H; := $H5215H
%0