Metamath Proof Explorer


Theorem oiiso2

Description: The order isomorphism of the well-order R on A is an isomorphism onto ran O (which is a subset of A by oif ). (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1 F=OrdIsoRA
Assertion oiiso2 RWeARSeAFIsomE,RdomFranF

Proof

Step Hyp Ref Expression
1 oicl.1 F=OrdIsoRA
2 eqid recshVιvwA|jranhjRw|uwA|jranhjRw¬uRv=recshVιvwA|jranhjRw|uwA|jranhjRw¬uRv
3 eqid wA|jranhjRw=wA|jranhjRw
4 eqid hVιvwA|jranhjRw|uwA|jranhjRw¬uRv=hVιvwA|jranhjRw|uwA|jranhjRw¬uRv
5 2 3 4 ordtypecbv recsfVιsyA|iranfiRy|ryA|iranfiRy¬rRs=recshVιvwA|jranhjRw|uwA|jranhjRw¬uRv
6 eqid xOn|tAzrecsfVιsyA|iranfiRy|ryA|iranfiRy¬rRsxzRt=xOn|tAzrecsfVιsyA|iranfiRy|ryA|iranfiRy¬rRsxzRt
7 simpl RWeARSeARWeA
8 simpr RWeARSeARSeA
9 5 3 4 6 1 7 8 ordtypelem8 RWeARSeAFIsomE,RdomFranF