Metamath Proof Explorer

Theorem isores2

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 isores2 
|- ( H Isom R , S ( A , B ) <-> H Isom R , ( S i^i ( B X. B ) ) ( A , B ) )

Proof

Step Hyp Ref Expression
1 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
2 ffvelrn 
 |-  ( ( H : A --> B /\ x e. A ) -> ( H ` x ) e. B )
3 2 adantrr 
 |-  ( ( H : A --> B /\ ( x e. A /\ y e. A ) ) -> ( H ` x ) e. B )
4 ffvelrn 
 |-  ( ( H : A --> B /\ y e. A ) -> ( H ` y ) e. B )
5 4 adantrl 
 |-  ( ( H : A --> B /\ ( x e. A /\ y e. A ) ) -> ( H ` y ) e. B )
6 brinxp 
 |-  ( ( ( H ` x ) e. B /\ ( H ` y ) e. B ) -> ( ( H ` x ) S ( H ` y ) <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) )
7 3 5 6 syl2anc 
 |-  ( ( H : A --> B /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) S ( H ` y ) <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) )
8 1 7 sylan 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) S ( H ` y ) <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) )
9 8 anassrs 
 |-  ( ( ( H : A -1-1-onto-> B /\ x e. A ) /\ y e. A ) -> ( ( H ` x ) S ( H ` y ) <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) )
10 9 bibi2d 
 |-  ( ( ( H : A -1-1-onto-> B /\ x e. A ) /\ y e. A ) -> ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( x R y <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) ) )
11 10 ralbidva 
 |-  ( ( H : A -1-1-onto-> B /\ x e. A ) -> ( A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. y e. A ( x R y <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) ) )
12 11 ralbidva 
 |-  ( H : A -1-1-onto-> B -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. x e. A A. y e. A ( x R y <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) ) )
13 12 pm5.32i 
 |-  ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) ) )
14 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
15 df-isom 
 |-  ( H Isom R , ( S i^i ( B X. B ) ) ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) ( S i^i ( B X. B ) ) ( H ` y ) ) ) )
16 13 14 15 3bitr4i 
 |-  ( H Isom R , S ( A , B ) <-> H Isom R , ( S i^i ( B X. B ) ) ( A , B ) )