Theorem wevonprcf1o

Description: If R is a set-like well-ordering of the universe and A is a proper class, then F is a bijection from the ordinals to A . This is the ZFC version of (4 -> 5) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 9-Jun-2026)

	Ref	Expression
Hypothesis	wevonprcf1o.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion	wevonprcf1o	⊢ ( ( 𝑅 We V ∧ 𝑅 Se V ∧ ¬ 𝐴 ∈ V ) → 𝐹 : On –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		wevonprcf1o.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
2		ssv	⊢ 𝐴 ⊆ V
3		wess	⊢ ( 𝐴 ⊆ V → ( 𝑅 We V → 𝑅 We 𝐴 ) )
4	2 3	ax-mp	⊢ ( 𝑅 We V → 𝑅 We 𝐴 )
5		sess2	⊢ ( 𝐴 ⊆ V → ( 𝑅 Se V → 𝑅 Se 𝐴 ) )
6	2 5	ax-mp	⊢ ( 𝑅 Se V → 𝑅 Se 𝐴 )
7		id	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 ∈ V )
8	4 6 7	3anim123i	⊢ ( ( 𝑅 We V ∧ 𝑅 Se V ∧ ¬ 𝐴 ∈ V ) → ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) )
9	1	ordtypeon	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) → 𝐹 Isom E , 𝑅 ( On , 𝐴 ) )
10		isof1o	⊢ ( 𝐹 Isom E , 𝑅 ( On , 𝐴 ) → 𝐹 : On –1-1-onto→ 𝐴 )
11	8 9 10	3syl	⊢ ( ( 𝑅 We V ∧ 𝑅 Se V ∧ ¬ 𝐴 ∈ V ) → 𝐹 : On –1-1-onto→ 𝐴 )