Metamath Proof Explorer

Theorem isoini

Description: Isomorphisms preserve initial segments. Proposition 6.31(2) of TakeutiZaring p. 33. (Contributed by NM, 20-Apr-2004)

Ref Expression
Assertion isoini 
|- ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( H " ( A i^i ( `' R " { D } ) ) ) = ( B i^i ( `' S " { ( H ` D ) } ) ) )

Proof

Step Hyp Ref Expression
1 dfima2 
 |-  ( H " ( A i^i ( `' R " { D } ) ) ) = { y | E. x e. ( A i^i ( `' R " { D } ) ) x H y }
2 elin 
 |-  ( y e. ( B i^i ( `' S " { ( H ` D ) } ) ) <-> ( y e. B /\ y e. ( `' S " { ( H ` D ) } ) ) )
3 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
4 f1ofo 
 |-  ( H : A -1-1-onto-> B -> H : A -onto-> B )
5 forn 
 |-  ( H : A -onto-> B -> ran H = B )
6 5 eleq2d 
 |-  ( H : A -onto-> B -> ( y e. ran H <-> y e. B ) )
7 3 4 6 3syl 
 |-  ( H Isom R , S ( A , B ) -> ( y e. ran H <-> y e. B ) )
8 f1ofn 
 |-  ( H : A -1-1-onto-> B -> H Fn A )
9 fvelrnb 
 |-  ( H Fn A -> ( y e. ran H <-> E. x e. A ( H ` x ) = y ) )
10 3 8 9 3syl 
 |-  ( H Isom R , S ( A , B ) -> ( y e. ran H <-> E. x e. A ( H ` x ) = y ) )
11 7 10 bitr3d 
 |-  ( H Isom R , S ( A , B ) -> ( y e. B <-> E. x e. A ( H ` x ) = y ) )
12 fvex 
 |-  ( H ` D ) e. _V
13 vex 
 |-  y e. _V
14 13 eliniseg 
 |-  ( ( H ` D ) e. _V -> ( y e. ( `' S " { ( H ` D ) } ) <-> y S ( H ` D ) ) )
15 12 14 mp1i 
 |-  ( H Isom R , S ( A , B ) -> ( y e. ( `' S " { ( H ` D ) } ) <-> y S ( H ` D ) ) )
16 11 15 anbi12d 
 |-  ( H Isom R , S ( A , B ) -> ( ( y e. B /\ y e. ( `' S " { ( H ` D ) } ) ) <-> ( E. x e. A ( H ` x ) = y /\ y S ( H ` D ) ) ) )
17 16 adantr 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( ( y e. B /\ y e. ( `' S " { ( H ` D ) } ) ) <-> ( E. x e. A ( H ` x ) = y /\ y S ( H ` D ) ) ) )
18 elin 
 |-  ( x e. ( A i^i ( `' R " { D } ) ) <-> ( x e. A /\ x e. ( `' R " { D } ) ) )
19 vex 
 |-  x e. _V
20 19 eliniseg 
 |-  ( D e. A -> ( x e. ( `' R " { D } ) <-> x R D ) )
21 20 anbi2d 
 |-  ( D e. A -> ( ( x e. A /\ x e. ( `' R " { D } ) ) <-> ( x e. A /\ x R D ) ) )
22 18 21 syl5bb 
 |-  ( D e. A -> ( x e. ( A i^i ( `' R " { D } ) ) <-> ( x e. A /\ x R D ) ) )
23 22 anbi1d 
 |-  ( D e. A -> ( ( x e. ( A i^i ( `' R " { D } ) ) /\ x H y ) <-> ( ( x e. A /\ x R D ) /\ x H y ) ) )
24 anass 
 |-  ( ( ( x e. A /\ x R D ) /\ x H y ) <-> ( x e. A /\ ( x R D /\ x H y ) ) )
25 23 24 bitrdi 
 |-  ( D e. A -> ( ( x e. ( A i^i ( `' R " { D } ) ) /\ x H y ) <-> ( x e. A /\ ( x R D /\ x H y ) ) ) )
26 25 adantl 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( ( x e. ( A i^i ( `' R " { D } ) ) /\ x H y ) <-> ( x e. A /\ ( x R D /\ x H y ) ) ) )
27 isorel 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x R D <-> ( H ` x ) S ( H ` D ) ) )
28 3 8 syl 
 |-  ( H Isom R , S ( A , B ) -> H Fn A )
29 fnbrfvb 
 |-  ( ( H Fn A /\ x e. A ) -> ( ( H ` x ) = y <-> x H y ) )
30 29 bicomd 
 |-  ( ( H Fn A /\ x e. A ) -> ( x H y <-> ( H ` x ) = y ) )
31 28 30 sylan 
 |-  ( ( H Isom R , S ( A , B ) /\ x e. A ) -> ( x H y <-> ( H ` x ) = y ) )
32 31 adantrr 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( x H y <-> ( H ` x ) = y ) )
33 27 32 anbi12d 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( ( x R D /\ x H y ) <-> ( ( H ` x ) S ( H ` D ) /\ ( H ` x ) = y ) ) )
34 ancom 
 |-  ( ( ( H ` x ) S ( H ` D ) /\ ( H ` x ) = y ) <-> ( ( H ` x ) = y /\ ( H ` x ) S ( H ` D ) ) )
35 breq1 
 |-  ( ( H ` x ) = y -> ( ( H ` x ) S ( H ` D ) <-> y S ( H ` D ) ) )
36 35 pm5.32i 
 |-  ( ( ( H ` x ) = y /\ ( H ` x ) S ( H ` D ) ) <-> ( ( H ` x ) = y /\ y S ( H ` D ) ) )
37 34 36 bitri 
 |-  ( ( ( H ` x ) S ( H ` D ) /\ ( H ` x ) = y ) <-> ( ( H ` x ) = y /\ y S ( H ` D ) ) )
38 33 37 bitrdi 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x e. A /\ D e. A ) ) -> ( ( x R D /\ x H y ) <-> ( ( H ` x ) = y /\ y S ( H ` D ) ) ) )
39 38 exp32 
 |-  ( H Isom R , S ( A , B ) -> ( x e. A -> ( D e. A -> ( ( x R D /\ x H y ) <-> ( ( H ` x ) = y /\ y S ( H ` D ) ) ) ) ) )
40 39 com23 
 |-  ( H Isom R , S ( A , B ) -> ( D e. A -> ( x e. A -> ( ( x R D /\ x H y ) <-> ( ( H ` x ) = y /\ y S ( H ` D ) ) ) ) ) )
41 40 imp 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( x e. A -> ( ( x R D /\ x H y ) <-> ( ( H ` x ) = y /\ y S ( H ` D ) ) ) ) )
42 41 pm5.32d 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( ( x e. A /\ ( x R D /\ x H y ) ) <-> ( x e. A /\ ( ( H ` x ) = y /\ y S ( H ` D ) ) ) ) )
43 26 42 bitrd 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( ( x e. ( A i^i ( `' R " { D } ) ) /\ x H y ) <-> ( x e. A /\ ( ( H ` x ) = y /\ y S ( H ` D ) ) ) ) )
44 43 rexbidv2 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( E. x e. ( A i^i ( `' R " { D } ) ) x H y <-> E. x e. A ( ( H ` x ) = y /\ y S ( H ` D ) ) ) )
45 r19.41v 
 |-  ( E. x e. A ( ( H ` x ) = y /\ y S ( H ` D ) ) <-> ( E. x e. A ( H ` x ) = y /\ y S ( H ` D ) ) )
46 44 45 bitrdi 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( E. x e. ( A i^i ( `' R " { D } ) ) x H y <-> ( E. x e. A ( H ` x ) = y /\ y S ( H ` D ) ) ) )
47 17 46 bitr4d 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( ( y e. B /\ y e. ( `' S " { ( H ` D ) } ) ) <-> E. x e. ( A i^i ( `' R " { D } ) ) x H y ) )
48 2 47 syl5bb 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( y e. ( B i^i ( `' S " { ( H ` D ) } ) ) <-> E. x e. ( A i^i ( `' R " { D } ) ) x H y ) )
49 48 abbi2dv 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( B i^i ( `' S " { ( H ` D ) } ) ) = { y | E. x e. ( A i^i ( `' R " { D } ) ) x H y } )
50 1 49 eqtr4id 
 |-  ( ( H Isom R , S ( A , B ) /\ D e. A ) -> ( H " ( A i^i ( `' R " { D } ) ) ) = ( B i^i ( `' S " { ( H ` D ) } ) ) )