Metamath Proof Explorer

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 \land R Se A \land \neg A \in V) \to F {Isom}_{E, R} (On, A)$

Proof

Step	Hyp	Ref	Expression
1		ordtypeon.1	$⊢ F = OrdIso (R, A)$
2	1	ordtype	$⊢ (R We A \land R Se A) \to F {Isom}_{E, R} (dom F, A)$
3	2	3adant3	$⊢ (R We A \land R Se A \land \neg A \in V) \to F {Isom}_{E, R} (dom F, A)$
4	1	oicl	$⊢ Ord dom F$
5		isof1o	$⊢ F {Isom}_{E, R} (dom F, A) \to F : dom F \underset{1-1 onto}{⟶} A$
6		f1ovv	$⊢ F : dom F \underset{1-1 onto}{⟶} A \to (dom F \in V \leftrightarrow A \in V)$
7	2 5 6	3syl	$⊢ (R We A \land R Se A) \to (dom F \in V \leftrightarrow A \in V)$
8	7	notbid	$⊢ (R We A \land R Se A) \to (\neg dom F \in V \leftrightarrow \neg A \in V)$
9	8	biimp3ar	$⊢ (R We A \land R Se A \land \neg A \in V) \to \neg dom F \in V$
10		ordprcon	$⊢ (Ord dom F \land \neg dom F \in V) \to dom F = On$
11	4 9 10	sylancr	$⊢ (R We A \land R Se A \land \neg A \in V) \to dom F = On$
12		isoeq4	$⊢ dom F = On \to (F {Isom}_{E, R} (dom F, A) \leftrightarrow F {Isom}_{E, R} (On, A))$
13	11 12	syl	$⊢ (R We A \land R Se A \land \neg A \in V) \to (F {Isom}_{E, R} (dom F, A) \leftrightarrow F {Isom}_{E, R} (On, A))$
14	3 13	mpbid	$⊢ (R We A \land R Se A \land \neg A \in V) \to F {Isom}_{E, R} (On, A)$