P. 71 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7001-7100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ctmlemr 7001*	Lemma for ctm 7002. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.)
|- ( E. x x e. A -> ( E. f f : om -onto-> A -> E. f f : om -onto-> ( A ⊔ 1o ) ) )
Theorem	ctm 7002*	Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- ( E. x x e. A -> ( E. f f : om -onto-> ( A ⊔ 1o ) <-> E. f f : om -onto-> A ) )
Theorem	ctssdclemn0 7003*	Lemma for ctssdc 7006. The -. (/) e. S case. (Contributed by Jim Kingdon, 16-Aug-2023.)
|- ( ph -> S C_ om )   &    |- ( ph -> A. n e. om DECID n e. S )   &    |- ( ph -> F : S -onto-> A )   &    |- ( ph -> -. (/) e. S )   =>    |- ( ph -> E. g g : om -onto-> ( A ⊔ 1o ) )
Theorem	ctssdccl 7004*	A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7006 but expressed in terms of classes rather than E.. (Contributed by Jim Kingdon, 30-Oct-2023.)
|- ( ph -> F : om -onto-> ( A ⊔ 1o ) )   &    |- S = { x e. om | ( F ` x ) e. (inl " A ) }   &    |- G = ( `'inl o. F )   =>    |- ( ph -> ( S C_ om /\ G : S -onto-> A /\ A. n e. om DECID n e. S ) )
Theorem	ctssdclemr 7005*	Lemma for ctssdc 7006. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.)
|- ( E. f f : om -onto-> ( A ⊔ 1o ) -> E. s ( s C_ om /\ E. f f : s -onto-> A /\ A. n e. om DECID n e. s ) )
Theorem	ctssdc 7006*	A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 7032. (Contributed by Jim Kingdon, 15-Aug-2023.)
|- ( E. s ( s C_ om /\ E. f f : s -onto-> A /\ A. n e. om DECID n e. s ) <-> E. f f : om -onto-> ( A ⊔ 1o ) )
Theorem	enumctlemm 7007*	Lemma for enumct 7008. The case where N is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- ( ph -> F : N -onto-> A )   &    |- ( ph -> N e. om )   &    |- ( ph -> (/) e. N )   &    |- G = ( k e. om |-> if ( k e. N , ( F ` k ) , ( F ` (/) ) ) )   =>    |- ( ph -> G : om -onto-> A )
Theorem	enumct 7008*	A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as E. n e. om E. f f : n -onto-> A per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as E. g g : om -onto-> ( A ⊔ 1o ) per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.)
|- ( E. n e. om E. f f : n -onto-> A -> E. g g : om -onto-> ( A ⊔ 1o ) )
Theorem	finct 7009*	A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.)
|- ( A e. Fin -> E. g g : om -onto-> ( A ⊔ 1o ) )
Theorem	omct 7010	om is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- E. f f : om -onto-> ( om ⊔ 1o )
Theorem	ctfoex 7011*	A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.)
|- ( E. f f : om -onto-> ( A ⊔ 1o ) -> A e. _V )
2.6.36  Omniscient sets
Syntax	comni 7012	Extend class definition to include the class of omniscient sets.
class Omni
Syntax	xnninf 7013	Set of nonincreasing sequences in 2o ^m om.
class ℕ∞
Definition	df-omni 7014*	An omniscient set is one where we can decide whether a predicate (here represented by a function f) holds (is equal to 1o) for all elements or fails to hold (is equal to (/)) for some element. Definition 3.1 of [Pierik], p. 14. In particular, om e. Omni is known as the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 28-Jun-2022.)
|- Omni = { y | A. f ( f : y --> 2o -> ( E. x e. y ( f ` x ) = (/) \/ A. x e. y ( f ` x ) = 1o ) ) }
Definition	df-nninf 7015*	Define the set of nonincreasing sequences in 2o ^m om. Definition in Section 3.1 of [Pierik], p. 15. If we assumed excluded middle, this would be essentially the same as NN0* as defined at df-xnn0 9065 but in its absence the relationship between the two is more complicated. This definition would function much the same whether we used om or NN0, but the former allows us to take advantage of 2o = { (/) , 1o } (df2o3 6335) so we adopt it. (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ℕ∞ = { f e. ( 2o ^m om ) | A. i e. om ( f ` suc i ) C_ ( f ` i ) }
Theorem	isomni 7016*	The predicate of being omniscient. (Contributed by Jim Kingdon, 28-Jun-2022.)
|- ( A e. V -> ( A e. Omni <-> A. f ( f : A --> 2o -> ( E. x e. A ( f ` x ) = (/) \/ A. x e. A ( f ` x ) = 1o ) ) ) )
Theorem	isomnimap 7017*	The predicate of being omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 13-Jul-2022.)
|- ( A e. V -> ( A e. Omni <-> A. f e. ( 2o ^m A ) ( E. x e. A ( f ` x ) = (/) \/ A. x e. A ( f ` x ) = 1o ) ) )
Theorem	enomnilem 7018	Lemma for enomni 7019. One direction of the biconditional. (Contributed by Jim Kingdon, 13-Jul-2022.)
|- ( A ~~ B -> ( A e. Omni -> B e. Omni ) )
Theorem	enomni 7019	Omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Limited Principle of Omniscience as either om e. Omni or NN0 e. Omni. The former is a better match to conventional notation in the sense that df2o3 6335 says that 2o = { (/) , 1o } whereas the corresponding relationship does not exist between 2 and { 0 , 1 }. (Contributed by Jim Kingdon, 13-Jul-2022.)
|- ( A ~~ B -> ( A e. Omni <-> B e. Omni ) )
Theorem	finomni 7020	A finite set is omniscient. Remark right after Definition 3.1 of [Pierik], p. 14. (Contributed by Jim Kingdon, 28-Jun-2022.)
|- ( A e. Fin -> A e. Omni )
Theorem	exmidomniim 7021	Given excluded middle, every set is omniscient. Remark following Definition 3.1 of [Pierik], p. 14. This is one direction of the biconditional exmidomni 7022. (Contributed by Jim Kingdon, 29-Jun-2022.)
|- (EXMID -> A. x x e. Omni )
Theorem	exmidomni 7022	Excluded middle is equivalent to every set being omniscient. (Contributed by BJ and Jim Kingdon, 30-Jun-2022.)
|- (EXMID <-> A. x x e. Omni )
Theorem	exmidlpo 7023	Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.)
|- (EXMID -> om e. Omni )
Theorem	fodjuomnilemdc 7024*	Lemma for fodjuomni 7029. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   =>    |- ( ( ph /\ X e. O ) -> DECID E. z e. A ( F ` X ) = (inl ` z ) )
Theorem	fodjuf 7025*	Lemma for fodjuomni 7029 and fodjumkv 7042. Domain and range of P. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   &    |- ( ph -> O e. V )   =>    |- ( ph -> P e. ( 2o ^m O ) )
Theorem	fodjum 7026*	Lemma for fodjuomni 7029 and fodjumkv 7042. A condition which shows that A is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   &    |- ( ph -> E. w e. O ( P ` w ) = (/) )   =>    |- ( ph -> E. x x e. A )
Theorem	fodju0 7027*	Lemma for fodjuomni 7029 and fodjumkv 7042. A condition which shows that A is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   &    |- ( ph -> A. w e. O ( P ` w ) = 1o )   =>    |- ( ph -> A = (/) )
Theorem	fodjuomnilemres 7028*	Lemma for fodjuomni 7029. The final result with P expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.)
|- ( ph -> O e. Omni )   &    |- ( ph -> F : O -onto-> ( A ⊔ B ) )   &    |- P = ( y e. O |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   =>    |- ( ph -> ( E. x x e. A \/ A = (/) ) )
Theorem	fodjuomni 7029*	A condition which ensures A is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.)
|- ( ph -> O e. Omni )   &    |- ( ph -> F : O -onto-> ( A ⊔ B ) )   =>    |- ( ph -> ( E. x x e. A \/ A = (/) ) )
Theorem	infnninf 7030	The point at infinity in ℕ∞ (the constant sequence equal to 1o). (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ( om X. { 1o } ) e. ℕ∞
Theorem	nnnninf 7031*	Elements of ℕ∞ corresponding to natural numbers. The natural number N corresponds to a sequence of N ones followed by zeroes. Contrast to a sequence which is all ones as seen at infnninf 7030. Remark/TODO: the theorem still holds if N = om, that is, the antecedent could be weakened to N e. suc om. (Contributed by Jim Kingdon, 14-Jul-2022.)
|- ( N e. om -> ( i e. om |-> if ( i e. N , 1o , (/) ) ) e. ℕ∞ )
Theorem	ctssexmid 7032*	The decidability condition in ctssdc 7006 is needed. More specifically, ctssdc 7006 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.)
|- ( ( y C_ om /\ E. f f : y -onto-> x ) -> E. f f : om -onto-> ( x ⊔ 1o ) )   &    |- om e. Omni   =>    |- ( ph \/ -. ph )
2.6.37  Markov's principle
Syntax	cmarkov 7033	Extend class definition to include the class of Markov sets.
class Markov
Definition	df-markov 7034*	A Markov set is one where if a predicate (here represented by a function f) on that set does not hold (where hold means is equal to 1o) for all elements, then there exists an element where it fails (is equal to (/)). Generalization of definition 2.5 of [Pierik], p. 9. In particular, om e. Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
|- Markov = { y | A. f ( f : y --> 2o -> ( -. A. x e. y ( f ` x ) = 1o -> E. x e. y ( f ` x ) = (/) ) ) }
Theorem	ismkv 7035*	The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.)
|- ( A e. V -> ( A e. Markov <-> A. f ( f : A --> 2o -> ( -. A. x e. A ( f ` x ) = 1o -> E. x e. A ( f ` x ) = (/) ) ) ) )
Theorem	ismkvmap 7036*	The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.)
|- ( A e. V -> ( A e. Markov <-> A. f e. ( 2o ^m A ) ( -. A. x e. A ( f ` x ) = 1o -> E. x e. A ( f ` x ) = (/) ) ) )
Theorem	ismkvnex 7037*	The predicate of being Markov stated in terms of double negation and comparison with 1o. (Contributed by Jim Kingdon, 29-Nov-2023.)
|- ( A e. V -> ( A e. Markov <-> A. f e. ( 2o ^m A ) ( -. -. E. x e. A ( f ` x ) = 1o -> E. x e. A ( f ` x ) = 1o ) ) )
Theorem	omnimkv 7038	An omniscient set is Markov. In particular, the case where A is om means that the Limited Principle of Omniscience (LPO) implies Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
|- ( A e. Omni -> A e. Markov )
Theorem	exmidmp 7039	Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.)
|- (EXMID -> om e. Markov )
Theorem	mkvprop 7040*	Markov's Principle expressed in terms of propositions (or more precisely, the A = om case is Markov's Principle). (Contributed by Jim Kingdon, 19-Mar-2023.)
|- ( ( A e. Markov /\ A. n e. A DECID ph /\ -. A. n e. A -. ph ) -> E. n e. A ph )
Theorem	fodjumkvlemres 7041*	Lemma for fodjumkv 7042. The final result with P expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> M e. Markov )   &    |- ( ph -> F : M -onto-> ( A ⊔ B ) )   &    |- P = ( y e. M |-> if ( E. z e. A ( F ` y ) = (inl ` z ) , (/) , 1o ) )   =>    |- ( ph -> ( A =/= (/) -> E. x x e. A ) )
Theorem	fodjumkv 7042*	A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.)
|- ( ph -> M e. Markov )   &    |- ( ph -> F : M -onto-> ( A ⊔ B ) )   =>    |- ( ph -> ( A =/= (/) -> E. x x e. A ) )
Theorem	enmkvlem 7043	Lemma for enmkv 7044. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.)
|- ( A ~~ B -> ( A e. Markov -> B e. Markov ) )
Theorem	enmkv 7044	Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either om e. Markov or NN0 e. Markov. The former is a better match to conventional notation in the sense that df2o3 6335 says that 2o = { (/) , 1o } whereas the corresponding relationship does not exist between 2 and { 0 , 1 }. (Contributed by Jim Kingdon, 24-Jun-2024.)
|- ( A ~~ B -> ( A e. Markov <-> B e. Markov ) )
2.6.38  Weakly omniscient sets
Syntax	cwomni 7045	Extend class definition to include the class of weakly omniscient sets.
class WOmni
Definition	df-womni 7046*	A weakly omniscient set is one where we can decide whether a predicate (here represented by a function f) holds (is equal to 1o) for all elements or not. Generalization of definition 2.4 of [Pierik], p. 9. In particular, om e. WOmni is known as the Weak Limited Principle of Omniscience (WLPO). The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- WOmni = { y | A. f ( f : y --> 2o -> DECID A. x e. y ( f ` x ) = 1o ) }
Theorem	iswomni 7047*	The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- ( A e. V -> ( A e. WOmni <-> A. f ( f : A --> 2o -> DECID A. x e. A ( f ` x ) = 1o ) ) )
Theorem	iswomnimap 7048*	The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- ( A e. V -> ( A e. WOmni <-> A. f e. ( 2o ^m A )DECID A. x e. A ( f ` x ) = 1o ) )
Theorem	omniwomnimkv 7049	A set is omniscient if and only if it is weakly omniscient and Markov. The case A = om says that LPO <-> WLPO /\ MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.)
|- ( A e. Omni <-> ( A e. WOmni /\ A e. Markov ) )
Theorem	enwomnilem 7050	Lemma for enwomni 7051. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
|- ( A ~~ B -> ( A e. WOmni -> B e. WOmni ) )
Theorem	enwomni 7051	Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either om e. WOmni or NN0 e. WOmni. The former is a better match to conventional notation in the sense that df2o3 6335 says that 2o = { (/) , 1o } whereas the corresponding relationship does not exist between 2 and { 0 , 1 }. (Contributed by Jim Kingdon, 20-Jun-2024.)
|- ( A ~~ B -> ( A e. WOmni <-> B e. WOmni ) )
2.6.39  Cardinal numbers
Syntax	ccrd 7052	Extend class definition to include the cardinal size function.
class card
Definition	df-card 7053*	Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.)
|- card = ( x e. _V |-> |^| { y e. On | y ~~ x } )
Theorem	cardcl 7054*	The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
|- ( E. y e. On y ~~ A -> ( card ` A ) e. On )
Theorem	isnumi 7055	A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. On /\ A ~~ B ) -> B e. dom card )
Theorem	finnum 7056	Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( A e. Fin -> A e. dom card )
Theorem	onenon 7057	Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
|- ( A e. On -> A e. dom card )
Theorem	cardval3ex 7058*	The value of ( card ` A ). (Contributed by Jim Kingdon, 30-Aug-2021.)
|- ( E. x e. On x ~~ A -> ( card ` A ) = |^| { y e. On | y ~~ A } )
Theorem	oncardval 7059*	The value of the cardinal number function with an ordinal number as its argument. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
|- ( A e. On -> ( card ` A ) = |^| { x e. On | x ~~ A } )
Theorem	cardonle 7060	The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.)
|- ( A e. On -> ( card ` A ) C_ A )
Theorem	card0 7061	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
|- ( card ` (/) ) = (/)
Theorem	carden2bex 7062*	If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
|- ( ( A ~~ B /\ E. x e. On x ~~ A ) -> ( card ` A ) = ( card ` B ) )
Theorem	pm54.43 7063	Theorem *54.43 of [WhiteheadRussell] p. 360. (Contributed by NM, 4-Apr-2007.)
|- ( ( A ~~ 1o /\ B ~~ 1o ) -> ( ( A i^i B ) = (/) <-> ( A u. B ) ~~ 2o ) )
Theorem	pr2nelem 7064	Lemma for pr2ne 7065. (Contributed by FL, 17-Aug-2008.)
|- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o )
Theorem	pr2ne 7065	If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o <-> A =/= B ) )
Theorem	exmidonfinlem 7066*	Lemma for exmidonfin 7067. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
|- A = { { x e. { (/) } | ph } , { x e. { (/) } | -. ph } }   =>    |- ( om = ( On i^i Fin ) -> DECID ph )
Theorem	exmidonfin 7067	If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6774 and nnon 4531. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
|- ( om = ( On i^i Fin ) -> EXMID )
Theorem	en2eleq 7068	Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } )
Theorem	en2other2 7069	Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
|- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X )
Theorem	dju1p1e2 7070	Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- ( 1o ⊔ 1o ) ~~ 2o
Theorem	infpwfidom 7071	The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption ( ~P A i^i Fin ) e. _V because this theorem also implies that A is a set if ~P A i^i Fin is.) (Contributed by Mario Carneiro, 17-May-2015.)
|- ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) )
Theorem	exmidfodomrlemeldju 7072	Lemma for exmidfodomr 7077. A variant of djur 6962. (Contributed by Jim Kingdon, 2-Jul-2022.)
|- ( ph -> A C_ 1o )   &    |- ( ph -> B e. ( A ⊔ 1o ) )   =>    |- ( ph -> ( B = (inl ` (/) ) \/ B = (inr ` (/) ) ) )
Theorem	exmidfodomrlemreseldju 7073	Lemma for exmidfodomrlemrALT 7076. A variant of eldju 6961. (Contributed by Jim Kingdon, 9-Jul-2022.)
|- ( ph -> A C_ 1o )   &    |- ( ph -> B e. ( A ⊔ 1o ) )   =>    |- ( ph -> ( ( (/) e. A /\ B = ( (inl |` A ) ` (/) ) ) \/ B = ( (inr |` 1o ) ` (/) ) ) )
Theorem	exmidfodomrlemim 7074*	Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- (EXMID -> A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) )
Theorem	exmidfodomrlemr 7075*	The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) -> EXMID )
Theorem	exmidfodomrlemrALT 7076*	The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7075. In particular, this proof uses eldju 6961 instead of djur 6962 and avoids djulclb 6948. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.)
|- ( A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) -> EXMID )
Theorem	exmidfodomr 7077*	Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.)
|- (EXMID <-> A. x A. y ( ( E. z z e. y /\ y ~<_ x ) -> E. f f : x -onto-> y ) )
2.6.40  Axiom of Choice equivalents
Syntax	wac 7078	Formula for an abbreviation of the axiom of choice.
wff CHOICE
Definition	df-ac 7079*	The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of [Enderton] p. 49. There are some decisions about how to write this definition especially around whether ax-setind 4460 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.)
|- (CHOICE <-> A. x E. f ( f C_ x /\ f Fn dom x ) )
Theorem	acfun 7080*	A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.)
|- ( ph -> CHOICE )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. x e. A E. w w e. x )   =>    |- ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. x ) )
Theorem	exmidaclem 7081*	Lemma for exmidac 7082. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.)
|- A = { x e. { (/) , { (/) } } | ( x = (/) \/ y = { (/) } ) }   &    |- B = { x e. { (/) , { (/) } } | ( x = { (/) } \/ y = { (/) } ) }   &    |- C = { A , B }   =>    |- (CHOICE -> EXMID )
Theorem	exmidac 7082	The axiom of choice implies excluded middle. See acexmid 5781 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.)
|- (CHOICE -> EXMID )
2.6.41  Cardinal number arithmetic
Theorem	endjudisj 7083	Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A e. V /\ B e. W /\ ( A i^i B ) = (/) ) -> ( A ⊔ B ) ~~ ( A u. B ) )
Theorem	djuen 7084	Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.)
|- ( ( A ~~ B /\ C ~~ D ) -> ( A ⊔ C ) ~~ ( B ⊔ D ) )
Theorem	djuenun 7085	Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.)
|- ( ( A ~~ B /\ C ~~ D /\ ( B i^i D ) = (/) ) -> ( A ⊔ C ) ~~ ( B u. D ) )
Theorem	dju1en 7086	Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ -. A e. A ) -> ( A ⊔ 1o ) ~~ suc A )
Theorem	dju0en 7087	Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( A e. V -> ( A ⊔ (/) ) ~~ A )
Theorem	xp2dju 7088	Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( 2o X. A ) = ( A ⊔ A )
Theorem	djucomen 7089	Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W ) -> ( A ⊔ B ) ~~ ( B ⊔ A ) )
Theorem	djuassen 7090	Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ( A ⊔ B ) ⊔ C ) ~~ ( A ⊔ ( B ⊔ C ) ) )
Theorem	xpdjuen 7091	Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( A X. ( B ⊔ C ) ) ~~ ( ( A X. B ) ⊔ ( A X. C ) ) )
Theorem	djudoml 7092	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> A ~<_ ( A ⊔ B ) )
Theorem	djudomr 7093	A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.)
|- ( ( A e. V /\ B e. W ) -> B ~<_ ( A ⊔ B ) )
PART 3  CHOICE PRINCIPLES We have already introduced the full Axiom of Choice df-ac 7079 but since it implies excluded middle as shown at exmidac 7082, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle.
3.1  Countable Choice and Dependent Choice
3.1.1  Introduce Countable Choice
Syntax	wacc 7094	Formula for an abbreviation of countable choice.
wff CCHOICE
Definition	df-cc 7095*	The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7079 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.)
|- (CCHOICE <-> A. x ( dom x ~~ om -> E. f ( f C_ x /\ f Fn dom x ) ) )
Theorem	ccfunen 7096*	Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A ~~ om )   &    |- ( ph -> A. x e. A E. w w e. x )   =>    |- ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. x ) )
Theorem	cc1 7097*	Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- (CCHOICE -> A. x ( ( x ~~ om /\ A. z e. x E. w w e. z ) -> E. f A. z e. x ( f ` z ) e. z ) )
Theorem	cc2lem 7098*	Lemma for cc2 7099. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> F Fn om )   &    |- ( ph -> A. x e. om E. w w e. ( F ` x ) )   &    |- A = ( n e. om |-> ( { n } X. ( F ` n ) ) )   &    |- G = ( n e. om |-> ( 2nd ` ( f ` ( A ` n ) ) ) )   =>    |- ( ph -> E. g ( g Fn om /\ A. n e. om ( g ` n ) e. ( F ` n ) ) )
Theorem	cc2 7099*	Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> F Fn om )   &    |- ( ph -> A. x e. om E. w w e. ( F ` x ) )   =>    |- ( ph -> E. g ( g Fn om /\ A. n e. om ( g ` n ) e. ( F ` n ) ) )
Theorem	cc3 7100*	Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
|- ( ph -> CCHOICE )   &    |- ( ph -> A. n e. N F e. _V )   &    |- ( ph -> A. n e. N E. w w e. F )   &    |- ( ph -> N ~~ om )   =>    |- ( ph -> E. f ( f Fn N /\ A. n e. N ( f ` n ) e. F ) )