Theorem vonf1owev

Description: If F is a bijection from the universe to the ordinals, then R 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)

	Ref	Expression
Hypothesis	vonf1owev.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
Assertion	vonf1owev	⊢ ( 𝐹 : V –1-1-onto→ On → 𝑅 We V )

Proof

Step	Hyp	Ref	Expression
1		vonf1owev.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
2		f1of1	⊢ ( 𝐹 : V –1-1-onto→ On → 𝐹 : V –1-1→ On )
3	1	vonf1wev	⊢ ( 𝐹 : V –1-1→ On → 𝑅 We V )
4	2 3	syl	⊢ ( 𝐹 : V –1-1-onto→ On → 𝑅 We V )