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

Metamath Proof Explorer

Theorem isores1

Description: An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion isores1 
|- ( H Isom R , S ( A , B ) <-> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) )

Proof

Step Hyp Ref Expression
1 isocnv 
 |-  ( H Isom R , S ( A , B ) -> `' H Isom S , R ( B , A ) )
2 isores2 
 |-  ( `' H Isom S , R ( B , A ) <-> `' H Isom S , ( R i^i ( A X. A ) ) ( B , A ) )
3 1 2 sylib 
 |-  ( H Isom R , S ( A , B ) -> `' H Isom S , ( R i^i ( A X. A ) ) ( B , A ) )
4 isocnv 
 |-  ( `' H Isom S , ( R i^i ( A X. A ) ) ( B , A ) -> `' `' H Isom ( R i^i ( A X. A ) ) , S ( A , B ) )
5 3 4 syl 
 |-  ( H Isom R , S ( A , B ) -> `' `' H Isom ( R i^i ( A X. A ) ) , S ( A , B ) )
6 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
7 f1orel 
 |-  ( H : A -1-1-onto-> B -> Rel H )
8 dfrel2 
 |-  ( Rel H <-> `' `' H = H )
9 isoeq1 
 |-  ( `' `' H = H -> ( `' `' H Isom ( R i^i ( A X. A ) ) , S ( A , B ) <-> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) ) )
10 8 9 sylbi 
 |-  ( Rel H -> ( `' `' H Isom ( R i^i ( A X. A ) ) , S ( A , B ) <-> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) ) )
11 6 7 10 3syl 
 |-  ( H Isom R , S ( A , B ) -> ( `' `' H Isom ( R i^i ( A X. A ) ) , S ( A , B ) <-> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) ) )
12 5 11 mpbid 
 |-  ( H Isom R , S ( A , B ) -> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) )
13 isocnv 
 |-  ( H Isom ( R i^i ( A X. A ) ) , S ( A , B ) -> `' H Isom S , ( R i^i ( A X. A ) ) ( B , A ) )
14 13 2 sylibr 
 |-  ( H Isom ( R i^i ( A X. A ) ) , S ( A , B ) -> `' H Isom S , R ( B , A ) )
15 isocnv 
 |-  ( `' H Isom S , R ( B , A ) -> `' `' H Isom R , S ( A , B ) )
16 14 15 syl 
 |-  ( H Isom ( R i^i ( A X. A ) ) , S ( A , B ) -> `' `' H Isom R , S ( A , B ) )
17 isof1o 
 |-  ( H Isom ( R i^i ( A X. A ) ) , S ( A , B ) -> H : A -1-1-onto-> B )
18 isoeq1 
 |-  ( `' `' H = H -> ( `' `' H Isom R , S ( A , B ) <-> H Isom R , S ( A , B ) ) )
19 8 18 sylbi 
 |-  ( Rel H -> ( `' `' H Isom R , S ( A , B ) <-> H Isom R , S ( A , B ) ) )
20 17 7 19 3syl 
 |-  ( H Isom ( R i^i ( A X. A ) ) , S ( A , B ) -> ( `' `' H Isom R , S ( A , B ) <-> H Isom R , S ( A , B ) ) )
21 16 20 mpbid 
 |-  ( H Isom ( R i^i ( A X. A ) ) , S ( A , B ) -> H Isom R , S ( A , B ) )
22 12 21 impbii 
 |-  ( H Isom R , S ( A , B ) <-> H Isom ( R i^i ( A X. A ) ) , S ( A , B ) )