Theorem oiiso

Description: The order isomorphism of the well-order R on A is an isomorphism. (Contributed by Mario Carneiro, 23-May-2015)

	Ref	Expression
Hypothesis	oicl.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion	oiiso	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		oicl.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
2		exse	⊢ ( 𝐴 ∈ 𝑉 → 𝑅 Se 𝐴 )
3	1	ordtype	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
4	3	ancoms	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑅 We 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )
5	2 4	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )