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 HIsomR,SABHIsomRA×A,SAB

Proof

Step Hyp Ref Expression
1 isocnv HIsomR,SABH-1IsomS,RBA
2 isores2 H-1IsomS,RBAH-1IsomS,RA×ABA
3 1 2 sylib HIsomR,SABH-1IsomS,RA×ABA
4 isocnv H-1IsomS,RA×ABAH-1-1IsomRA×A,SAB
5 3 4 syl HIsomR,SABH-1-1IsomRA×A,SAB
6 isof1o HIsomR,SABH:A1-1 ontoB
7 f1orel H:A1-1 ontoBRelH
8 dfrel2 RelHH-1-1=H
9 isoeq1 H-1-1=HH-1-1IsomRA×A,SABHIsomRA×A,SAB
10 8 9 sylbi RelHH-1-1IsomRA×A,SABHIsomRA×A,SAB
11 6 7 10 3syl HIsomR,SABH-1-1IsomRA×A,SABHIsomRA×A,SAB
12 5 11 mpbid HIsomR,SABHIsomRA×A,SAB
13 isocnv HIsomRA×A,SABH-1IsomS,RA×ABA
14 13 2 sylibr HIsomRA×A,SABH-1IsomS,RBA
15 isocnv H-1IsomS,RBAH-1-1IsomR,SAB
16 14 15 syl HIsomRA×A,SABH-1-1IsomR,SAB
17 isof1o HIsomRA×A,SABH:A1-1 ontoB
18 isoeq1 H-1-1=HH-1-1IsomR,SABHIsomR,SAB
19 8 18 sylbi RelHH-1-1IsomR,SABHIsomR,SAB
20 17 7 19 3syl HIsomRA×A,SABH-1-1IsomR,SABHIsomR,SAB
21 16 20 mpbid HIsomRA×A,SABHIsomR,SAB
22 12 21 impbii HIsomR,SABHIsomRA×A,SAB