P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nelscottrankgt 35801	If a member of the input set is not a member of the Scott's trick set, then its rank is greater than the rank of a member of the Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026.)
⊢ ((𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ Scott 𝐵) → (rank‘𝐴) ∈ (rank‘𝐶))
Theorem	scottsn 35802	Applying Scott's trick to a singleton leaves it unchanged. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ Scott {𝐴} = {𝐴}
Theorem	scott0bOLD 35803	Obsolete version of scott0b 9939 as of 18-Jul-2026. (Contributed by BTernaryTau, 3-Jul-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 = ∅ ↔ Scott 𝐴 = ∅)
Theorem	rankscott 35804	The rank of a nonempty Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026.)
⊢ (𝐴 ≠ ∅ → (rank‘Scott 𝐴) = suc ∩ (rank “ 𝐴))
Theorem	rankscottu 35805	An upper bound on the rank of a Scott's trick set. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → (rank‘Scott 𝐵) ⊆ suc (rank‘𝐴))
Theorem	scottssr1 35806	Relationship between a Scott's trick set and the cumulative hierarchy. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ 𝐵 → Scott 𝐵 ⊆ (𝑅1‘suc (rank‘𝐴)))
Theorem	dfac15 35807*	Axiom of Choice equivalent: every set can be mapped one-to-one into the ordinals. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ (CHOICE ↔ ∀𝑥∃𝑓 𝑓:𝑥–1-1→On)
Theorem	dfac16 35808*	Axiom of Choice equivalent: for every pair of sets, one is dominated by the other (see also entri3 10645). (Contributed by BTernaryTau, 17-Sep-2026.)
⊢ (CHOICE ↔ ∀𝑥∀𝑦(𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥))
Theorem	acnum 35809	The Axiom of Choice implies that any set is numerable. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (CHOICE → (𝐴 ∈ 𝑉 → 𝐴 ∈ dom card))
Theorem	weexenwe 35810*	If a well-ordering of an infinite set exists, then a well-ordering equinumerous to the set exists. (Contributed by BTernaryTau, 31-Jul-2026.)
⊢ ((∃𝑟 𝑟 We 𝐴 ∧ ω ≼ 𝐴) → ∃𝑠(𝑠 ⊆ (𝐴 × 𝐴) ∧ 𝑠 We 𝐴 ∧ 𝑠 ≈ 𝐴))
Theorem	infinfnum 35811	Equivalence between two infiniteness criteria for numerable sets. (Contributed by BTernaryTau, 15-Jul-2026.)
⊢ (𝐴 ∈ dom card → (¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴))
Theorem	rncardr1prc 35812	The Axiom of Choice implies that the cardinalities of the layers of the cumulative hierarchy form a proper class. (Contributed by BTernaryTau, 2-Jul-2026.)
⊢ (CHOICE → ¬ ran (card ∘ 𝑅1) ∈ V)
Theorem	acwer1prclem 35813*	Lemma for acwer1prc 35814. (Contributed by BTernaryTau, 31-Jul-2026.)
⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    ⇒   ⊢ ((CHOICE ∧ ω ≼ 𝐴 ∧ (card‘(𝑅1‘𝐵)) = 𝐴) → ∃𝑠((card‘𝑠) ∈ (card “ 𝑊) ∧ (card‘𝑠) = 𝐴))
Theorem	acwer1prc 35814*	The class of all well-orderings of the stages of the cumulative hierarchy is a proper class. (Contributed by BTernaryTau, 31-Jul-2026.)
⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    ⇒   ⊢ (CHOICE → ¬ 𝑊 ∈ V)
21.6.2.1  Ordinals 5 through 9
Syntax	c5o 35815	Extend the definition of a class to include the ordinal number 5.
class 5o
Syntax	c6o 35816	Extend the definition of a class to include the ordinal number 6.
class 6o
Syntax	c7o 35817	Extend the definition of a class to include the ordinal number 7.
class 7o
Syntax	c8o 35818	Extend the definition of a class to include the ordinal number 8.
class 8o
Syntax	c9o 35819	Extend the definition of a class to include the ordinal number 9.
class 9o
Definition	df-5o 35820	Define the ordinal number 5. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 5o = suc 4o
Definition	df-6o 35821	Define the ordinal number 6. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 6o = suc 5o
Definition	df-7o 35822	Define the ordinal number 7. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 7o = suc 6o
Definition	df-8o 35823	Define the ordinal number 8. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 8o = suc 7o
Definition	df-9o 35824	Define the ordinal number 9. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 9o = suc 8o
Theorem	5on 35825	Ordinal 5 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 5o ∈ On
Theorem	6on 35826	Ordinal 6 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 6o ∈ On
Theorem	7on 35827	Ordinal 7 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 7o ∈ On
Theorem	8on 35828	Ordinal 8 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 8o ∈ On
Theorem	9on 35829	Ordinal 9 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 9o ∈ On
Theorem	5onn 35830	The ordinal 5 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 5o ∈ ω
Theorem	6onn 35831	The ordinal 6 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 6o ∈ ω
Theorem	7onn 35832	The ordinal 7 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 7o ∈ ω
Theorem	8onn 35833	The ordinal 8 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 8o ∈ ω
Theorem	9onn 35834	The ordinal 9 is a natural number. (Contributed by BTernaryTau, 4-Sep-2026.)
⊢ 9o ∈ ω
21.6.2.2  Finitism
Theorem	prcinf 35835*	Any proper class is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. This proof holds regardless of whether the Axiom of Infinity is accepted or negated. (Contributed by BTernaryTau, 22-Jun-2025.)
⊢ (¬ 𝐴 ∈ V → ∀𝑛 ∈ ω ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛))
Theorem	fineqvrep 35836*	If all sets are finite, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
Theorem	fineqvpow 35837*	If all sets are finite, then the Axiom of Power Sets becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024.)
⊢ (Fin = V → ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
Theorem	fineqvac 35838	If all sets are finite, then the Axiom of Choice becomes redundant. For a shorter proof using ax-rep 5231 and ax-pow 5326, see fineqvacALT 35839. (Contributed by BTernaryTau, 21-Sep-2024.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvacALT 35839	Shorter proof of fineqvac 35838 using ax-rep 5231 and ax-pow 5326. (Contributed by BTernaryTau, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Fin = V → CHOICE)
Theorem	fineqvomon 35840	If all sets are finite, then the class of all natural numbers equals the proper class of all ordinal numbers. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (Fin = V → ω = On)
Theorem	fineqvomonb 35841	All sets are finite iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (Fin = V ↔ ω = On)
Theorem	omprcomonb 35842	The class of all finite ordinals is a proper class iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026.)
⊢ (¬ ω ∈ V ↔ ω = On)
Theorem	fineqvnttrclselem1 35843*	Lemma for fineqvnttrclse 35846. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ (𝐵 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝐴 +o 𝑑) = 𝐵} ∈ ω)
Theorem	fineqvnttrclselem2 35844*	Lemma for fineqvnttrclse 35846. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵 ∧ 𝐴 ∈ suc suc 𝑁) → (𝐴 +o (𝐹‘𝐴)) = 𝐵)
Theorem	fineqvnttrclselem3 35845*	Lemma for fineqvnttrclse 35846. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    &   ⊢ 𝐹 = (𝑣 ∈ suc suc 𝑁 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝐵})    ⇒   ⊢ ((𝐵 ∈ (ω ∖ 1o) ∧ 𝑁 ∈ 𝐵) → ∀𝑎 ∈ suc 𝑁(𝐹‘𝑎)𝑅(𝐹‘suc 𝑎))
Theorem	fineqvnttrclse 35846*	A counterexample demonstrating that ttrclse 9730 does not hold when all sets are finite. (Contributed by BTernaryTau, 12-Jan-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}    &   ⊢ 𝐴 = ω    ⇒   ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))
Theorem	fineqvinfep 35847*	A counterexample demonstrating that tz9.1 9732 does not hold when all sets are finite and an infinite descending ∈-chain exists. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ 𝐴 = {(𝐹‘∅)}    ⇒   ⊢ ((Fin = V ∧ 𝐹:ω–1-1→V ∧ ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ¬ ∃𝑦(𝐴 ⊆ 𝑦 ∧ Tr 𝑦))
21.6.2.3  Introduce ax-regs
Axiom	ax-regs 35848*	A strong version of the Axiom of Regularity. It states that if there exists a set with property 𝜑, then there must exist a set with property 𝜑 such that none of its elements have property 𝜑. This axiom can be derived from the axioms of ZF set theory as shown in axregs 35861, but this derivation relies on ax-inf2 9644 and is thus not possible in a finitist context. (Contributed by BTernaryTau, 29-Dec-2025.)
⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
Theorem	axreg 35849*	Derivation of ax-reg 9588 from ax-regs 35848 and Tarski's FOL axiom schemes. This demonstrates the sense in which ax-regs 35848 is a stronger version of ax-reg 9588. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	axregscl 35850*	A version of ax-regs 35848 with a class variable instead of a wff variable. Axiom D in Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory (1940), p. 6. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴)))
Theorem	axregszf 35851*	Derivation of zfregs 9735 using ax-regs 35848. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	setindregs 35852*	Set (epsilon) induction. This version of setind 9750 replaces zfregs 9735 with axregszf 35851. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V)
Theorem	setinds2regs 35853*	Principle of set induction (or E-induction). If a property passes from all elements of 𝑥 to 𝑥 itself, then it holds for all 𝑥. (Contributed by BTernaryTau, 31-Dec-2025.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	noinfepfnregs 35854*	There are no infinite descending ∈-chains, proven using ax-regs 35848. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ (𝐹 Fn ω → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))
Theorem	noinfepregs 35855*	There are no infinite descending ∈-chains, proven using ax-regs 35848. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)
Theorem	tz9.1regs 35856*	Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9732 depends on ax-regs 35848 instead of ax-reg 9588 and ax-inf2 9644. This suggests a possible answer to the third question posed in tz9.1 9732, namely that the missing property is that countably infinite classes must obey regularity. In ZF set theory we can prove this by showing that countably infinite classes are sets and thus ax-reg 9588 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35848 is required since countably infinite classes are proper classes. A related candidate for the missing property is the non-existence of infinite descending ∈-chains, proven as noinfep 9663 using ax-reg 9588 and ax-inf2 9644 and as noinfepregs 35855 using ax-regs 35848. If all sets are finite, then the existence of such a chain implies there is a set which does not have a transitive closure, as shown in fineqvinfep 35847. (Contributed by BTernaryTau, 31-Dec-2025.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
Theorem	unir1regs 35857	The cumulative hierarchy of sets covers the universe. This version of unir1 9823 replaces setind 9750 with setindregs 35852. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ ∪ (𝑅1 “ On) = V
Theorem	trssfir1omregs 35858	If every element in a transitive class is finite, then every element is also hereditarily finite. This version of trssfir1om 35787 replaces setinds2 9754 with setinds2regs 35853. (Contributed by BTernaryTau, 20-Jan-2026.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ ∪ (𝑅1 “ ω))
Theorem	r1omhfbregs 35859*	The class of all hereditarily finite sets is the only class with the property that all sets are members of it iff they are finite and all of their elements are members of it. This version of r1omhfb 35788 replaces setinds2 9754 with setinds2regs 35853 and trssfir1om 35787 with trssfir1omregs 35858. (Contributed by BTernaryTau, 21-Jan-2026.)
⊢ (𝐻 = ∪ (𝑅1 “ ω) ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻)))
Theorem	fineqvr1ombregs 35860	All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ (Fin = V ↔ ∪ (𝑅1 “ ω) = V)
21.6.2.4  Derive ax-regs
Theorem	axregs 35861*	Derivation of ax-regs 35848 from the axioms of ZF set theory. (Contributed by BTernaryTau, 29-Dec-2025.)
⊢ (∃𝑥𝜑 → ∃𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ ∀𝑥(𝑥 = 𝑧 → 𝜑))))
21.6.2.5  ZFC axioms with reduced distinct variable conditions
Theorem	axsepg2 35862*	A generalization of ax-sep 5248 in which 𝑥 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5248 with the degenerate instance ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑧 ∧ 𝜑)) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by BTernaryTau, 21-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3 35863*	A generalization of ax-sep 5248 in which 𝑦 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5248 with the degenerate instance ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑦 ∧ 𝜑)) which is satisfied by the existence of the empty set. Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3ALT 35864*	Alternate proof of axsepg3 35863, derived directly from ax-sep 5248 with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg4 35865*	A generalization of ax-sep 5248 that combines axsepg 5249 and axsepg2 35862 into a single theorem scheme. Unlike ax-sep 5248, this scheme lacks a distinct variable condition for 𝜑 and 𝑧 as well as for 𝑥 and 𝑧. Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg5 35866*	A generalization of ax-sep 5248 that combines axsepg 5249, axsepg2 35862, and axsepg3 35863 into a single theorem scheme. Unlike ax-sep 5248, this scheme lacks a distinct variable condition for 𝜑 and 𝑧, for 𝑥 and 𝑧, and for 𝑦 and 𝑧. Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axnulg 35867	A generalization of ax-nul 5259 in which 𝑥 and 𝑦 need not be distinct. This theorem scheme bundles ax-nul 5259 with the degenerate instance ∃𝑥∀𝑥¬ 𝑥 ∈ 𝑥 which is satisfied by elirrv 9593. Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axpowg 35868*	A generalization of ax-pow 5326 that combines it and zfpow 5327 into a single theorem scheme. Unlike ax-pow 5326, this scheme lacks a distinct variable condition for 𝑦 and 𝑤. (Contributed by BTernaryTau, 26-May-2026.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg2 35869*	A generalization of ax-pow 5326 in which 𝑥 and 𝑤 need not be distinct. This theorem scheme bundles ax-pow 5326 with the degenerate instance ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 5384). Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg3 35870*	A generalization of ax-pow 5326 that combines axpowg 35868 and axpowg2 35869 into a single theorem scheme. Unlike ax-pow 5326, this scheme lacks a distinct variable condition for 𝑦 and 𝑤 as well as for 𝑥 and 𝑤. Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
21.6.2.6  Cardinality without the Axiom of Choice
Syntax	ckard 35871	Extend class definition to include the alternative cardinal size function.
class kard
Definition	df-kard 35872*	Define the alternative cardinal number function. Under this definition, the cardinal number of a set is the set of all sets equinumerous to it and having the least possible rank. Definition of [Enderton] p. 222. See kardval 35874 for its value. The principal theorem relating this type of cardinality to equinumerosity is kardeng 35879. Our notation is from Enderton and differentiates this function from the standard cardinal size function defined in df-card 10022. (Contributed by BTernaryTau, 2-Jul-2026.)
⊢ kard = (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})
Theorem	kardfn 35873	The kard class is a function on the universe. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ kard Fn V
Theorem	kardval 35874*	The value of the kard function. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. See also kardval2 35875. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = Scott {𝑥 ∣ 𝑥 ≈ 𝐴}
Theorem	kardval2 35875*	The value of the kard function. This theorem depends on the Axiom of Regularity and the Axiom of Infinity, but it does not depend on the Axiom of Choice. See also kardval 35874. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	kard0 35876	The kard cardinality of the empty set is the singleton of the empty set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘∅) = {∅}
Theorem	elkarden 35877	Any member of the kard cardinal number of a set is equinumerous to the set. Contrast with cardne 10048 for card cardinals. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ (kard‘𝐵) → 𝐴 ≈ 𝐵)
Theorem	kardeq0 35878	Applying kard to a class yields the empty set iff the class is a proper class. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = ∅ ↔ ¬ 𝐴 ∈ V)
Theorem	kardeng 35879	Two sets are equinumerous iff their kard cardinal numbers are equal. Unlike carden 10637, this theorem does not depend on the Axiom of Choice, but it does depend on the Axiom of Regularity and the Axiom of Infinity. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ 𝑉 → ((kard‘𝐴) = (kard‘𝐵) ↔ 𝐴 ≈ 𝐵))
Theorem	kardenir 35880	If two sets are equinumerous, then their kard cardinal numbers are equal. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ≈ 𝐵 → (kard‘𝐴) = (kard‘𝐵))
Theorem	kard0b 35881	The empty set is the only set with cardinality zero. This is the kard version of cardeq0 10638. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = (kard‘∅) ↔ 𝐴 = ∅)
Theorem	kardsn 35882	A singleton has cardinality one. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ 𝑉 → (kard‘{𝐴}) = (kard‘1o))
Theorem	karddom 35883*	One set dominates another iff an element in its kard cardinality dominates an element in the second set's kard cardinality. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥 ∈ (kard‘𝐴)∃𝑦 ∈ (kard‘𝐵)𝑥 ≼ 𝑦)
Theorem	kardsdom 35884*	One set strictly dominates another iff an element in its kard cardinality strictly dominates an element in the second set's kard cardinality. (Contributed by BTernaryTau, 6-Jul-2026.)
⊢ (𝐴 ≺ 𝐵 ↔ ∃𝑥 ∈ (kard‘𝐴)∃𝑦 ∈ (kard‘𝐵)𝑥 ≺ 𝑦)
Theorem	kardexen 35885*	One set is equinumerous to another iff an element in its kard cardinality is equinumerous to an element in the second set's kard cardinality. See kardeng 35879 for a version with equality of cardinals. (Contributed by BTernaryTau, 7-Jul-2026.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑥 ∈ (kard‘𝐴)∃𝑦 ∈ (kard‘𝐵)𝑥 ≈ 𝑦)
Theorem	kardcard2a 35886	If two sets have equal nonzero card cardinalities, then they have equal kard cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (((card‘𝐴) = (card‘𝐵) ∧ (card‘𝐴) ≠ ∅) → (kard‘𝐴) = (kard‘𝐵))
Theorem	kardcard2b 35887	If two sets have equal kard cardinalities, then they have equal card cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = (kard‘𝐵) → (card‘𝐴) = (card‘𝐵))
Theorem	kardcard2 35888	Two numerable sets have equal kard cardinalities iff they have equal card cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((kard‘𝐴) = (kard‘𝐵) ↔ (card‘𝐴) = (card‘𝐵)))
Theorem	ackardcard 35889	The Axiom of Choice implies that two sets have equal kard cardinalities iff they have equal card cardinalities. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (CHOICE → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((kard‘𝐴) = (kard‘𝐵) ↔ (card‘𝐴) = (card‘𝐵))))
Theorem	kardcard 35890	Two sets have equal kard cardinalities iff they have equal card cardinalities. This theorem depends on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((kard‘𝐴) = (kard‘𝐵) ↔ (card‘𝐴) = (card‘𝐵)))
Theorem	kardnnfi 35891	The kard cardinal number of a finite ordinal is finite. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ ω → (kard‘𝐴) ∈ Fin)
Theorem	kardfi 35892	The kard cardinal number of a finite set is finite. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ Fin → (kard‘𝐴) ∈ Fin)
Theorem	rankkardu 35893	An upper bound on the rank of a kard cardinal. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (rank‘(kard‘𝐴)) ⊆ suc (rank‘𝐴)
Theorem	1enumkard 35894*	The Fundamental Theorem of Enumeration (see https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf), extended to all sets. The expression ∪ 𝑥 ∈ 𝐴({𝑥} × 𝐵) can be thought of as expressing an indexed disjoint union ⊔ 𝑥 ∈ 𝐴𝐵 where each 𝐵 has its elements tagged with the set 𝑥 that generated it. See the comment directly before undjudom 10248 for context on disjoint union as a representation of cardinal addition. This theorem is not limited to numerable sets, but it also does not depend on AC. See 1enumen 35773 for a version that uses equinumerosity , 1enumcard 35774 for a version that uses the card function, and 1enum 35978 for a version that uses an explicit sum of complex number 1s. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ V → (kard‘𝐴) = (kard‘∪ 𝑥 ∈ 𝐴 ({𝑥} × 1o)))
21.6.2.7  Gödel operations
Syntax	ccnv2 35895	Extend the definition of a class to include the second converse function.
class Cnv2
Syntax	ccnv3 35896	Extend the definition of a class to include the third converse function.
class Cnv3
Syntax	cgdlop1 35897	Extend the definition of a class to include the first Gödel operation.
class ℱ1
Syntax	cgdlop2 35898	Extend the definition of a class to include the second Gödel operation.
class ℱ2
Syntax	cgdlop3 35899	Extend the definition of a class to include the third Gödel operation.
class ℱ3
Syntax	cgdlop4 35900	Extend the definition of a class to include the fourth Gödel operation.
class ℱ4