P. 360 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35901-36000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	noinfepregs 35901*	There are no infinite descending ∈-chains, proven using ax-regs 35894. (Contributed by BTernaryTau, 18-Feb-2026.)
⊢ ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)
Theorem	tz9.1regs 35902*	Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9757 depends on ax-regs 35894 instead of ax-reg 9613 and ax-inf2 9669. This suggests a possible answer to the third question posed in tz9.1 9757, 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 9613 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35894 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 9688 using ax-reg 9613 and ax-inf2 9669 and as noinfepregs 35901 using ax-regs 35894. 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 35893. (Contributed by BTernaryTau, 31-Dec-2025.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
Theorem	unir1regs 35903	The cumulative hierarchy of sets covers the universe. This version of unir1 9848 replaces setind 9775 with setindregs 35898. (Contributed by BTernaryTau, 30-Dec-2025.)
⊢ ∪ (𝑅1 “ On) = V
Theorem	trssfihfregs 35904	If every element in a transitive class is finite, then every element is also hereditarily finite. This version of trssfihf 35819 replaces setinds2 9779 with setinds2regs 35899. (Contributed by BTernaryTau, 20-Jan-2026.) Use HF. (Revised by BTernaryTau, 24-Oct-2026.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ Fin) → 𝐴 ⊆ HF )
Theorem	eqhfregs 35905*	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 eqhf 35820 replaces setinds2 9779 with setinds2regs 35899 and trssfihf 35819 with trssfihfregs 35904. (Contributed by BTernaryTau, 21-Jan-2026.) Use HF. (Revised by BTernaryTau, 24-Oct-2026.)
⊢ (𝐻 = HF ↔ ∀𝑥(𝑥 ∈ 𝐻 ↔ (𝑥 ∈ Fin ∧ ∀𝑦 ∈ 𝑥 𝑦 ∈ 𝐻)))
Theorem	fineqvhfbregs 35906	All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025.) Use HF. (Revised by BTernaryTau, 24-Oct-2026.)
⊢ (Fin = V ↔ HF = V)
21.6.2.4  Derive ax-regs
Theorem	axregs 35907*	Derivation of ax-regs 35894 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 35908*	A generalization of ax-sep 5252 in which 𝑥 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5252 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 2404. (Contributed by BTernaryTau, 21-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3 35909*	A generalization of ax-sep 5252 in which 𝑦 and 𝑧 need not be distinct. This theorem scheme bundles ax-sep 5252 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 2404. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg3ALT 35910*	Alternate proof of axsepg3 35909, derived directly from ax-sep 5252 with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg4 35911*	A generalization of ax-sep 5252 that combines axsepg 5253 and axsepg2 35908 into a single theorem scheme. Unlike ax-sep 5252, 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 2404. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axsepg5 35912*	A generalization of ax-sep 5252 that combines axsepg 5253, axsepg2 35908, and axsepg3 35909 into a single theorem scheme. Unlike ax-sep 5252, 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 2404. (Contributed by BTernaryTau, 24-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	axnulg 35913	A generalization of ax-nul 5263 in which 𝑥 and 𝑦 need not be distinct. This theorem scheme bundles ax-nul 5263 with the degenerate instance ∃𝑥∀𝑥¬ 𝑥 ∈ 𝑥 which is satisfied by elirrv 9618. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 3-Aug-2025.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
Theorem	axpowg 35914*	A generalization of ax-pow 5331 that combines it and zfpow 5332 into a single theorem scheme. Unlike ax-pow 5331, this scheme lacks a distinct variable condition for 𝑦 and 𝑤. (Contributed by BTernaryTau, 26-May-2026.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg2 35915*	A generalization of ax-pow 5331 in which 𝑥 and 𝑤 need not be distinct. This theorem scheme bundles ax-pow 5331 with the degenerate instance ∃𝑦∀𝑧(∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑥) → 𝑧 ∈ 𝑦) which is satisfied by the existence of a set that contains all empty sets (see axprlem1 5389). Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	axpowg3 35916*	A generalization of ax-pow 5331 that combines axpowg 35914 and axpowg2 35915 into a single theorem scheme. Unlike ax-pow 5331, 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 2404. (Contributed by BTernaryTau, 26-May-2026.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
21.6.2.6  Cardinality without the Axiom of Choice
Syntax	ckard 35917	Extend class definition to include the alternative cardinal size function.
class kard
Definition	df-kard 35918*	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 35920 for its value. The principal theorem relating this type of cardinality to equinumerosity is kardeng 35925. Our notation is from Enderton and differentiates this function from the standard cardinal size function defined in df-card 10047. (Contributed by BTernaryTau, 2-Jul-2026.)
⊢ kard = (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})
Theorem	kardfn 35919	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 35920*	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 35921. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = Scott {𝑥 ∣ 𝑥 ≈ 𝐴}
Theorem	kardval2 35921*	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 35920. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘𝐴) = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
Theorem	kard0 35922	The kard cardinality of the empty set is the singleton of the empty set. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (kard‘∅) = {∅}
Theorem	elkarden 35923	Any member of the kard cardinal number of a set is equinumerous to the set. Contrast with cardne 10073 for card cardinals. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ (kard‘𝐵) → 𝐴 ≈ 𝐵)
Theorem	kardeq0 35924	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 35925	Two sets are equinumerous iff their kard cardinal numbers are equal. Unlike carden 10662, 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 35926	If two sets are equinumerous, then their kard cardinal numbers are equal. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ≈ 𝐵 → (kard‘𝐴) = (kard‘𝐵))
Theorem	kard0b 35927	The empty set is the only set with cardinality zero. This is the kard version of cardeq0 10663. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ ((kard‘𝐴) = (kard‘∅) ↔ 𝐴 = ∅)
Theorem	kardsn 35928	A singleton has cardinality one. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (𝐴 ∈ 𝑉 → (kard‘{𝐴}) = (kard‘1o))
Theorem	karddom 35929*	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 35930*	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 35931*	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 35925 for a version with equality of cardinals. (Contributed by BTernaryTau, 7-Jul-2026.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑥 ∈ (kard‘𝐴)∃𝑦 ∈ (kard‘𝐵)𝑥 ≈ 𝑦)
Theorem	kardcard2a 35932	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 35933	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 35934	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 35935	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 35936	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 35937	The kard cardinal number of a finite ordinal is finite. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ ω → (kard‘𝐴) ∈ Fin)
Theorem	kardfi 35938	The kard cardinal number of a finite set is finite. (Contributed by BTernaryTau, 3-Jul-2026.)
⊢ (𝐴 ∈ Fin → (kard‘𝐴) ∈ Fin)
Theorem	rankkardu 35939	An upper bound on the rank of a kard cardinal. (Contributed by BTernaryTau, 4-Jul-2026.)
⊢ (rank‘(kard‘𝐴)) ⊆ suc (rank‘𝐴)
Theorem	1enumkard 35940*	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 10273 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 35807 for a version that uses equinumerosity , 1enumcard 35808 for a version that uses the card function, and 1enum 36061 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 35941	Extend the definition of a class to include the second converse function.
class Cnv2
Syntax	ccnv3 35942	Extend the definition of a class to include the third converse function.
class Cnv3
Syntax	cgdlop1 35943	Extend the definition of a class to include the first Gödel operation.
class ℱ1
Syntax	cgdlop2 35944	Extend the definition of a class to include the second Gödel operation.
class ℱ2
Syntax	cgdlop3 35945	Extend the definition of a class to include the third Gödel operation.
class ℱ3
Syntax	cgdlop4 35946	Extend the definition of a class to include the fourth Gödel operation.
class ℱ4
Syntax	cgdlop5 35947	Extend the definition of a class to include the fifth Gödel operation.
class ℱ5
Syntax	cgdlop6 35948	Extend the definition of a class to include the sixth Gödel operation.
class ℱ6
Syntax	cgdlop7 35949	Extend the definition of a class to include the seventh Gödel operation.
class ℱ7
Syntax	cgdlop8 35950	Extend the definition of a class to include the eighth Gödel operation.
class ℱ8
Syntax	cgdlopc 35951	Extend the definition of a class to include the combined Gödel operations.
class ℱ
Definition	df-cnv2 35952*	Define a function that returns the second converse of a set. The second converse of a set takes all ordered triples in the set and rotates them so the last argument becomes the first argument. Based on Definition 14.1(1) of [TakeutiZaring] p. 143. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ Cnv2 = (𝑤 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑧, 𝑥⟩, 𝑦⟩ ∈ 𝑤})
Definition	df-cnv3 35953*	Define a function that returns the third converse of a set. The third converse of a set takes all ordered triples in the set and swaps the second and third arguments. Based on Definition 14.1(2) of [TakeutiZaring] p. 143. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ Cnv3 = (𝑤 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∈ 𝑤})
Definition	df-gdlop1 35954*	Define the first Gödel operation. This function takes two arguments and returns the unordered pair containing both (see df-pr 4591). Based on the first case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ1 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑥, 𝑦})
Definition	df-gdlop2 35955*	Define the second Gödel operation. This function takes two arguments and returns the intersection of the first argument with the membership relation (see df-in 4094 and df-eprel 5555). The second argument is ignored. Based on the second case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ2 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∩ E ))
Definition	df-gdlop3 35956*	Define the third Gödel operation. This function takes two arguments and returns the first argument minus the second argument (see df-dif 4050). Based on the third case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ3 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∖ 𝑦))
Definition	df-gdlop4 35957*	Define the fourth Gödel operation. This function takes two arguments and returns the first argument restricted to the second argument (see df-res 5667). Based on the fourth case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ4 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ↾ 𝑦))
Definition	df-gdlop5 35958*	Define the fifth Gödel operation. This function takes two arguments and returns the intersection of the first argument with the domain of the second argument (see df-in 4094 and df-dm 5665). Based on the fifth case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ5 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∩ dom 𝑦))
Definition	df-gdlop6 35959*	Define the sixth Gödel operation. This function takes two arguments and returns the intersection of the first argument with the converse of the second argument (see df-in 4094 and df-cnv 5663). Based on the sixth case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ6 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∩ ◡𝑦))
Definition	df-gdlop7 35960*	Define the seventh Gödel operation. This function takes two arguments and returns the intersection of the first argument with the second converse of the second argument (see df-in 4094 and df-cnv2 35952). Based on the seventh case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ7 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∩ (Cnv2‘𝑦)))
Definition	df-gdlop8 35961*	Define the eighth Gödel operation. This function takes two arguments and returns the intersection of the first argument with the third converse of the second argument (see df-in 4094 and df-cnv3 35953). Based on the eighth case of Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ8 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∩ (Cnv3‘𝑦)))
Definition	df-gdlopc 35962*	Define the combined Gödel operations. This function takes three arguments and uses the first to determine which of the eight Gödel operations df-gdlop1 35954 through df-gdlop8 35961 to apply to the second and third arguments. Based on Definition 14.2 of [TakeutiZaring] p. 144. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ ℱ = (𝑛 ∈ (9o ∖ {∅}), 𝑥 ∈ V, 𝑦 ∈ V ↦ if(𝑛 = 1o, (ℱ1‘⟨𝑥, 𝑦⟩), if(𝑛 = 2o, (ℱ2‘⟨𝑥, 𝑦⟩), if(𝑛 = 3o, (ℱ3‘⟨𝑥, 𝑦⟩), if(𝑛 = 4o, (ℱ4‘⟨𝑥, 𝑦⟩), if(𝑛 = 5o, (ℱ5‘⟨𝑥, 𝑦⟩), if(𝑛 = 6o, (ℱ6‘⟨𝑥, 𝑦⟩), if(𝑛 = 7o, (ℱ7‘⟨𝑥, 𝑦⟩), (ℱ8‘⟨𝑥, 𝑦⟩)))))))))
Theorem	gdlop1fv 35963	The value of the first Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ1‘⟨𝐴, 𝐵⟩) = {𝐴, 𝐵})
Theorem	gdlop2fv 35964	The value of the second Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ2‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ E ))
Theorem	gdlop3fv 35965	The value of the third Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ3‘⟨𝐴, 𝐵⟩) = (𝐴 ∖ 𝐵))
Theorem	gdlop4fv 35966	The value of the fourth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ4‘⟨𝐴, 𝐵⟩) = (𝐴 ↾ 𝐵))
Theorem	gdlop5fv 35967	The value of the fifth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ5‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ dom 𝐵))
Theorem	gdlop6fv 35968	The value of the sixth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ6‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ ◡𝐵))
Theorem	gdlop7fv 35969	The value of the seventh Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ7‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ (Cnv2‘𝐵)))
Theorem	gdlop8fv 35970	The value of the eighth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ8‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ (Cnv3‘𝐵)))
Theorem	gdlopcfvlem 35971	Lemma for gdlopcfv2 35973 through gdlopcfv8 35979. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    &   ⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → if(𝐶 = 𝐴, 𝐷, 𝐸) = 𝐸)
Theorem	gdlopcfv1 35972	The value of the combined Gödel operations function when its first argument is 1. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨1o, 𝐴, 𝐵⟩) = {𝐴, 𝐵})
Theorem	gdlopcfv2 35973	The value of the combined Gödel operations function when its first argument is 2. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨2o, 𝐴, 𝐵⟩) = (𝐴 ∩ E ))
Theorem	gdlopcfv3 35974	The value of the combined Gödel operations function when its first argument is 3. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨3o, 𝐴, 𝐵⟩) = (𝐴 ∖ 𝐵))
Theorem	gdlopcfv4 35975	The value of the combined Gödel operations function when its first argument is 4. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨4o, 𝐴, 𝐵⟩) = (𝐴 ↾ 𝐵))
Theorem	gdlopcfv5 35976	The value of the combined Gödel operations function when its first argument is 5. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨5o, 𝐴, 𝐵⟩) = (𝐴 ∩ dom 𝐵))
Theorem	gdlopcfv6 35977	The value of the combined Gödel operations function when its first argument is 6. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨6o, 𝐴, 𝐵⟩) = (𝐴 ∩ ◡𝐵))
Theorem	gdlopcfv7 35978	The value of the combined Gödel operations function when its first argument is 7. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨7o, 𝐴, 𝐵⟩) = (𝐴 ∩ (Cnv2‘𝐵)))
Theorem	gdlopcfv8 35979	The value of the combined Gödel operations function when its first argument is 8. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨8o, 𝐴, 𝐵⟩) = (𝐴 ∩ (Cnv3‘𝐵)))
21.6.2.8  The constructible universe
Syntax	clexo 35980	Extend the definition of a class to include the lexicographical ordering of On × On.
class LexOrd
Syntax	cr0 35981	Extend the definition of a class to include a set-like well-ordering of On × On.
class 𝑅0
Syntax	ccj0 35982	Extend the definition of a class to include the 𝑅0 order isomorphism from On × On to On.
class 𝐽0
Syntax	cj 35983	Extend the definition of a class to include an order isomorphism from (On × On) × 9o to On.
class 𝐽
Syntax	ck1 35984	Extend the definition of a class to include the first argument of the 𝐽 function.
class 𝐾1
Syntax	ck2 35985	Extend the definition of a class to include the second argument of the 𝐽 function.
class 𝐾2
Syntax	ck3 35986	Extend the definition of a class to include the third argument of the 𝐽 function.
class 𝐾3
Syntax	cfnl 35987	Extend the definition of a class to include the constructible sets function.
class 𝐹𝐿
Syntax	cl 35988	Extend the definition of a class to include the class of all constructible sets.
class 𝐿
Definition	df-lexo 35989*	Define the lexicographical ordering of On × On. Based on Definition 7.55 of [TakeutiZaring] p. 54. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ LexOrd = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}
Definition	df-r0 35990*	Define a particular set-like well-ordering of On × On using the lexicographical ordering LexOrd. Based on Definition 7.57 of [TakeutiZaring] p. 54. See r0weseon 36000 for a proof that this relation is a set-like well-order. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝑅0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) ∈ ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∨ (((1st ‘𝑥) ∪ (2nd ‘𝑥)) = ((1st ‘𝑦) ∪ (2nd ‘𝑦)) ∧ 𝑥LexOrd𝑦)))}
Definition	df-j0 35991	Define the 𝑅0 order isomorphism of On × On onto On. Equivalent to Definition 7.59 of [TakeutiZaring] p. 55 (see j0iso 36004). (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝐽0 = ◡OrdIso(𝑅0, (On × On))
Definition	df-j 35992*	Define an order isomorphism from (On × On) × 9o to On. Based on Definition 15.2 of [TakeutiZaring] p. 155. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝐽 = (𝑥 ∈ On, 𝑦 ∈ On, 𝑛 ∈ 9o ↦ ((9o ·o (𝐽0‘⟨𝑥, 𝑦⟩)) +o 𝑛))
Definition	df-k1 35993*	Define a function that takes an ordinal and returns the first argument of the ordered triple ⟨𝑥, 𝑦, 𝑛⟩ such that the ordinal equals (𝐽‘⟨𝑥, 𝑦, 𝑛⟩). Based on the first case of Definition 15.7 of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝐾1 = {⟨𝑧, 𝑥⟩ ∣ (𝑥 ∈ On ∧ ∃𝑛 ∈ 9o ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}
Definition	df-k2 35994*	Define a function that takes an ordinal and returns the second argument of the ordered triple ⟨𝑥, 𝑦, 𝑛⟩ such that the ordinal equals (𝐽‘⟨𝑥, 𝑦, 𝑛⟩). Based on the second case of Definition 15.7 of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝐾2 = {⟨𝑧, 𝑦⟩ ∣ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9o ∃𝑥 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}
Definition	df-k3 35995*	Define a function that takes an ordinal and returns the third argument of the ordered triple ⟨𝑥, 𝑦, 𝑛⟩ such that the ordinal equals (𝐽‘⟨𝑥, 𝑦, 𝑛⟩). Based on the third case of Definition 15.7 of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝐾3 = {⟨𝑧, 𝑛⟩ ∣ (𝑛 ∈ 9o ∧ ∃𝑥 ∈ On ∃𝑦 ∈ On 𝑧 = (𝐽‘⟨𝑥, 𝑦, 𝑛⟩))}
Definition	df-fnl 35996	Define a function whose range contains all and only the constructible sets. Based on Definition 15.13 of [TakeutiZaring] p. 158. (Contributed by BTernaryTau, 3-Sep-2026.)
⊢ 𝐹𝐿 = recs((𝑥 ∈ V ↦ if((𝐾3‘dom 𝑥) = ∅, ran 𝑥, (ℱ ‘⟨(𝐾3‘dom 𝑥), (𝑥‘(𝐾1‘dom 𝑥)), (𝑥‘(𝐾2‘dom 𝑥))⟩))))
Definition	df-l 35997	Define the class of all constructible sets. Definition 15.15 of [TakeutiZaring] p. 158. (Contributed by BTernaryTau, 3-Sep-2026.)
⊢ 𝐿 = (𝐹𝐿 “ On)
Theorem	lexoweon 35998	Lexicographical order is a well-ordering of On × On. Part of Proposition 7.56(1) of [TakeutiZaring] p. 54. Unlike 𝑅0, this order is not set-like, as the preimage of ⟨1o, ∅⟩ is the proper class ({∅} × On). This theorem is leweon 10117 expressed using LexOrd. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ LexOrd We (On × On)
Theorem	brlexod 35999	Condition for two ordered pairs to be related by LexOrd. (Contributed by BTernaryTau, 20-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩LexOrd⟨𝐶, 𝐷⟩ ↔ (𝐴 ∈ 𝐶 ∨ (𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷))))
Theorem	r0weseon 36000	𝑅0 is a set-like well-ordering of On × On. Part of Proposition 7.58 of [TakeutiZaring] p. 54. This theorem is r0weon 10118 expressed using 𝑅0. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ (𝑅0 We (On × On) ∧ 𝑅0 Se (On × On))