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	|- F = OrdIso ( R , A )
Assertion	ordtypeon	|- ( ( R We A /\ R Se A /\ -. A e. _V ) -> F Isom _E , R ( On , A ) )

Proof

Step	Hyp	Ref	Expression
1		ordtypeon.1	|- F = OrdIso ( R , A )
2	1	ordtype	|- ( ( R We A /\ R Se A ) -> F Isom _E , R ( dom F , A ) )
3	2	3adant3	|- ( ( R We A /\ R Se A /\ -. A e. _V ) -> F Isom _E , R ( dom F , A ) )
4	1	oicl	|- Ord dom F
5		isof1o	|- ( F Isom _E , R ( dom F , A ) -> F : dom F -1-1-onto-> A )
6		f1ovv	|- ( F : dom F -1-1-onto-> A -> ( dom F e. _V <-> A e. _V ) )
7	2 5 6	3syl	|- ( ( R We A /\ R Se A ) -> ( dom F e. _V <-> A e. _V ) )
8	7	notbid	|- ( ( R We A /\ R Se A ) -> ( -. dom F e. _V <-> -. A e. _V ) )
9	8	biimp3ar	|- ( ( R We A /\ R Se A /\ -. A e. _V ) -> -. dom F e. _V )
10		ordprcon	|- ( ( Ord dom F /\ -. dom F e. _V ) -> dom F = On )
11	4 9 10	sylancr	|- ( ( R We A /\ R Se A /\ -. A e. _V ) -> dom F = On )
12		isoeq4	|- ( dom F = On -> ( F Isom _E , R ( dom F , A ) <-> F Isom _E , R ( On , A ) ) )
13	11 12	syl	|- ( ( R We A /\ R Se A /\ -. A e. _V ) -> ( F Isom _E , R ( dom F , A ) <-> F Isom _E , R ( On , A ) ) )
14	3 13	mpbid	|- ( ( R We A /\ R Se A /\ -. A e. _V ) -> F Isom _E , R ( On , A ) )