This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oien

Description: The order type of a well-ordered set is equinumerous to the set. (Contributed by Mario Carneiro, 23-May-2015)

		Ref	Expression
	Hypothesis	oicl.1	$⊢ F = OrdIso (R, A)$
	Assertion	oien	$⊢ (A \in V \land R We A) \to dom F \approx A$

Step	Hyp	Ref	Expression
1		oicl.1	$⊢ F = OrdIso (R, A)$
2	1	oiexg	$⊢ A \in V \to F \in V$
3	1	oiiso	$⊢ (A \in V \land R We A) \to F {Isom}_{E, R} (dom F, A)$
4		isof1o	$⊢ F {Isom}_{E, R} (dom F, A) \to F : dom F \underset{1-1 onto}{⟶} A$
5	3 4	syl	$⊢ (A \in V \land R We A) \to F : dom F \underset{1-1 onto}{⟶} A$
6		f1oen3g	$⊢ (F \in V \land F : dom F \underset{1-1 onto}{⟶} A) \to dom F \approx A$
7	2 5 6	syl2an2r	$⊢ (A \in V \land R We A) \to dom F \approx A$