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	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion	oien	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → dom 𝐹 ≈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		oicl.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
2	1	oiexg	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 ∈ V )
3	1	oiiso	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
4		isof1o	⊢ ( 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
5	3 4	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
6		f1oen3g	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 ) → dom 𝐹 ≈ 𝐴 )
7	2 5 6	syl2an2r	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → dom 𝐹 ≈ 𝐴 )