Theorem vonf1osev

Description: If F is a bijection from the universe to the ordinals, then R is a set-like well-ordering of the universe. This is the ZFC version of (2 -> 4) which is 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)

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

Proof

Step	Hyp	Ref	Expression
1		vonf1osev.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
2	1	vonf1owev	⊢ ( 𝐹 : V –1-1-onto→ On → 𝑅 We V )
3		vex	⊢ 𝑤 ∈ V
4		vex	⊢ 𝑧 ∈ V
5		fveq2	⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
6	5	eleq1d	⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
7		fveq2	⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
8	7	eleq2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
9	3 4 6 8 1	brab	⊢ ( 𝑤 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) )
10		fvex	⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
11	10	epeli	⊢ ( ( 𝐹 ‘ 𝑤 ) E ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) )
12	9 11	bitr4i	⊢ ( 𝑤 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) E ( 𝐹 ‘ 𝑧 ) )
13	12	rgen2w	⊢ ∀ 𝑤 ∈ V ∀ 𝑧 ∈ V ( 𝑤 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) E ( 𝐹 ‘ 𝑧 ) )
14		df-isom	⊢ ( 𝐹 Isom 𝑅 , E ( V , On ) ↔ ( 𝐹 : V –1-1-onto→ On ∧ ∀ 𝑤 ∈ V ∀ 𝑧 ∈ V ( 𝑤 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) E ( 𝐹 ‘ 𝑧 ) ) ) )
15	13 14	mpbiran2	⊢ ( 𝐹 Isom 𝑅 , E ( V , On ) ↔ 𝐹 : V –1-1-onto→ On )
16		epse	⊢ E Se On
17		isose	⊢ ( 𝐹 Isom 𝑅 , E ( V , On ) → ( 𝑅 Se V ↔ E Se On ) )
18	16 17	mpbiri	⊢ ( 𝐹 Isom 𝑅 , E ( V , On ) → 𝑅 Se V )
19	15 18	sylbir	⊢ ( 𝐹 : V –1-1-onto→ On → 𝑅 Se V )
20	2 19	jca	⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝑅 We V ∧ 𝑅 Se V ) )