# 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}}\left({A},{B}\right)↔{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 isocnv ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {{H}}^{-1}{Isom}_{{S},{R}}\left({B},{A}\right)$
2 isores2 ${⊢}{{H}}^{-1}{Isom}_{{S},{R}}\left({B},{A}\right)↔{{H}}^{-1}{Isom}_{{S},{R}\cap \left({A}×{A}\right)}\left({B},{A}\right)$
3 1 2 sylib ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {{H}}^{-1}{Isom}_{{S},{R}\cap \left({A}×{A}\right)}\left({B},{A}\right)$
4 isocnv ${⊢}{{H}}^{-1}{Isom}_{{S},{R}\cap \left({A}×{A}\right)}\left({B},{A}\right)\to {{{H}}^{-1}}^{-1}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)$
5 3 4 syl ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {{{H}}^{-1}}^{-1}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)$
6 isof1o ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {H}:{A}\underset{1-1 onto}{⟶}{B}$
7 f1orel ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}\to \mathrm{Rel}{H}$
8 dfrel2 ${⊢}\mathrm{Rel}{H}↔{{{H}}^{-1}}^{-1}={H}$
9 isoeq1 ${⊢}{{{H}}^{-1}}^{-1}={H}\to \left({{{H}}^{-1}}^{-1}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)↔{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\right)$
10 8 9 sylbi ${⊢}\mathrm{Rel}{H}\to \left({{{H}}^{-1}}^{-1}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)↔{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\right)$
11 6 7 10 3syl ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to \left({{{H}}^{-1}}^{-1}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)↔{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\right)$
12 5 11 mpbid ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)\to {H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)$
13 isocnv ${⊢}{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\to {{H}}^{-1}{Isom}_{{S},{R}\cap \left({A}×{A}\right)}\left({B},{A}\right)$
14 13 2 sylibr ${⊢}{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\to {{H}}^{-1}{Isom}_{{S},{R}}\left({B},{A}\right)$
15 isocnv ${⊢}{{H}}^{-1}{Isom}_{{S},{R}}\left({B},{A}\right)\to {{{H}}^{-1}}^{-1}{Isom}_{{R},{S}}\left({A},{B}\right)$
16 14 15 syl ${⊢}{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\to {{{H}}^{-1}}^{-1}{Isom}_{{R},{S}}\left({A},{B}\right)$
17 isof1o ${⊢}{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\to {H}:{A}\underset{1-1 onto}{⟶}{B}$
18 isoeq1 ${⊢}{{{H}}^{-1}}^{-1}={H}\to \left({{{H}}^{-1}}^{-1}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{R},{S}}\left({A},{B}\right)\right)$
19 8 18 sylbi ${⊢}\mathrm{Rel}{H}\to \left({{{H}}^{-1}}^{-1}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{R},{S}}\left({A},{B}\right)\right)$
20 17 7 19 3syl ${⊢}{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\to \left({{{H}}^{-1}}^{-1}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{R},{S}}\left({A},{B}\right)\right)$
21 16 20 mpbid ${⊢}{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)\to {H}{Isom}_{{R},{S}}\left({A},{B}\right)$
22 12 21 impbii ${⊢}{H}{Isom}_{{R},{S}}\left({A},{B}\right)↔{H}{Isom}_{{R}\cap \left({A}×{A}\right),{S}}\left({A},{B}\right)$