P. 61 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fliftcnv 6001*	Converse of the relation F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. A , B >. )   &    |- ( ( ph /\ x e. X ) -> A e. R )   &    |- ( ( ph /\ x e. X ) -> B e. S )   =>    |- ( ph -> `' F = ran ( x e. X |-> <. B , A >. ) )
Theorem	fliftfun 6002*	The function F is the unique function defined by F ` A = B, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. A , B >. )   &    |- ( ( ph /\ x e. X ) -> A e. R )   &    |- ( ( ph /\ x e. X ) -> B e. S )   &    |- ( x = y -> A = C )   &    |- ( x = y -> B = D )   =>    |- ( ph -> ( Fun F <-> A. x e. X A. y e. X ( A = C -> B = D ) ) )
Theorem	fliftfund 6003*	The function F is the unique function defined by F ` A = B, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. A , B >. )   &    |- ( ( ph /\ x e. X ) -> A e. R )   &    |- ( ( ph /\ x e. X ) -> B e. S )   &    |- ( x = y -> A = C )   &    |- ( x = y -> B = D )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ A = C ) ) -> B = D )   =>    |- ( ph -> Fun F )
Theorem	fliftfuns 6004*	The function F is the unique function defined by F ` A = B, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. A , B >. )   &    |- ( ( ph /\ x e. X ) -> A e. R )   &    |- ( ( ph /\ x e. X ) -> B e. S )   =>    |- ( ph -> ( Fun F <-> A. y e. X A. z e. X ( [_ y / x ]_ A = [_ z / x ]_ A -> [_ y / x ]_ B = [_ z / x ]_ B ) ) )
Theorem	fliftf 6005*	The domain and range of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. A , B >. )   &    |- ( ( ph /\ x e. X ) -> A e. R )   &    |- ( ( ph /\ x e. X ) -> B e. S )   =>    |- ( ph -> ( Fun F <-> F : ran ( x e. X |-> A ) --> S ) )
Theorem	fliftval 6006*	The value of the function F. (Contributed by Mario Carneiro, 23-Dec-2016.)
|- F = ran ( x e. X |-> <. A , B >. )   &    |- ( ( ph /\ x e. X ) -> A e. R )   &    |- ( ( ph /\ x e. X ) -> B e. S )   &    |- ( x = Y -> A = C )   &    |- ( x = Y -> B = D )   &    |- ( ph -> Fun F )   =>    |- ( ( ph /\ Y e. X ) -> ( F ` C ) = D )
Theorem	isoeq1 6007	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
|- ( H = G -> ( H Isom R , S ( A , B ) <-> G Isom R , S ( A , B ) ) )
Theorem	isoeq2 6008	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
|- ( R = T -> ( H Isom R , S ( A , B ) <-> H Isom T , S ( A , B ) ) )
Theorem	isoeq3 6009	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
|- ( S = T -> ( H Isom R , S ( A , B ) <-> H Isom R , T ( A , B ) ) )
Theorem	isoeq4 6010	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
|- ( A = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( C , B ) ) )
Theorem	isoeq5 6011	Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
|- ( B = C -> ( H Isom R , S ( A , B ) <-> H Isom R , S ( A , C ) ) )
Theorem	nfiso 6012	Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- F/_ x H   &    |- F/_ x R   &    |- F/_ x S   &    |- F/_ x A   &    |- F/_ x B   =>    |- F/ x H Isom R , S ( A , B )
Theorem	isof1o 6013	An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)
|- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
Theorem	isorel 6014	An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
|- ( ( H Isom R , S ( A , B ) /\ ( C e. A /\ D e. A ) ) -> ( C R D <-> ( H ` C ) S ( H ` D ) ) )
Theorem	isoresbr 6015*	A consequence of isomorphism on two relations for a function's restriction. (Contributed by Jim Kingdon, 11-Jan-2019.)
|- ( ( F |` A ) Isom R , S ( A , ( F " A ) ) -> A. x e. A A. y e. A ( x R y -> ( F ` x ) S ( F ` y ) ) )
Theorem	isoid 6016	Identity law for isomorphism. Proposition 6.30(1) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
|- ( _I |` A ) Isom R , R ( A , A )
Theorem	isocnv 6017	Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
|- ( H Isom R , S ( A , B ) -> `' H Isom S , R ( B , A ) )
Theorem	isocnv2 6018	Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014.)
|- ( H Isom R , S ( A , B ) <-> H Isom `' R , `' S ( A , B ) )
Theorem	isores2 6019	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
|- ( H Isom R , S ( A , B ) <-> H Isom R , ( S i^i ( B X. B ) ) ( A , B ) )
Theorem	isores1 6020	An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013.)
|- ( H Isom R , S ( A , B ) <-> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) )
Theorem	isores3 6021	Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014.)
|- ( ( H Isom R , S ( A , B ) /\ K C_ A /\ X = ( H " K ) ) -> ( H |` K ) Isom R , S ( K , X ) )
Theorem	isotr 6022	Composition (transitive) law for isomorphism. Proposition 6.30(3) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( ( H Isom R , S ( A , B ) /\ G Isom S , T ( B , C ) ) -> ( G o. H ) Isom R , T ( A , C ) )
Theorem	iso0 6023	The empty set is an R , S isomorphism from the empty set to the empty set. (Contributed by Steve Rodriguez, 24-Oct-2015.)
|- (/) Isom R , S ( (/) , (/) )
Theorem	isoini 6024	Isomorphisms preserve initial segments. Proposition 6.31(2) of [TakeutiZaring] p. 33. (Contributed by NM, 20-Apr-2004.)
|- ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( H " ( A i^i ( `' R " { D } ) ) ) = ( B i^i ( `' S " { ( H ` D ) } ) ) )
Theorem	isoini2 6025	Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014.)
|- C = ( A i^i ( `' R " { X } ) )   &    |- D = ( B i^i ( `' S " { ( H ` X ) } ) )   =>    |- ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( H |` C ) Isom R , S ( C , D ) )
Theorem	isoselem 6026*	Lemma for isose 6027. (Contributed by Mario Carneiro, 23-Jun-2015.)
|- ( ph -> H Isom R , S ( A , B ) )   &    |- ( ph -> ( H " x ) e. _V )   =>    |- ( ph -> ( R Se A -> S Se B ) )
Theorem	isose 6027	An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015.)
|- ( H Isom R , S ( A , B ) -> ( R Se A <-> S Se B ) )
Theorem	isopolem 6028	Lemma for isopo 6029. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( S Po B -> R Po A ) )
Theorem	isopo 6029	An isomorphism preserves partial ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( R Po A <-> S Po B ) )
Theorem	isosolem 6030	Lemma for isoso 6031. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( S Or B -> R Or A ) )
Theorem	isoso 6031	An isomorphism preserves strict ordering. (Contributed by Stefan O'Rear, 16-Nov-2014.)
|- ( H Isom R , S ( A , B ) -> ( R Or A <-> S Or B ) )
Theorem	f1oiso 6032*	Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34. (Contributed by NM, 30-Apr-2004.)
|- ( ( H : A -1-1-onto-> B /\ S = { <. z , w >. | E. x e. A E. y e. A ( ( z = ( H ` x ) /\ w = ( H ` y ) ) /\ x R y ) } ) -> H Isom R , S ( A , B ) )
Theorem	f1oiso2 6033*	Any one-to-one onto function determines an isomorphism with an induced relation S. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- S = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( `' H ` x ) R ( `' H ` y ) ) }   =>    |- ( H : A -1-1-onto-> B -> H Isom R , S ( A , B ) )
Theorem	fdmrn 6034	A different way to write F is a function. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- ( Fun F <-> F : dom F --> ran F )
Theorem	rinvf1o 6035	Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- Fun F   &    |- `' F = F   &    |- ( F " A ) C_ B   &    |- ( F " B ) C_ A   &    |- A C_ dom F   &    |- B C_ dom F   =>    |- ( F |` A ) : A -1-1-onto-> B
2.6.9  Cantor's Theorem
Theorem	canth 6036	No set A is equinumerous to its power set (Cantor's theorem), i.e., no function can map A onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1553 if you want the form -. E. f f : A -onto-> ~P A.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)
|- A e. _V   =>    |- -. F : A -onto-> ~P A
2.6.10  Restricted iota (description binder)
Syntax	crio 6037	Extend class notation with restricted description binder.
class ( iota_ x e. A ph )
Definition	df-riota 6038	Define restricted description binder. In case there is no unique x such that ( x e. A /\ ph ) holds, it evaluates to the empty set. See also comments for df-iota 5337. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)
|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
Theorem	riotaeqdv 6039*	Formula-building deduction for iota. (Contributed by NM, 15-Sep-2011.)
|- ( ph -> A = B )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ps ) )
Theorem	riotabidv 6040*	Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )
Theorem	riotaeqbidv 6041*	Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.)
|- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. B ch ) )
Theorem	riotaexg 6042*	Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- ( A e. V -> ( iota_ x e. A ps ) e. _V )
Theorem	iotaexel 6043*	Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.)
|- ( ( A e. V /\ A. x ( ph -> x e. A ) ) -> ( iota x ph ) e. _V )
Theorem	riotav 6044	An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011.)
|- ( iota_ x e. _V ph ) = ( iota x ph )
Theorem	riotauni 6045	Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011.)
|- ( E! x e. A ph -> ( iota_ x e. A ph ) = U. { x e. A | ph } )
Theorem	nfriota1 6046*	The abstraction variable in a restricted iota descriptor isn't free. (Contributed by NM, 12-Oct-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x ( iota_ x e. A ph )
Theorem	nfriotadxy 6047*	Deduction version of nfriota 6048. (Contributed by Jim Kingdon, 12-Jan-2019.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x ( iota_ y e. A ps ) )
Theorem	nfriota 6048*	A variable not free in a wff remains so in a restricted iota descriptor. (Contributed by NM, 12-Oct-2011.)
|- F/ x ph   &    |- F/_ x A   =>    |- F/_ x ( iota_ y e. A ph )
Theorem	cbvriotavw 6049*	Change bound variable in a restricted description binder. Version of cbvriotav 6051 with a disjoint variable condition. (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ y e. A ps )
Theorem	cbvriota 6050*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ y e. A ps )
Theorem	cbvriotav 6051*	Change bound variable in a restricted description binder. (Contributed by NM, 18-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ y e. A ps )
Theorem	csbriotag 6052*	Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013.)
|- ( A e. V -> [_ A / x ]_ ( iota_ y e. B ph ) = ( iota_ y e. B [. A / x ]. ph ) )
Theorem	riotacl2 6053	Membership law for "the unique element in A such that ph." (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)
|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )
Theorem	riotacl 6054*	Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)
|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )
Theorem	riotasbc 6055	Substitution law for descriptions. (Contributed by NM, 23-Aug-2011.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( E! x e. A ph -> [. ( iota_ x e. A ph ) / x ]. ph )
Theorem	riotabidva 6056*	Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 2809 analog.) (Contributed by NM, 17-Jan-2012.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = ( iota_ x e. A ch ) )
Theorem	riotabiia 6057	Equivalent wff's yield equal restricted iotas (inference form). (rabbiia 2807 analog.) (Contributed by NM, 16-Jan-2012.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( iota_ x e. A ph ) = ( iota_ x e. A ps )
Theorem	riota1 6058*	Property of restricted iota. Compare iota1 5352. (Contributed by Mario Carneiro, 15-Oct-2016.)
|- ( E! x e. A ph -> ( ( x e. A /\ ph ) <-> ( iota_ x e. A ph ) = x ) )
Theorem	riota1a 6059	Property of iota. (Contributed by NM, 23-Aug-2011.)
|- ( ( x e. A /\ E! x e. A ph ) -> ( ph <-> ( iota x ( x e. A /\ ph ) ) = x ) )
Theorem	riota2df 6060*	A deduction version of riota2f 6061. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/_ x B )   &    |- ( ph -> F/ x ch )   &    |- ( ph -> B e. A )   &    |- ( ( ph /\ x = B ) -> ( ps <-> ch ) )   =>    |- ( ( ph /\ E! x e. A ps ) -> ( ch <-> ( iota_ x e. A ps ) = B ) )
Theorem	riota2f 6061*	This theorem shows a condition that allows us to represent a descriptor with a class expression B. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x B   &    |- F/ x ps   &    |- ( x = B -> ( ph <-> ps ) )   =>    |- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )
Theorem	riota2 6062*	This theorem shows a condition that allows us to represent a descriptor with a class expression B. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
|- ( x = B -> ( ph <-> ps ) )   =>    |- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )
Theorem	riotaeqimp 6063*	If two restricted iota descriptors for an equality are equal, then the terms of the equality are equal. (Contributed by AV, 6-Dec-2020.)
|- I = ( iota_ a e. V X = A )   &    |- J = ( iota_ a e. V Y = A )   &    |- ( ph -> E! a e. V X = A )   &    |- ( ph -> E! a e. V Y = A )   =>    |- ( ( ph /\ I = J ) -> X = Y )
Theorem	riotaprop 6064*	Properties of a restricted definite description operator. Todo (df-riota 6038 update): can some uses of riota2f 6061 be shortened with this? (Contributed by NM, 23-Nov-2013.)
|- F/ x ps   &    |- B = ( iota_ x e. A ph )   &    |- ( x = B -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph -> ( B e. A /\ ps ) )
Theorem	riota5f 6065*	A method for computing restricted iota. (Contributed by NM, 16-Apr-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- ( ph -> F/_ x B )   &    |- ( ph -> B e. A )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> x = B ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = B )
Theorem	riota5 6066*	A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
|- ( ph -> B e. A )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> x = B ) )   =>    |- ( ph -> ( iota_ x e. A ps ) = B )
Theorem	riotass2 6067*	Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011.) (Revised by NM, 22-Mar-2013.)
|- ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ps ) )
Theorem	riotass 6068*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )
Theorem	moriotass 6069*	Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.)
|- ( ( A C_ B /\ E. x e. A ph /\ E* x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )
Theorem	snriota 6070	A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006.)
|- ( E! x e. A ph -> { x e. A | ph } = { ( iota_ x e. A ph ) } )
Theorem	eusvobj2 6071*	Specify the same property in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- B e. _V   =>    |- ( E! x E. y e. A x = B -> ( E. y e. A x = B <-> A. y e. A x = B ) )
Theorem	eusvobj1 6072*	Specify the same object in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)
|- B e. _V   =>    |- ( E! x E. y e. A x = B -> ( iota x E. y e. A x = B ) = ( iota x A. y e. A x = B ) )
Theorem	f1ofveu 6073*	There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006.)
|- ( ( F : A -1-1-onto-> B /\ C e. B ) -> E! x e. A ( F ` x ) = C )
Theorem	f1ocnvfv3 6074*	Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( ( F : A -1-1-onto-> B /\ C e. B ) -> ( `' F ` C ) = ( iota_ x e. A ( F ` x ) = C ) )
Theorem	riotaund 6075*	Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 13-Sep-2018.)
|- ( -. E! x e. A ph -> ( iota_ x e. A ph ) = (/) )
Theorem	acexmidlema 6076*	Lemma for acexmid 6084. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( { (/) } e. A -> ph )
Theorem	acexmidlemb 6077*	Lemma for acexmid 6084. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( (/) e. B -> ph )
Theorem	acexmidlemph 6078*	Lemma for acexmid 6084. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( ph -> A = B )
Theorem	acexmidlemab 6079*	Lemma for acexmid 6084. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) -> -. ph )
Theorem	acexmidlemcase 6080*	Lemma for acexmid 6084. Here we divide the proof into cases (based on the disjunction implicit in an unordered pair, not the sort of case elimination which relies on excluded middle). The cases are (1) the choice function evaluated at A equals { (/) }, (2) the choice function evaluated at B equals (/), and (3) the choice function evaluated at A equals (/) and the choice function evaluated at B equals { (/) }. Because of the way we represent the choice function y, the choice function evaluated at A is ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) and the choice function evaluated at B is ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ). Other than the difference in notation these work just as ( y ` A ) and ( y ` B ) would if y were a function as defined by df-fun 5379. Although it isn't exactly about the division into cases, it is also convenient for this lemma to also include the step that if the choice function evaluated at A equals { (/) }, then { (/) } e. A and likewise for B. (Contributed by Jim Kingdon, 7-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( { (/) } e. A \/ (/) e. B \/ ( ( iota_ v e. A E. u e. y ( A e. u /\ v e. u ) ) = (/) /\ ( iota_ v e. B E. u e. y ( B e. u /\ v e. u ) ) = { (/) } ) ) )
Theorem	acexmidlem1 6081*	Lemma for acexmid 6084. List the cases identified in acexmidlemcase 6080 and hook them up to the lemmas which handle each case. (Contributed by Jim Kingdon, 7-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ph \/ -. ph ) )
Theorem	acexmidlem2 6082*	Lemma for acexmid 6084. This builds on acexmidlem1 6081 by noting that every element of C is inhabited. (Note that y is not quite a function in the df-fun 5379 sense because it uses ordered pairs as described in opthreg 4703 rather than df-op 3718). The set A is also found in onsucelsucexmidlem 4676. (Contributed by Jim Kingdon, 5-Aug-2019.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ ph ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ ph ) }   &    |- C = { A , B }   =>    |- ( A. z e. C A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) -> ( ph \/ -. ph ) )
Theorem	acexmidlemv 6083*	Lemma for acexmid 6084. This is acexmid 6084 with additional disjoint variable conditions, most notably between ph and x. (Contributed by Jim Kingdon, 6-Aug-2019.)
|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )   =>    |- ( ph \/ -. ph )
Theorem	acexmid 6084*	The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483. The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function y provides a value when z is inhabited (as opposed to nonempty as in some statements of the axiom of choice). Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967). For this theorem stated using the df-ac 7562 and df-exmid 4332 syntaxes, see exmidac 7565. (Contributed by Jim Kingdon, 4-Aug-2019.)
|- E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u )   =>    |- ( ph \/ -. ph )
2.6.11  Operations
Syntax	co 6085	Extend class notation to include the value of an operation F (such as + ) for two arguments A and B. Note that the syntax is simply three class symbols in a row surrounded by parentheses. Since operation values are the only possible class expressions consisting of three class expressions in a row surrounded by parentheses, the syntax is unambiguous.
class ( A F B )
Syntax	coprab 6086	Extend class notation to include class abstraction (class builder) of nested ordered pairs.
class { <. <. x , y >. , z >. | ph }
Syntax	cmpo 6087	Extend the definition of a class to include maps-to notation for defining an operation via a rule.
class ( x e. A , y e. B |-> C )
Definition	df-ov 6088	Define the value of an operation. Definition of operation value in [Enderton] p. 79. Note that the syntax is simply three class expressions in a row bracketed by parentheses. There are no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation F and its arguments A and B- will be useful for proving meaningful theorems. For example, if class F is the operation + and arguments A and B are 3 and 2 , the expression ( 3 + 2 ) can be proved to equal 5 . This definition is well-defined, although not very meaningful, when classes A and/or B are proper classes (i.e. are not sets); see ovprc1 6122 and ovprc2 6123. On the other hand, we often find uses for this definition when F is a proper class. F is normally equal to a class of nested ordered pairs of the form defined by df-oprab 6089. (Contributed by NM, 28-Feb-1995.)
|- ( A F B ) = ( F ` <. A , B >. )
Definition	df-oprab 6089*	Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally x, y, and z are distinct, although the definition doesn't strictly require it. See df-ov 6088 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ovmpo 6224. (Contributed by NM, 12-Mar-1995.)
|- { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
Definition	df-mpo 6090*	Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B) to B ( x , y )". An extension of df-mpt 4194 for two arguments. (Contributed by NM, 17-Feb-2008.)
|- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
Theorem	oveq 6091	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( F = G -> ( A F B ) = ( A G B ) )
Theorem	oveq1 6092	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( A F C ) = ( B F C ) )
Theorem	oveq2 6093	Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
|- ( A = B -> ( C F A ) = ( C F B ) )
Theorem	oveq12 6094	Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
|- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
Theorem	oveq1i 6095	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( A F C ) = ( B F C )
Theorem	oveq2i 6096	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
|- A = B   =>    |- ( C F A ) = ( C F B )
Theorem	oveq12i 6097	Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- A = B   &    |- C = D   =>    |- ( A F C ) = ( B F D )
Theorem	oveqi 6098	Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
|- A = B   =>    |- ( C A D ) = ( C B D )
Theorem	oveq123i 6099	Equality inference for operation value. (Contributed by FL, 11-Jul-2010.)
|- A = C   &    |- B = D   &    |- F = G   =>    |- ( A F B ) = ( C G D )
Theorem	oveq1d 6100	Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A F C ) = ( B F C ) )