Theorem ordtypeon

Description: A proper class with a set-like well-ordering is isomorphic to the proper class of all ordinal numbers. (Contributed by BTernaryTau, 9-Jun-2026)

	Ref	Expression
Hypothesis	ordtypeon.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion	ordtypeon	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) → 𝐹 Isom E , 𝑅 ( On , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtypeon.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
2	1	ordtype	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
3	2	3adant3	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
4	1	oicl	⊢ Ord dom 𝐹
5		isof1o	⊢ ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
6		f1ovv	⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 → ( dom 𝐹 ∈ V ↔ 𝐴 ∈ V ) )
7	2 5 6	3syl	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( dom 𝐹 ∈ V ↔ 𝐴 ∈ V ) )
8	7	notbid	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( ¬ dom 𝐹 ∈ V ↔ ¬ 𝐴 ∈ V ) )
9	8	biimp3ar	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) → ¬ dom 𝐹 ∈ V )
10		ordprcon	⊢ ( ( Ord dom 𝐹 ∧ ¬ dom 𝐹 ∈ V ) → dom 𝐹 = On )
11	4 9 10	sylancr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) → dom 𝐹 = On )
12		isoeq4	⊢ ( dom 𝐹 = On → ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ↔ 𝐹 Isom E , 𝑅 ( On , 𝐴 ) ) )
13	11 12	syl	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) → ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) ↔ 𝐹 Isom E , 𝑅 ( On , 𝐴 ) ) )
14	3 13	mpbid	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ¬ 𝐴 ∈ V ) → 𝐹 Isom E , 𝑅 ( On , 𝐴 ) )