P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gdlop5fv 36001	The value of the fifth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ5‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ dom 𝐵))
Theorem	gdlop6fv 36002	The value of the sixth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ6‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ ◡𝐵))
Theorem	gdlop7fv 36003	The value of the seventh Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ7‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ (Cnv2‘𝐵)))
Theorem	gdlop8fv 36004	The value of the eighth Gödel operation. (Contributed by BTernaryTau, 18-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ8‘⟨𝐴, 𝐵⟩) = (𝐴 ∩ (Cnv3‘𝐵)))
Theorem	gdlopcfvlem 36005	Lemma for gdlopcfv2 36007 through gdlopcfv8 36013. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ 𝐴 ∈ On    &   ⊢ 𝐵 ∈ On    &   ⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → if(𝐶 = 𝐴, 𝐷, 𝐸) = 𝐸)
Theorem	gdlopcfv1 36006	The value of the combined Gödel operations function when its first argument is 1. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨1o, 𝐴, 𝐵⟩) = {𝐴, 𝐵})
Theorem	gdlopcfv2 36007	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 36008	The value of the combined Gödel operations function when its first argument is 3. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨3o, 𝐴, 𝐵⟩) = (𝐴 ∖ 𝐵))
Theorem	gdlopcfv4 36009	The value of the combined Gödel operations function when its first argument is 4. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨4o, 𝐴, 𝐵⟩) = (𝐴 ↾ 𝐵))
Theorem	gdlopcfv5 36010	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 36011	The value of the combined Gödel operations function when its first argument is 6. (Contributed by BTernaryTau, 19-Oct-2026.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (ℱ ‘⟨6o, 𝐴, 𝐵⟩) = (𝐴 ∩ ◡𝐵))
Theorem	gdlopcfv7 36012	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 36013	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 36014	Extend the definition of a class to include the lexicographical ordering of On × On.
class LexOrd
Syntax	cr0 36015	Extend the definition of a class to include a set-like well-ordering of On × On.
class 𝑅0
Syntax	ccj0 36016	Extend the definition of a class to include the 𝑅0 order isomorphism from On × On to On.
class 𝐽0
Syntax	cj 36017	Extend the definition of a class to include an order isomorphism from (On × On) × 9o to On.
class 𝐽
Syntax	ck1 36018	Extend the definition of a class to include the first argument of the 𝐽 function.
class 𝐾1
Syntax	ck2 36019	Extend the definition of a class to include the second argument of the 𝐽 function.
class 𝐾2
Syntax	ck3 36020	Extend the definition of a class to include the third argument of the 𝐽 function.
class 𝐾3
Syntax	cfnl 36021	Extend the definition of a class to include the constructible sets function.
class 𝐹𝐿
Syntax	cl 36022	Extend the definition of a class to include the class of all constructible sets.
class 𝐿
Definition	df-lexo 36023*	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 36024*	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 36034 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 36025	Define the 𝑅0 order isomorphism of On × On onto On. Equivalent to Definition 7.59 of [TakeutiZaring] p. 55 (see j0iso 36038). (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝐽0 = ◡OrdIso(𝑅0, (On × On))
Definition	df-j 36026*	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 36027*	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 36028*	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 36029*	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 36030	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 36031	Define the class of all constructible sets. Definition 15.15 of [TakeutiZaring] p. 158. (Contributed by BTernaryTau, 3-Sep-2026.)
⊢ 𝐿 = (𝐹𝐿 “ On)
Theorem	lexoweon 36032	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 10127 expressed using LexOrd. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ LexOrd We (On × On)
Theorem	brlexod 36033	Condition for two ordered pairs to be related by LexOrd. (Contributed by BTernaryTau, 20-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩LexOrd⟨𝐶, 𝐷⟩ ↔ (𝐴 ∈ 𝐶 ∨ (𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷))))
Theorem	r0weseon 36034	𝑅0 is a set-like well-ordering of On × On. Part of Proposition 7.58 of [TakeutiZaring] p. 54. This theorem is r0weon 10128 expressed using 𝑅0. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ (𝑅0 We (On × On) ∧ 𝑅0 Se (On × On))
Theorem	brr0d 36035	Condition for two ordered pairs to be related by 𝑅0. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑅0⟨𝐶, 𝐷⟩ ↔ ((𝐴 ∪ 𝐵) ∈ (𝐶 ∪ 𝐷) ∨ ((𝐴 ∪ 𝐵) = (𝐶 ∪ 𝐷) ∧ ⟨𝐴, 𝐵⟩LexOrd⟨𝐶, 𝐷⟩))))
Theorem	dmr0ss 36036	The domain of 𝑅0 is a subset of On × On. (Contributed by BTernaryTau, 22-Sep-2026.)
⊢ dom 𝑅0 ⊆ (On × On)
Theorem	r0maxss 36037	If two ordered pairs are related by 𝑅0, then the maximum of the first pair is less than or equal to the maximum of the second pair. (The union of two ordinals is proven to be their maximum in ordunmax 35826.) (Contributed by BTernaryTau, 22-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩𝑅0⟨𝐶, 𝐷⟩)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ (𝐶 ∪ 𝐷))
Theorem	j0iso 36038	𝐽0 is the 𝑅0 order isomorphism of On × On onto On. Definition 7.59 of [TakeutiZaring] p. 55. This isomorphism is unique by weisoeq 7394 and r0weseon 36034. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ 𝐽0 Isom 𝑅0, E ((On × On), On)
Theorem	j00smo 36039	𝐽0 is strictly monotonic over its second argument when its first argument is zero. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ 𝐹 = (𝑥 ∈ On ↦ (𝐽0‘⟨∅, 𝑥⟩))    ⇒   ⊢ Smo 𝐹
Theorem	maxssj0 36040	The value of 𝐽0 is at least the maximum of its two arguments. Proposition 15.1(1) of [TakeutiZaring] p. 154. (Contributed by BTernaryTau, 22-Sep-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ⊆ (𝐽0‘⟨𝐴, 𝐵⟩))
Theorem	j0ltalephlem 36041	Lemma for j0ltaleph 36042. (Contributed by BTernaryTau, 25-Sep-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐽0‘⟨𝐴, 𝐵⟩) ≼ (suc (𝐴 ∪ 𝐵) × suc (𝐴 ∪ 𝐵)))
Theorem	j0ltaleph 36042	The value of 𝐽0 is less than an aleph if its two arguments are less than that aleph. Proposition 15.1(2) of [TakeutiZaring] p. 154. (Contributed by BTernaryTau, 25-Sep-2026.)
⊢ ((𝐴 ∈ (ℵ‘𝐶) ∧ 𝐵 ∈ (ℵ‘𝐶)) → (𝐽0‘⟨𝐴, 𝐵⟩) ∈ (ℵ‘𝐶))
Theorem	dfj2 36043	Alternate definition of 𝐽 as a one-argument function. (Contributed by BTernaryTau, 4-Oct-2026.)
⊢ 𝐽 = (𝑥 ∈ ((On × On) × 9o) ↦ ((9o ·o (𝐽0‘(1st ‘𝑥))) +o (2nd ‘𝑥)))
Theorem	jf1 36044	𝐽 is a one-to-one function. Part of Proposition 15.3 of [TakeutiZaring] p. 155. (Contributed by BTernaryTau, 6-Oct-2026.)
⊢ 𝐽:((On × On) × 9o)⟶1-1On
Theorem	jf1o 36045	𝐽 is a bijection from ((On × On) × 9o) to On. Proposition 15.3 of [TakeutiZaring] p. 155. (Contributed by BTernaryTau, 6-Oct-2026.)
⊢ 𝐽:((On × On) × 9o)⟶1-1ontoOn
Theorem	dfk12 36046	Alternate definition of 𝐾1 using maps-to notation. (Contributed by BTernaryTau, 9-Oct-2026.)
⊢ 𝐾1 = (𝑥 ∈ On ↦ (1st ‘(1st ‘(◡𝐽‘𝑥))))
Theorem	dfk22 36047	Alternate definition of 𝐾2 using maps-to notation. (Contributed by BTernaryTau, 10-Oct-2026.)
⊢ 𝐾2 = (𝑥 ∈ On ↦ (2nd ‘(1st ‘(◡𝐽‘𝑥))))
Theorem	dfk32 36048	Alternate definition of 𝐾3 using maps-to notation. (Contributed by BTernaryTau, 10-Oct-2026.)
⊢ 𝐾3 = (𝑥 ∈ On ↦ (2nd ‘(◡𝐽‘𝑥)))
Theorem	k1on 36049	Values of the 𝐾1 function are ordinals. (Contributed by BTernaryTau, 11-Oct-2026.)
⊢ (𝐾1‘𝐴) ∈ On
Theorem	k2on 36050	Values of the 𝐾2 function are ordinals. (Contributed by BTernaryTau, 11-Oct-2026.)
⊢ (𝐾2‘𝐴) ∈ On
Theorem	k39o 36051	Values of the 𝐾3 function are ordinals less than 9. (Contributed by BTernaryTau, 11-Oct-2026.)
⊢ (𝐾3‘𝐴) ∈ 9o
Theorem	jk1k2k3 36052	Identity law for the 𝐽 function. Proposition 15.8 of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 11-Oct-2026.)
⊢ (𝐴 ∈ On → 𝐴 = (𝐽‘⟨(𝐾1‘𝐴), (𝐾2‘𝐴), (𝐾3‘𝐴)⟩))
Theorem	j0le 36053	An upper bound on the value of 𝐽0. (Contributed by BTernaryTau, 12-Oct-2026.)
⊢ (𝐴 ∈ On → (𝐽0‘⟨(𝐾1‘𝐴), (𝐾2‘𝐴)⟩) ⊆ 𝐴)
Theorem	k3n0j0lt 36054	A strict upper bound on the value of 𝐽0 for nonzero values of 𝐾3. (Contributed by BTernaryTau, 12-Oct-2026.)
⊢ ((𝐴 ∈ On ∧ ∅ ∈ (𝐾3‘𝐴)) → (𝐽0‘⟨(𝐾1‘𝐴), (𝐾2‘𝐴)⟩) ∈ 𝐴)
Theorem	k1le 36055	The value of 𝐾1 is bounded by its argument. Part of Proposition 15.10(1) of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 12-Oct-2026.)
⊢ (𝐴 ∈ On → (𝐾1‘𝐴) ⊆ 𝐴)
Theorem	k2le 36056	The value of 𝐾2 is bounded by its argument. Part of Proposition 15.10(1) of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 12-Oct-2026.)
⊢ (𝐴 ∈ On → (𝐾2‘𝐴) ⊆ 𝐴)
Theorem	k3n0k1lt 36057	The value of 𝐾1 is strictly bounded by its argument when the value of 𝐾3 is nonzero. Part of Proposition 15.10(2) of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 12-Oct-2026.)
⊢ ((𝐴 ∈ On ∧ ∅ ∈ (𝐾3‘𝐴)) → (𝐾1‘𝐴) ∈ 𝐴)
Theorem	k3n0k2lt 36058	The value of 𝐾2 is strictly bounded by its argument when the value of 𝐾3 is nonzero. Part of Proposition 15.10(2) of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 12-Oct-2026.)
⊢ ((𝐴 ∈ On ∧ ∅ ∈ (𝐾3‘𝐴)) → (𝐾2‘𝐴) ∈ 𝐴)
Theorem	jltalephlem 36059	Lemma for jltaleph 36060. (Contributed by BTernaryTau, 16-Oct-2026.)
⊢ ((𝐶 ∈ 9o ∧ ω ≼ (𝐽0‘⟨𝐴, 𝐵⟩)) → ((9o ·o (𝐽0‘⟨𝐴, 𝐵⟩)) +o 𝐶) ≈ (𝐽0‘⟨𝐴, 𝐵⟩))
Theorem	jltaleph 36060	The value of 𝐽 is less than an aleph if its first two arguments are less than that aleph. Proposition 15.11 of [TakeutiZaring] p. 156. (Contributed by BTernaryTau, 16-Oct-2026.)
⊢ ((𝐴 ∈ (ℵ‘𝐷) ∧ 𝐵 ∈ (ℵ‘𝐷) ∧ 𝐶 ∈ 9o) → (𝐽‘⟨𝐴, 𝐵, 𝐶⟩) ∈ (ℵ‘𝐷))
Theorem	fnlfvk30 36061	The value of 𝐹𝐿 when the value of 𝐾3 is zero. Part of Proposition 15.14 of [TakeutiZaring] p. 158. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ ((𝐴 ∈ On ∧ (𝐾3‘𝐴) = ∅) → (𝐹𝐿‘𝐴) = (𝐹𝐿 “ 𝐴))
Theorem	fnlfvk3n0 36062	The value of 𝐹𝐿 when the value of 𝐾3 is nonzero. Part of Proposition 15.14 of [TakeutiZaring] p. 158. (Contributed by BTernaryTau, 17-Oct-2026.)
⊢ ((𝐴 ∈ On ∧ (𝐾3‘𝐴) ≠ ∅) → (𝐹𝐿‘𝐴) = (ℱ ‘⟨(𝐾3‘𝐴), (𝐹𝐿‘(𝐾1‘𝐴)), (𝐹𝐿‘(𝐾2‘𝐴))⟩))
21.6.2.9  Global choice
Theorem	gblacfnacd 36063*	If 𝐺 is a global choice function, then the Axiom of Choice (in the form of the right-hand side of dfac4 10238) holds. Note that 𝐺 must be a proper class by fndmexb 7950. This means we cannot show that the existence of a class that behaves as a global choice function is sufficient because we only have existential quantifiers for sets, not (proper) classes. However, if a class variant of exlimiv 1965 were available, then it could be used alongside the closed form of this theorem to prove that result. (Contributed by BTernaryTau, 12-Dec-2024.)
⊢ (𝜑 → 𝐺 Fn V)    &   ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    ⇒   ⊢ (𝜑 → ∀𝑥∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑧 ∈ 𝑥 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
Theorem	gblacfnac2d 36064*	If 𝐺 is a global choice function, then the Axiom of Choice holds. This is gblacfnacd 36063 expressed using CHOICE. (Contributed by BTernaryTau, 25-Sep-2026.)
⊢ (𝜑 → 𝐺 Fn V)    &   ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    ⇒   ⊢ (𝜑 → CHOICE)
Theorem	onvf1odlem1 36065*	Lemma for onvf1od 36069. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴)
Theorem	onvf1odlem2 36066*	Lemma for onvf1od 36069. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ 𝐴))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑉 → 𝑁 ∈ ((𝑅1‘𝑀) ∖ 𝐴)))
Theorem	onvf1odlem3 36067*	Lemma for onvf1od 36069. The value of 𝐹 at an ordinal 𝐴. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤))    &   ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁))    &   ⊢ 𝐵 = ∩ {𝑢 ∈ On ∣ ∃𝑣 ∈ (𝑅1‘𝑢) ¬ 𝑣 ∈ (𝐹 “ 𝐴)}    &   ⊢ 𝐶 = (𝐺‘((𝑅1‘𝐵) ∖ (𝐹 “ 𝐴)))    ⇒   ⊢ (𝐴 ∈ On → (𝐹‘𝐴) = 𝐶)
Theorem	onvf1odlem4 36068*	Lemma for onvf1od 36069. If the range of 𝐹 does not exist, then it must equal the universe. (Contributed by BTernaryTau, 4-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤))    &   ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁))    &   ⊢ 𝐵 = ∩ {𝑢 ∈ On ∣ ∃𝑣 ∈ (𝑅1‘𝑢) ¬ 𝑣 ∈ (𝐹 “ 𝑡)}    &   ⊢ 𝐶 = (𝐺‘((𝑅1‘𝐵) ∖ (𝐹 “ 𝑡)))    ⇒   ⊢ (𝜑 → (¬ ran 𝐹 ∈ V → ran 𝐹 = V))
Theorem	onvf1od 36069*	If 𝐺 is a global choice function, then 𝐹 is a bijection from the ordinals to the universe. This is the ZFC version of (1 → 2) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 5-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ ran 𝑤}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ ran 𝑤))    &   ⊢ 𝐹 = recs((𝑤 ∈ V ↦ 𝑁))    ⇒   ⊢ (𝜑 → 𝐹:On⟶1-1ontoV)
Theorem	vonf1wev 36070*	If 𝐹 maps the universe one-to-one into the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (6 → 3) which can be used in place of (7 → 3) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝑋∃𝐹𝐹:𝑋⟶1-1On, but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. (Contributed by BTernaryTau, 11-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V⟶1-1On → 𝑅 We V)
Theorem	vonf1owev 36071*	If 𝐹 is a bijection from the universe to the ordinals, then 𝑅 well-orders the universe. This is the ZFC version of (2 → 3) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 6-Dec-2025.) (Proof shortened by BTernaryTau, 11-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V⟶1-1ontoOn → 𝑅 We V)
Theorem	vonf1owevOLD 36072*	Obsolete version of vonf1owev 36071 as of 11-Jun-2026. (Contributed by BTernaryTau, 6-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V⟶1-1ontoOn → 𝑅 We V)
Theorem	wevgblacfn 36073*	If 𝑅 is a well-ordering of the universe, then 𝐺 is a global choice function. Here 𝐺 maps each set 𝑧 to its minimal element with respect to 𝑅 (except when 𝑧 is the empty set, in which case it is mapped to the empty set, though this is only done for convenience). This is the ZFC version of (3 → 1) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 29-Jun-2025.)
⊢ 𝐺 = (𝑧 ∈ V ↦ ∪ {𝑦 ∈ 𝑧 ∣ ∀𝑥 ∈ 𝑧 ¬ 𝑥𝑅𝑦})    ⇒   ⊢ (𝑅 We V → (𝐺 Fn V ∧ ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧)))
Theorem	vonf1osev 36074*	If 𝐹 is a bijection from the universe to the ordinals, then 𝑅 is a set-like well-ordering of the universe. This is the ZFC version of (2 → 4) which can be used in place of (3 → 4) in https://tinyurl.com/hamkins-gblac. This proof takes advantage of the fact that the well-order constructed in (2 → 3) is also set-like. (Contributed by BTernaryTau, 8-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V⟶1-1ontoOn → (𝑅 We V ∧ 𝑅 Se V))
Theorem	wevsev 36075*	If 𝑅 is a well-ordering of the universe, then 𝑆 is a set-like well-ordering of the universe. This is the ZFC version of (3 → 4) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 18-Sep-2026.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((rank‘𝑥) ∈ (rank‘𝑦) ∨ ((rank‘𝑥) = (rank‘𝑦) ∧ 𝑥𝑅𝑦))}    ⇒   ⊢ (𝑅 We V → (𝑆 We V ∧ 𝑆 Se V))
Theorem	wevonprcf1o 36076	If 𝑅 is a set-like well-ordering of the universe and 𝐴 is a proper class, then 𝐹 is a bijection from the ordinals to 𝐴. This is the ZFC version of (4 → 5) in https://tinyurl.com/hamkins-gblac. (Contributed by BTernaryTau, 9-Jun-2026.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We V ∧ 𝑅 Se V ∧ ¬ 𝐴 ∈ V) → 𝐹:On⟶1-1onto𝐴)
Theorem	vonf1oonf1 36077	If 𝐹 is a bijection from the universe to the ordinals, then 𝐻 maps 𝐴 one-to-one into the ordinals. This is the ZFC version of (5 → 6) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:𝑋⟶1-1ontoOn), but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. This theorem can also be viewed as (2 → 6). (Contributed by BTernaryTau, 10-Jun-2026.)
⊢ 𝐻 = (𝐹 ↾ 𝐴)    ⇒   ⊢ (𝐹:V⟶1-1ontoOn → 𝐻:𝐴⟶1-1On)
Theorem	vonf1onprcf1ac 36078	If 𝐹 maps the universe one-to-one into the ordinals and 𝐴 is a proper class, then 𝐼 maps the ordinals one-to-one into 𝐴 and the Axiom of Choice holds. This is the ZFC version of (6 → 7) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the first hypothesis would be something like 𝜑 → ∀𝑋∃𝐹𝐹:𝑋⟶1-1On, but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. (Contributed by BTernaryTau, 22-Jun-2026.)
⊢ (𝜑 → 𝐹:V⟶1-1On)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ V)    &   ⊢ 𝐼 = (◡(𝐹 ↾ 𝐴) ∘ 𝐻)    &   ⊢ 𝐻 = OrdIso( E , (𝐹 “ 𝐴))    ⇒   ⊢ (𝜑 → (𝐼:On⟶1-1𝐴 ∧ CHOICE))
Theorem	onprcf1acwevdlem1 36079*	Lemma for onprcf1acwevd 36081 and prconf1acwevd 36082. (Contributed by BTernaryTau, 10-Sep-2026.)
⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    ⇒   ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ∈ V)
Theorem	onprcf1acwevdlem2 36080*	Lemma for onprcf1acwevd 36081 and prconf1acwevd 36082. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ 𝑅 = {⟨𝑦, 𝑧⟩ ∣ ((rank‘𝑦) ∈ (rank‘𝑧) ∨ ((rank‘𝑦) = (rank‘𝑧) ∧ 𝑦𝑆𝑧))}    &   ⊢ 𝑆 = (𝐹‘∩ {𝑤 ∈ On ∣ (𝐹‘𝑤) We (𝑅1‘suc (rank‘𝑦))})    &   ⊢ ((𝜑 ∧ 𝑢 ∈ On) → ∃𝑤 ∈ On (𝐹‘𝑤) We (𝑅1‘𝑢))    ⇒   ⊢ (𝜑 → 𝑅 We V)
Theorem	onprcf1acwevd 36081*	If 𝐹 maps the ordinals one-to-one into the proper class 𝑊 and the Axiom of Choice holds, then 𝑅 well-orders the universe. This is the ZFC version of (7 → 3) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the first hypothesis would be something like (𝜑 → ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:On⟶1-1𝑋)), but since we cannot quantify over classes, we instead consider only the case 𝑋 = 𝑊 which is sufficient for this proof. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ (𝜑 → (¬ 𝑊 ∈ V → 𝐹:On⟶1-1𝑊))    &   ⊢ (𝜑 → CHOICE)    &   ⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    &   ⊢ 𝑅 = {⟨𝑦, 𝑧⟩ ∣ ((rank‘𝑦) ∈ (rank‘𝑧) ∨ ((rank‘𝑦) = (rank‘𝑧) ∧ 𝑦𝑆𝑧))}    &   ⊢ 𝑆 = (𝐹‘∩ {𝑤 ∈ On ∣ (𝐹‘𝑤) We (𝑅1‘suc (rank‘𝑦))})    ⇒   ⊢ (𝜑 → 𝑅 We V)
Theorem	prconf1acwevd 36082*	If 𝐹 maps the proper class 𝑊 one-to-one into the ordinals and the Axiom of Choice holds, then 𝑅 well-orders the universe. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ (𝜑 → (¬ 𝑊 ∈ V → 𝐹:𝑊⟶1-1On))    &   ⊢ (𝜑 → CHOICE)    &   ⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    &   ⊢ 𝑅 = {⟨𝑦, 𝑧⟩ ∣ ((rank‘𝑦) ∈ (rank‘𝑧) ∨ ((rank‘𝑦) = (rank‘𝑧) ∧ 𝑦𝑆𝑧))}    &   ⊢ 𝑆 = (◡𝐹‘∩ {𝑤 ∈ On ∣ (◡𝐹‘𝑤) We (𝑅1‘suc (rank‘𝑦))})    ⇒   ⊢ (𝜑 → 𝑅 We V)
Theorem	vonf1oonfo 36083*	If 𝐹 is a bijection from the ordinals to the universe and 𝐴 is non-empty, then 𝐻 maps the ordinals onto 𝐴. This is the ZFC version of (5 → 8) in https://tinyurl.com/hamkins-gblac, though it neglects to specify that 𝐴 must be non-empty. Note that in NBG set theory the antecedent would be something like ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:𝑋⟶1-1ontoOn), but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. This theorem can also be viewed as (2 → 8). (Contributed by BTernaryTau, 11-Jun-2026.)
⊢ 𝐻 = (𝑥 ∈ On ↦ if((𝐹‘𝑥) ∈ 𝐴, (𝐹‘𝑥), 𝐷))    &   ⊢ 𝐷 = (𝐹‘∩ {𝑦 ∈ On ∣ (𝐹‘𝑦) ∈ 𝐴})    ⇒   ⊢ ((𝐹:On⟶1-1ontoV ∧ 𝐴 ≠ ∅) → 𝐻:On⟶onto𝐴)
Theorem	onvfowev 36084*	If 𝐹 maps the ordinals onto the universe, then 𝑅 well-orders the universe. This is the ZFC version of (8 → 3) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝑋(𝑋 ≠ ∅ → ∃𝐹𝐹:On⟶onto𝑋), but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. (Contributed by BTernaryTau, 12-Jun-2026.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐻‘𝑥) ∈ (𝐻‘𝑦)}    &   ⊢ 𝐻 = (𝑧 ∈ V ↦ ∩ (◡𝐹 “ {𝑧}))    ⇒   ⊢ (𝐹:On⟶ontoV → 𝑅 We V)
Theorem	onf1onf1or 36085	If 𝐹 maps 𝐴 one-to-one into the ordinals, then either 𝐴 can be mapped one-to-one into the ordinals (by 𝐹), or the ordinals can be mapped one-to-one into 𝐴. This is the ZFC version of (6 → 9) in https://tinyurl.com/hamkins-gblac. The proof is trivial but is included for completeness. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ (𝐹:𝐴⟶1-1On → (𝐹:𝐴⟶1-1On ∨ 𝐻:On⟶1-1𝐴))
Theorem	onf1oracwevd 36086*	If 𝐹 maps the proper class 𝑊 one-to-one into the ordinals or 𝐻 maps the ordinals one-to-one into the proper class 𝑊, and if every set can either be mapped one-to-one into the ordinals or have the ordinals mapped one-to-one into it, then 𝑅 well-orders the universe. This is the ZFC version of (9 → 3) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the first two hypotheses would be replaced by something like (𝜑 → ∀𝑋(∃𝐹𝐹:𝑋⟶1-1On ∨ ∃𝐻𝐻:On⟶1-1𝑋)). However, we cannot quantify over classes, so we split this into the case where 𝑋 is a set and the case where 𝑋 is the proper class 𝑊 which together are sufficient for this proof. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ (𝜑 → (𝐹:𝑊⟶1-1On ∨ 𝐻:On⟶1-1𝑊))    &   ⊢ (𝜑 → ∀𝑣(∃𝑓 𝑓:𝑣⟶1-1On ∨ ∃ℎ ℎ:On⟶1-1𝑣))    &   ⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    &   ⊢ 𝑅 = {⟨𝑦, 𝑧⟩ ∣ ((rank‘𝑦) ∈ (rank‘𝑧) ∨ ((rank‘𝑦) = (rank‘𝑧) ∧ 𝑦𝐴𝑧))}    &   ⊢ 𝐴 = (𝐼‘∩ {𝑤 ∈ On ∣ (𝐼‘𝑤) We (𝑅1‘suc (rank‘𝑦))})    &   ⊢ 𝐼 = if(𝐹:𝑊⟶1-1On, ◡𝐹, 𝐻)    ⇒   ⊢ (𝜑 → 𝑅 We V)
Theorem	onprcf1of1orad 36087	If 𝐹 is a bijection from the ordinals to the universe and 𝐻 is a bijection from the ordinals to the proper class 𝐵, then 𝐼 maps 𝐴 one-to-one into 𝐵. This is the ZFC version of (5 → 10) in https://tinyurl.com/hamkins-gblac in the case where one of the classes is a proper class. See onprcf1of1orbd 36088 for the case where neither class is a proper class, and see onprcf1of1ord 36089 for a theorem that covers both cases. Note that in NBG set theory the first two hypotheses would be replaced by something like (𝜑 → ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:On⟶1-1onto𝑋)). However, we cannot quantify over classes, so we split this into the case where 𝑋 is the universe and the case where 𝑋 is an arbitrary proper class 𝐵 which together are sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026.)
⊢ (𝜑 → 𝐹:On⟶1-1ontoV)    &   ⊢ (𝜑 → (¬ 𝐵 ∈ V → 𝐻:On⟶1-1onto𝐵))    &   ⊢ (𝜑 → ¬ 𝐵 ∈ V)    &   ⊢ 𝐼 = (𝐻 ∘ (◡𝐹 ↾ 𝐴))    ⇒   ⊢ (𝜑 → 𝐼:𝐴⟶1-1𝐵)
Theorem	onprcf1of1orbd 36088*	If 𝐹 is a bijection from the ordinals to the universe and both 𝐴 and 𝐵 are sets, then either 𝐴 can be mapped one-to-one into 𝐵 or 𝐵 can be mapped one-to-one into 𝐴. This is the ZFC version of (5 → 10) in https://tinyurl.com/hamkins-gblac in the case where neither class is a proper class. See onprcf1of1orad 36087 for the case where one of the classes is a proper class, and see onprcf1of1ord 36089 for a theorem that covers both cases. Note that in NBG set theory the first hypothesis would be replaced by something like (𝜑 → ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:On⟶1-1onto𝑋)), but since we cannot quantify over classes, we instead consider only the case 𝑋 = V which is sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026.)
⊢ (𝜑 → 𝐹:On⟶1-1ontoV)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (∃𝑓 𝑓:𝐴⟶1-1𝐵 ∨ ∃ℎ ℎ:𝐵⟶1-1𝐴))
Theorem	onprcf1of1ord 36089*	If 𝐹 is a bijection from the ordinals to the universe, 𝐻 is a bijection from the ordinals to 𝐴 if 𝐴 is a proper class, and 𝐼 is a bijection from the ordinals to 𝐵 if 𝐵 is a proper class, then 𝐽 either maps 𝐴 one-to-one into 𝐵 or maps 𝐵 one-to-one into 𝐴. This is the ZFC version of (5 → 10) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the first three hypotheses would be replaced by something like (𝜑 → ∀𝑋(¬ 𝑋 ∈ V → ∃𝐹𝐹:On⟶1-1onto𝑋)). However, we cannot quantify over classes, so we split this into the case where 𝑋 is the universe, the case where 𝑋 is an arbitrary proper class 𝐴, and the case where 𝑋 is an arbitrary proper class 𝐵, which together are sufficient for this proof. (Contributed by BTernaryTau, 17-Sep-2026.)
⊢ (𝜑 → 𝐹:On⟶1-1ontoV)    &   ⊢ (𝜑 → (¬ 𝐴 ∈ V → 𝐻:On⟶1-1onto𝐴))    &   ⊢ (𝜑 → (¬ 𝐵 ∈ V → 𝐼:On⟶1-1onto𝐵))    &   ⊢ 𝐽 = if(𝐴 ∈ V, if(𝐵 ∈ V, 𝐾, (𝐼 ∘ (◡𝐹 ↾ 𝐴))), (𝐻 ∘ (◡𝐹 ↾ 𝐵)))    &   ⊢ 𝐾 = (𝐹‘∩ {𝑥 ∈ On ∣ ((𝐹‘𝑥):𝐴⟶1-1𝐵 ∨ (𝐹‘𝑥):𝐵⟶1-1𝐴)})    ⇒   ⊢ (𝜑 → (𝐽:𝐴⟶1-1𝐵 ∨ 𝐽:𝐵⟶1-1𝐴))
Theorem	f1oronf1or 36090	If 𝐹 maps 𝐴 one-to-one into the ordinals or 𝐻 maps the ordinals one-to-one into 𝐴, then either 𝐴 can be mapped one-to-one into the ordinals (by 𝐹), or the ordinals can be mapped one-to-one into 𝐴 (by 𝐻). This is the ZFC version of (10 → 9) in https://tinyurl.com/hamkins-gblac. Note that in NBG set theory the antecedent would be something like ∀𝐴∀𝑋(∃𝐹𝐹:𝐴⟶1-1𝑋 ∨ ∃𝐻𝐻:𝑋⟶1-1𝐴), but since we cannot quantify over classes, we instead consider only the case 𝑋 = On which is sufficient for this proof. The proof is trivial but is included for completeness. (Contributed by BTernaryTau, 17-Sep-2026.)
⊢ ((𝐹:𝐴⟶1-1On ∨ 𝐻:On⟶1-1𝐴) → (𝐹:𝐴⟶1-1On ∨ 𝐻:On⟶1-1𝐴))
21.6.3  Real and complex numbers
Theorem	zltp1ne 36091	Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nnltp1ne 36092	Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nn0ltp1ne 36093	Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	fisshasheq 36094	A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵)
Theorem	1enum 36095*	The Fundamental Theorem of Enumeration. According to Doron Zeilberger (in https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf), this theorem was independently discovered by several anonymous cave-dwellers. Zeilberger also states that "While this formula is still useful after all these years, enumerating specific finite sets is no longer considered mathematics. A genuine mathematical fact has to incorporate infinitely many facts". Fortunately, theorems in Metamath are actually theorem schemes that correspond to an infinite number of object-language theorems, so this concern does not apply to us. See 1enumen 35841 for a version that uses equinumerosity , 1enumcard 35842 for a version that uses the card function, and 1enumkard 35974 for a version that uses the kard function. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ Fin → (♯‘𝐴) = Σ𝑎 ∈ 𝐴 1)
21.6.4  Graph theory
Theorem	cplgredgex 36096*	Any two (distinct) vertices in a complete graph are connected to each other by at least one edge. (Contributed by BTernaryTau, 2-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒))
Theorem	cusgredgex 36097	Any two (distinct) vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	cusgredgex2 36098	Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	revwlkb 36099	Two words represent a walk if and only if their reverses also represent a walk. (Contributed by BTernaryTau, 4-Dec-2023.)
⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈) → (𝐹(Walks‘𝐺)𝑃 ↔ (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)))
Theorem	usgrgt2cycl 36100	A non-trivial cycle in a simple graph has a length greater than 2. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝐹))