Metamath Proof Explorer


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 𝐹 , 𝐴 ) )