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
Syntax	cgdlop3 35901	Extend the definition of a class to include the third Gödel operation.
class ℱ3
Syntax	cgdlop4 35902	Extend the definition of a class to include the fourth Gödel operation.
class ℱ4
Syntax	cgdlop5 35903	Extend the definition of a class to include the fifth Gödel operation.
class ℱ5
Syntax	cgdlop6 35904	Extend the definition of a class to include the sixth Gödel operation.
class ℱ6
Syntax	cgdlop7 35905	Extend the definition of a class to include the seventh Gödel operation.
class ℱ7
Syntax	cgdlop8 35906	Extend the definition of a class to include the eighth Gödel operation.
class ℱ8
Syntax	cgdlopc 35907	Extend the definition of a class to include the combined Gödel operations.
class ℱ
Definition	df-cnv2 35908*	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 35909*	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 35910*	Define the first Gödel operation. This function takes two arguments and returns the unordered pair containing both (see df-pr 4587). 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 35911*	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 4091 and df-eprel 5550). 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 35912*	Define the third Gödel operation. This function takes two arguments and returns the first argument minus the second argument (see df-dif 4047). 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 35913*	Define the fourth Gödel operation. This function takes two arguments and returns the first argument restricted to the second argument (see df-res 5662). 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 35914*	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 4091 and df-dm 5660). 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 35915*	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 4091 and df-cnv 5658). 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 35916*	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 4091 and df-cnv2 35908). 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 35917*	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 4091 and df-cnv3 35909). 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 35918*	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 35910 through df-gdlop8 35917 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‘⟨𝑥, 𝑦⟩)))))))))
21.6.2.8  The constructible universe
Syntax	clexo 35919	Extend the definition of a class to include the lexicographical ordering of On × On.
class LexOrd
Syntax	cr0 35920	Extend the definition of a class to include a set-like well-ordering of On × On.
class 𝑅0
Syntax	ccj0 35921	Extend the definition of a class to include the 𝑅0 order isomorphism from On × On to On.
class 𝐽0
Syntax	cj 35922	Extend the definition of a class to include an order isomorphism from (On × On) × 9o to On.
class 𝐽
Syntax	ck1 35923	Extend the definition of a class to include the first argument of the 𝐽 function.
class 𝐾1
Syntax	ck2 35924	Extend the definition of a class to include the second argument of the 𝐽 function.
class 𝐾2
Syntax	ck3 35925	Extend the definition of a class to include the third argument of the 𝐽 function.
class 𝐾3
Syntax	cfnl 35926	Extend the definition of a class to include the constructible sets function.
class 𝐹𝐿
Syntax	cl 35927	Extend the definition of a class to include the class of all constructible sets.
class 𝐿
Definition	df-lexo 35928*	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 35929*	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 35939 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 35930	Define the 𝑅0 order isomorphism of On × On onto On. Equivalent to Definition 7.59 of [TakeutiZaring] p. 55 (see j0iso 35943). (Contributed by BTernaryTau, 2-Sep-2026.)
⊢ 𝐽0 = ◡OrdIso(𝑅0, (On × On))
Definition	df-j 35931*	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 35932*	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 35933*	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 35934*	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 35935	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 35936	Define the class of all constructible sets. Definition 15.15 of [TakeutiZaring] p. 158. (Contributed by BTernaryTau, 3-Sep-2026.)
⊢ 𝐿 = (𝐹𝐿 “ On)
Theorem	lexoweon 35937	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 10093 expressed using LexOrd. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ LexOrd We (On × On)
Theorem	brlexod 35938	Condition for two ordered pairs to be related by LexOrd. (Contributed by BTernaryTau, 20-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩LexOrd⟨𝐶, 𝐷⟩ ↔ (𝐴 ∈ 𝐶 ∨ (𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷))))
Theorem	r0weseon 35939	𝑅0 is a set-like well-ordering of On × On. Part of Proposition 7.58 of [TakeutiZaring] p. 54. This theorem is r0weon 10094 expressed using 𝑅0. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ (𝑅0 We (On × On) ∧ 𝑅0 Se (On × On))
Theorem	brr0d 35940	Condition for two ordered pairs to be related by 𝑅0. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑅0⟨𝐶, 𝐷⟩ ↔ ((𝐴 ∪ 𝐵) ∈ (𝐶 ∪ 𝐷) ∨ ((𝐴 ∪ 𝐵) = (𝐶 ∪ 𝐷) ∧ ⟨𝐴, 𝐵⟩LexOrd⟨𝐶, 𝐷⟩))))
Theorem	dmr0ss 35941	The domain of 𝑅0 is a subset of On × On. (Contributed by BTernaryTau, 22-Sep-2026.)
⊢ dom 𝑅0 ⊆ (On × On)
Theorem	r0maxss 35942	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 35765.) (Contributed by BTernaryTau, 22-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐶 ∈ On)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩𝑅0⟨𝐶, 𝐷⟩)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ (𝐶 ∪ 𝐷))
Theorem	j0iso 35943	𝐽0 is the 𝑅0 order isomorphism of On × On onto On. Definition 7.59 of [TakeutiZaring] p. 55. This isomorphism is unique by weisoeq 7365 and r0weseon 35939. (Contributed by BTernaryTau, 19-Sep-2026.)
⊢ 𝐽0 Isom 𝑅0, E ((On × On), On)
Theorem	j00smo 35944	𝐽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 35945	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 35946	Lemma for j0ltaleph 35947. (Contributed by BTernaryTau, 25-Sep-2026.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐽0‘⟨𝐴, 𝐵⟩) ≼ (suc (𝐴 ∪ 𝐵) × suc (𝐴 ∪ 𝐵)))
Theorem	j0ltaleph 35947	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‘⟨𝐴, 𝐵⟩) ∈ (ℵ‘𝐶))
21.6.2.9  Global choice
Theorem	gblacfnacd 35948*	If 𝐺 is a global choice function, then the Axiom of Choice (in the form of the right-hand side of dfac4 10204) holds. Note that 𝐺 must be a proper class by fndmexb 7918. 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 1962 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 35949*	If 𝐺 is a global choice function, then the Axiom of Choice holds. This is gblacfnacd 35948 expressed using CHOICE. (Contributed by BTernaryTau, 25-Sep-2026.)
⊢ (𝜑 → 𝐺 Fn V)    &   ⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    ⇒   ⊢ (𝜑 → CHOICE)
Theorem	onvf1odlem1 35950*	Lemma for onvf1od 35954. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴)
Theorem	onvf1odlem2 35951*	Lemma for onvf1od 35954. (Contributed by BTernaryTau, 2-Dec-2025.)
⊢ (𝜑 → ∀𝑧(𝑧 ≠ ∅ → (𝐺‘𝑧) ∈ 𝑧))    &   ⊢ 𝑀 = ∩ {𝑥 ∈ On ∣ ∃𝑦 ∈ (𝑅1‘𝑥) ¬ 𝑦 ∈ 𝐴}    &   ⊢ 𝑁 = (𝐺‘((𝑅1‘𝑀) ∖ 𝐴))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑉 → 𝑁 ∈ ((𝑅1‘𝑀) ∖ 𝐴)))
Theorem	onvf1odlem3 35952*	Lemma for onvf1od 35954. 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 35953*	Lemma for onvf1od 35954. 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 35954*	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-1-onto→V)
Theorem	vonf1wev 35955*	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-1→On, 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-1→On → 𝑅 We V)
Theorem	vonf1owev 35956*	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-1-onto→On → 𝑅 We V)
Theorem	vonf1owevOLD 35957*	Obsolete version of vonf1owev 35956 as of 11-Jun-2026. (Contributed by BTernaryTau, 6-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝐹‘𝑥) ∈ (𝐹‘𝑦)}    ⇒   ⊢ (𝐹:V–1-1-onto→On → 𝑅 We V)
Theorem	wevgblacfn 35958*	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 35959*	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-1-onto→On → (𝑅 We V ∧ 𝑅 Se V))
Theorem	wevsev 35960*	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 35961	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-1-onto→𝐴)
Theorem	vonf1oonf1 35962	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-1-onto→On), 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-1-onto→On → 𝐻:𝐴–1-1→On)
Theorem	vonf1onprcf1ac 35963	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-1→On, 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-1→On)    &   ⊢ (𝜑 → ¬ 𝐴 ∈ V)    &   ⊢ 𝐼 = (◡(𝐹 ↾ 𝐴) ∘ 𝐻)    &   ⊢ 𝐻 = OrdIso( E , (𝐹 “ 𝐴))    ⇒   ⊢ (𝜑 → (𝐼:On–1-1→𝐴 ∧ CHOICE))
Theorem	onprcf1acwevdlem1 35964*	Lemma for onprcf1acwevd 35966 and prconf1acwevd 35967. (Contributed by BTernaryTau, 10-Sep-2026.)
⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    ⇒   ⊢ ((𝐴 ⊆ 𝑊 ∧ 𝐵 ∈ On ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦 We (𝑅1‘𝐵)) → 𝐴 ∈ V)
Theorem	onprcf1acwevdlem2 35965*	Lemma for onprcf1acwevd 35966 and prconf1acwevd 35967. (Contributed by BTernaryTau, 16-Sep-2026.)
⊢ 𝑅 = {⟨𝑦, 𝑧⟩ ∣ ((rank‘𝑦) ∈ (rank‘𝑧) ∨ ((rank‘𝑦) = (rank‘𝑧) ∧ 𝑦𝑆𝑧))}    &   ⊢ 𝑆 = (𝐹‘∩ {𝑤 ∈ On ∣ (𝐹‘𝑤) We (𝑅1‘suc (rank‘𝑦))})    &   ⊢ ((𝜑 ∧ 𝑢 ∈ On) → ∃𝑤 ∈ On (𝐹‘𝑤) We (𝑅1‘𝑢))    ⇒   ⊢ (𝜑 → 𝑅 We V)
Theorem	onprcf1acwevd 35966*	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 35967*	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-1→On))    &   ⊢ (𝜑 → CHOICE)    &   ⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    &   ⊢ 𝑅 = {⟨𝑦, 𝑧⟩ ∣ ((rank‘𝑦) ∈ (rank‘𝑧) ∨ ((rank‘𝑦) = (rank‘𝑧) ∧ 𝑦𝑆𝑧))}    &   ⊢ 𝑆 = (◡𝐹‘∩ {𝑤 ∈ On ∣ (◡𝐹‘𝑤) We (𝑅1‘suc (rank‘𝑦))})    ⇒   ⊢ (𝜑 → 𝑅 We V)
Theorem	vonf1oonfo 35968*	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-1-onto→On), 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-1-onto→V ∧ 𝐴 ≠ ∅) → 𝐻:On–onto→𝐴)
Theorem	onvfowev 35969*	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–onto→V → 𝑅 We V)
Theorem	onf1onf1or 35970	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-1→On → (𝐹:𝐴–1-1→On ∨ 𝐻:On–1-1→𝐴))
Theorem	onf1oracwevd 35971*	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-1→On ∨ ∃𝐻𝐻: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-1→On ∨ 𝐻:On–1-1→𝑊))    &   ⊢ (𝜑 → ∀𝑣(∃𝑓 𝑓:𝑣–1-1→On ∨ ∃ℎ ℎ:On–1-1→𝑣))    &   ⊢ 𝑊 = {𝑟 ∣ ∃𝑥 ∈ On (𝑟 ⊆ ((𝑅1‘𝑥) × (𝑅1‘𝑥)) ∧ 𝑟 We (𝑅1‘𝑥))}    &   ⊢ 𝑅 = {⟨𝑦, 𝑧⟩ ∣ ((rank‘𝑦) ∈ (rank‘𝑧) ∨ ((rank‘𝑦) = (rank‘𝑧) ∧ 𝑦𝐴𝑧))}    &   ⊢ 𝐴 = (𝐼‘∩ {𝑤 ∈ On ∣ (𝐼‘𝑤) We (𝑅1‘suc (rank‘𝑦))})    &   ⊢ 𝐼 = if(𝐹:𝑊–1-1→On, ◡𝐹, 𝐻)    ⇒   ⊢ (𝜑 → 𝑅 We V)
Theorem	onprcf1of1orad 35972	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 35973 for the case where neither class is a proper class, and see onprcf1of1ord 35974 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-1-onto→𝑋)). 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-1-onto→V)    &   ⊢ (𝜑 → (¬ 𝐵 ∈ V → 𝐻:On–1-1-onto→𝐵))    &   ⊢ (𝜑 → ¬ 𝐵 ∈ V)    &   ⊢ 𝐼 = (𝐻 ∘ (◡𝐹 ↾ 𝐴))    ⇒   ⊢ (𝜑 → 𝐼:𝐴–1-1→𝐵)
Theorem	onprcf1of1orbd 35973*	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 35972 for the case where one of the classes is a proper class, and see onprcf1of1ord 35974 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-1-onto→𝑋)), 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-1-onto→V)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (∃𝑓 𝑓:𝐴–1-1→𝐵 ∨ ∃ℎ ℎ:𝐵–1-1→𝐴))
Theorem	onprcf1of1ord 35974*	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-1-onto→𝑋)). 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-1-onto→V)    &   ⊢ (𝜑 → (¬ 𝐴 ∈ V → 𝐻:On–1-1-onto→𝐴))    &   ⊢ (𝜑 → (¬ 𝐵 ∈ V → 𝐼:On–1-1-onto→𝐵))    &   ⊢ 𝐽 = if(𝐴 ∈ V, if(𝐵 ∈ V, 𝐾, (𝐼 ∘ (◡𝐹 ↾ 𝐴))), (𝐻 ∘ (◡𝐹 ↾ 𝐵)))    &   ⊢ 𝐾 = (𝐹‘∩ {𝑥 ∈ On ∣ ((𝐹‘𝑥):𝐴–1-1→𝐵 ∨ (𝐹‘𝑥):𝐵–1-1→𝐴)})    ⇒   ⊢ (𝜑 → (𝐽:𝐴–1-1→𝐵 ∨ 𝐽:𝐵–1-1→𝐴))
Theorem	f1oronf1or 35975	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-1→On ∨ 𝐻:On–1-1→𝐴) → (𝐹:𝐴–1-1→On ∨ 𝐻:On–1-1→𝐴))
21.6.3  Real and complex numbers
Theorem	zltp1ne 35976	Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nnltp1ne 35977	Positive integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	nn0ltp1ne 35978	Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	fisshasheq 35979	A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵)
Theorem	1enum 35980*	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 35775 for a version that uses equinumerosity , 1enumcard 35776 for a version that uses the card function, and 1enumkard 35896 for a version that uses the kard function. (Contributed by BTernaryTau, 26-Jun-2026.)
⊢ (𝐴 ∈ Fin → (♯‘𝐴) = Σ𝑎 ∈ 𝐴 1)
21.6.4  Graph theory
Theorem	cplgredgex 35981*	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 35982	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 35983	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 35984	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 35985	A non-trivial cycle in a simple graph has a length greater than 2. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝐹))
Theorem	usgrcyclgt2v 35986	A simple graph with a non-trivial cycle must have at least 3 vertices. (Contributed by BTernaryTau, 5-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝑉))
Theorem	cusgr3cyclex 35987*	Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 2 < (♯‘𝑉)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))
Theorem	2cycl2d 35988	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐴”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐴, 𝐵} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
21.6.4.1  Acyclic graphs
Theorem	acycgr0v 35989	A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr1v 35990	A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ (♯‘𝑉) = 1) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr2v 35991	A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 2) → 𝐺 ∈ AcyclicGraph)
Theorem	prclisacycgr 35992*	A proper class (representing a null graph, see vtxvalprc 29628) has the property of an acyclic graph (see also acycgr0v 35989). (Contributed by BTernaryTau, 11-Oct-2023.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ 𝐺 ∈ V → ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅))
Theorem	acycgrislfgr 35993*	An acyclic hypergraph is a loop-free hypergraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph) → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})
Theorem	upgracycumgr 35994	An acyclic pseudograph is a multigraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ UMGraph)
Theorem	umgracycusgr 35995	An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	upgracycusgr 35996	An acyclic pseudograph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	cusgracyclt3v 35997	A complete simple graph is acyclic if and only if it has fewer than three vertices. (Contributed by BTernaryTau, 20-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → (𝐺 ∈ AcyclicGraph ↔ (♯‘𝑉) < 3))
Theorem	pthacycspth 35998	A path in an acyclic graph is a simple path. (Contributed by BTernaryTau, 21-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Paths‘𝐺)𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	acycgrsubgr 35999	The subgraph of an acyclic graph is also acyclic. (Contributed by BTernaryTau, 23-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ AcyclicGraph)
21.6.5  Model theory
Syntax	wsmext 36000	Extend wff notation to include a predicate for standard models of the Axiom of Extensionality.
wff 𝑀 ⊨ Ax-Ext