# 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 ) )`