P. 96 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oien 9501	The order type of a well-ordered set is equinumerous to the set. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → dom 𝐹 ≈ 𝐴)
Theorem	oieu 9502	Uniqueness of the unique ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ((Ord 𝐵 ∧ 𝐺 Isom E , 𝑅 (𝐵, 𝐴)) ↔ (𝐵 = dom 𝐹 ∧ 𝐺 = 𝐹)))
Theorem	oismo 9503	When 𝐴 is a subclass of On, 𝐹 is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of 𝐴). The proof avoids ax-rep 5239 (the second statement is trivial under ax-rep 5239). (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = OrdIso( E , 𝐴)    ⇒   ⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴))
Theorem	oiid 9504	The order type of an ordinal under the ∈ order is itself, and the order isomorphism is the identity function. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ (Ord 𝐴 → OrdIso( E , 𝐴) = ( I ↾ 𝐴))
Theorem	hartogslem1 9505*	Lemma for hartogs 9507. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}    &   ⊢ 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}    ⇒   ⊢ (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴 ∈ 𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}))
Theorem	hartogslem2 9506*	Lemma for hartogs 9507. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}    &   ⊢ 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V)
Theorem	hartogs 9507*	The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9505 and hartogslem2 9506) proof can be given using the axiom of choice, see ondomon 10548. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9520. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On)
Theorem	wofib 9508	The only sets which are well-ordered forwards and backwards are finite sets. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 23-May-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ↔ (𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴))
Theorem	wemaplem1 9509*	Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏)))))
Theorem	wemaplem2 9510*	Lemma for wemapso 9514. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)))    &   ⊢ (𝜑 → 𝑏 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐)))    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemaplem3 9511*	Lemma for wemapso 9514. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑃𝑇𝑋)    &   ⊢ (𝜑 → 𝑋𝑇𝑄)    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemappo 9512*	Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴))
Theorem	wemapsolem 9513*	Lemma for wemapso 9514. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Or 𝐵)    &   ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑈)
Theorem	wemapso 9514*	Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑m 𝐴))
Theorem	wemapso2lem 9515*	Lemma for wemapso2 9516. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈)
Theorem	wemapso2 9516*	An alternative to having a well-order on 𝑅 in wemapso 9514 is to restrict the function set to finitely-supported functions. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or 𝑈)
Theorem	card2on 9517*	The alternate definition of the cardinal of a set given in cardval2 9978 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On
Theorem	card2inf 9518*	The alternate definition of the cardinal of a set given in cardval2 9978 has the curious property that for non-numerable sets (for which ndmfv 6915 yields ∅), it still evaluates to a nonempty set, and indeed it contains ω. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (¬ ∃𝑦 ∈ On 𝑦 ≈ 𝐴 → ω ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})
2.4.40  Hartogs function
Syntax	char 9519	Class symbol for the Hartogs function.
class har
Definition	df-har 9520*	Define the Hartogs function as mapping a set to the class of ordinals it dominates. That class is an ordinal by hartogs 9507, which is used in harf 9521. The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 9984 proves that the Hartogs function actually gives the Hartogs number for well-orderable sets. The Hartogs number of an ordinal is its cardinal successor. This is proved for finite ordinal in harsucnn 9985. Traditionally, the Hartogs number of a set 𝑋 is written ℵ(𝑋), and its cardinal successor, 𝑋 +; we use functional notation for this, and cannot use the aleph symbol because it is taken for the enumerating function of the infinite initial ordinals df-aleph 9927. Some authors define the Hartogs number of a set to be the least *infinite* ordinal which does not inject into it, thus causing the range to consist only of alephs. We use the simpler definition where the value can be any successor cardinal. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥})
Theorem	harf 9521	Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ har:V⟶On
Theorem	harcl 9522	Values of the Hartogs function are ordinals (closure of the Hartogs function in the ordinals). (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (har‘𝑋) ∈ On
Theorem	harval 9523*	Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋})
Theorem	elharval 9524	The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl 9522, this implies that the Hartogs number of a set is greater than all ordinals that set dominates. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝑌 ∈ (har‘𝑋) ↔ (𝑌 ∈ On ∧ 𝑌 ≼ 𝑋))
Theorem	harndom 9525	The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ ¬ (har‘𝑋) ≼ 𝑋
Theorem	harword 9526	Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.)
⊢ (𝑋 ≼ 𝑌 → (har‘𝑋) ⊆ (har‘𝑌))
2.4.41  Weak dominance
Syntax	cwdom 9527	Class symbol for the weak dominance relation.
class ≼*
Definition	df-wdom 9528*	A set is weakly dominated by a "larger" set if the "larger" set can be mapped onto the "smaller" set or the smaller set is empty, or equivalently, if the smaller set can be placed into bijection with some partition of the larger set. Dominance (df-dom 8946) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10508 proves that the axiom of choice implies the partition principle (over ZF). It is not known whether the partition principle is equivalent to the axiom of choice (over ZF), although it is know to imply dependent choice. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}
Theorem	relwdom 9529	Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ Rel ≼*
Theorem	brwdom 9530*	Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))
Theorem	brwdomi 9531*	Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≼* 𝑌 → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))
Theorem	brwdomn0 9532*	Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋))
Theorem	0wdom 9533	Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → ∅ ≼* 𝑋)
Theorem	fowdom 9534	An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼* 𝑌)
Theorem	wdomref 9535	Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋)
Theorem	brwdom2 9536*	Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
Theorem	domwdom 9537	Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌)
Theorem	wdomtr 9538	Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑋 ≼* 𝑍)
Theorem	wdomen1 9539	Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼* 𝐶 ↔ 𝐵 ≼* 𝐶))
Theorem	wdomen2 9540	Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵))
Theorem	wdompwdom 9541	Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌)
Theorem	canthwdom 9542	Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 9119, equivalent to canth 7366). (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ¬ 𝒫 𝐴 ≼* 𝐴
Theorem	wdom2d 9543*	Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 5239). (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* 𝐵)
Theorem	wdomd 9544*	Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* 𝐵)
Theorem	brwdom3 9545*	Condition for weak dominance with a condition reminiscent of wdomd 9544. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑋 ≼* 𝑌 ↔ ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦)))
Theorem	brwdom3i 9546*	Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝑋 ≼* 𝑌 → ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦))
Theorem	unwdomg 9547	Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼* (𝐵 ∪ 𝐷))
Theorem	xpwdomg 9548	Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷))
Theorem	wdomima2g 9549	A set is weakly dominant over its image under any function. This version of wdomimag 9550 is stated so as to avoid ax-rep 5239. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 “ 𝐴) ≼* 𝐴)
Theorem	wdomimag 9550	A set is weakly dominant over its image under any function. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉) → (𝐹 “ 𝐴) ≼* 𝐴)
Theorem	unxpwdom2 9551	Lemma for unxpwdom 9552. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
Theorem	unxpwdom 9552	If a Cartesian product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 × 𝐴) ≼ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
Theorem	ixpiunwdom 9553*	Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 8927 this shows that ∪ 𝑥 ∈ 𝐴𝐵 and X𝑥 ∈ 𝐴𝐵 have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈ 𝐴 𝐵 × 𝐴))
Theorem	harwdom 9554	The value of the Hartogs function at a set 𝑋 is weakly dominated by 𝒫 (𝑋 × 𝑋). This follows from a more precise analysis of the bound used in hartogs 9507 to prove that (har‘𝑋) is an ordinal. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* 𝒫 (𝑋 × 𝑋))
2.5  ZF Set Theory - add the Axiom of Regularity
2.5.1  Introduce the Axiom of Regularity
Axiom	ax-reg 9555*	Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also called the Axiom of Foundation. A rather non-intuitive axiom that denies more than it asserts, it states (in the form of zfreg 9559) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9560). A stronger version that works for proper classes is proved as zfregs 9702. (Contributed by NM, 14-Aug-1993.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	axreg2 9556*	Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.)
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	zfregcl 9557*	The Axiom of Regularity with class variables. (Contributed by NM, 5-Aug-1994.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) Avoid ax-10 2176 and ax-12 2213. (Revised by TM, 31-Dec-2025.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴))
Theorem	zfregclOLD 9558*	Obsolete version of zfregcl 9557 as of 31-Dec-2025. (Contributed by NM, 5-Aug-1994.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴))
Theorem	zfreg 9559*	The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the "weak form". Axiom Reg of [BellMachover] p. 480. There is also a "strong form", not requiring that 𝐴 be a set, that can be proved with more difficulty (see zfregs 9702). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	elirrv 9560	The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. This is trivial to prove from zfregfr 9574 and efrirr 5643 (see elirrvALT 9575), but this proof is direct from ax-reg 9555. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9555 directly. (Revised by BTernaryTau, 27-Dec-2025.) Avoid ax-pr 5406. (Revised by BTernaryTau, 21-May-2026.) (Proof shortened by Matthew House, 23-May-2026.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirrvOLD 9561	Obsolete version of elirrv 9560 as of 21-May-2026. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9555 directly. (Revised by BTernaryTau, 27-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirrvOLDOLD 9562	Obsolete version of elirrv 9560 as of 27-Dec-2025. (Contributed by NM, 19-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirr 9563	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ¬ 𝐴 ∈ 𝐴
Theorem	elneq 9564	A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ≠ 𝐵)
Theorem	nelaneq 9565	A class is not an element of and equal to a class at the same time. Variant of elneq 9564 analogously to elnotel 9580 and en2lp 9576. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof shortened by TM, 31-Dec-2025.) (Proof shortened by SN, 22-Apr-2026.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	nelaneqOLD 9566	Obsolete version of nelaneq 9565 as of 22-Apr-2026. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof shortened by TM, 31-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	nelaneqOLDOLD 9567	Obsolete version of nelaneq 9565 as of 31-Dec-2025. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	epinid0 9568	The membership relation and the identity relation are disjoint. Variable-free version of nelaneq 9565. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.)
⊢ ( E ∩ I ) = ∅
Theorem	sucprcreg 9569	A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004.) (Proof shortened by BJ, 16-Apr-2019.) (Proof shortened by SN, 22-Apr-2026.)
⊢ (¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴)
Theorem	sucprcregOLD 9570	Obsolete version of sucprcreg 9569 as of 31-Dec-2025. (Contributed by NM, 9-Jul-2004.) (Proof shortened by BJ, 16-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴)
Theorem	ruv 9571	The Russell class is equal to the universe V. Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	ruALT 9572	Alternate proof of ru 3744, simplified using (indirectly) the Axiom of Regularity ax-reg 9555. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V
Theorem	disjcsn 9573	A class is disjoint from its singleton. A consequence of regularity. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, 4-Apr-2019.)
⊢ (𝐴 ∩ {𝐴}) = ∅
Theorem	zfregfr 9574	The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.)
⊢ E Fr 𝐴
Theorem	elirrvALT 9575	Alternate proof of elirrv 9560, shorter but using more axioms. (Contributed by BTernaryTau, 28-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	en2lp 9576	No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206. (Contributed by NM, 16-Oct-1996.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴)
Theorem	elnanel 9577	Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9576 and serves as an example in the context of Godel codes, see elnanelprv 35899. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴)
Theorem	cnvepnep 9578	The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9576. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.)
⊢ (◡ E ∩ E ) = ∅
Theorem	epnsym 9579	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ◡ E ≠ E
Theorem	elnotel 9580	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴)
Theorem	elnel 9581	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐵 ∉ 𝐴)
Theorem	en3lplem1 9582*	Lemma for en3lp 9584. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lplem2 9583*	Lemma for en3lp 9584. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝑥 ∩ {𝐴, 𝐵, 𝐶}) ≠ ∅))
Theorem	en3lp 9584	No class has 3-cycle membership loops. This proof was automatically generated from the virtual deduction proof en3lpVD 45533 using a translation program. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)
Theorem	preleqg 9585	Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq 9586. (Contributed by AV, 15-Jun-2022.)
⊢ (((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	preleq 9586	Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Revised by AV, 15-Jun-2022.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (((𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	preleqALT 9587	Alternate proof of preleq 9586, not based on preleqg 9585: Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ (((𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷) ∧ {𝐴, 𝐵} = {𝐶, 𝐷}) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	opthreg 9588	Theorem for alternate representation of ordered pairs, requiring the Axiom of Regularity ax-reg 9555 (via the preleq 9586 step). See df-op 4597 for a description of other ordered pair representations. Exercise 34 of [Enderton] p. 207. (Contributed by NM, 16-Oct-1996.) (Proof shortened by AV, 15-Jun-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    ⇒   ⊢ ({𝐴, {𝐴, 𝐵}} = {𝐶, {𝐶, 𝐷}} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	suc11reg 9589	The successor operation behaves like a one-to-one function (assuming the Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its converse. (Contributed by NM, 25-Oct-2003.)
⊢ (suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵)
Theorem	dford2 9590*	Assuming ax-reg 9555, an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
2.5.2  Axiom of Infinity equivalents
Theorem	inf0 9591*	Existence of ω implies our axiom of infinity ax-inf 9608. The proof shows that the especially contrived class "ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) " exists, is a subset of its union, and contains a given set 𝑥 (and thus is nonempty). Thus, it provides an example demonstrating that a set 𝑦 exists with the necessary properties demanded by ax-inf 9608. (Contributed by NM, 15-Oct-1996.) Revised to closed form. (Revised by BJ, 20-May-2024.)
⊢ (ω ∈ 𝑉 → ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))))
Theorem	inf1 9592	Variation of Axiom of Infinity (using zfinf 9609 as a hypothesis). Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 14-Oct-1996.) (Revised by David Abernethy, 1-Oct-2013.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))    ⇒   ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))
Theorem	inf2 9593*	Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf 9609 as a hypothesis). Abbreviated version of the Axiom of Infinity in [FreydScedrov] p. 283. (Contributed by NM, 28-Oct-1996.)
⊢ ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))    ⇒   ⊢ ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥)
Theorem	inf3lema 9594*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9605 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ (𝐺‘𝐵) ↔ (𝐴 ∈ 𝑥 ∧ (𝐴 ∩ 𝑥) ⊆ 𝐵))
Theorem	inf3lemb 9595*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9605 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹‘∅) = ∅
Theorem	inf3lemc 9596*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9605 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘suc 𝐴) = (𝐺‘(𝐹‘𝐴)))
Theorem	inf3lemd 9597*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9605 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ 𝑥)
Theorem	inf3lem1 9598*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9605 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ ω → (𝐹‘𝐴) ⊆ (𝐹‘suc 𝐴))
Theorem	inf3lem2 9599*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9605 for detailed description. (Contributed by NM, 28-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ 𝑥))
Theorem	inf3lem3 9600*	Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 9605 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg 9559. (Contributed by NM, 29-Oct-1996.)
⊢ 𝐺 = (𝑦 ∈ V ↦ {𝑤 ∈ 𝑥 ∣ (𝑤 ∩ 𝑥) ⊆ 𝑦})    &   ⊢ 𝐹 = (rec(𝐺, ∅) ↾ ω)    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥) → (𝐴 ∈ ω → (𝐹‘𝐴) ≠ (𝐹‘suc 𝐴)))