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 bitrid
 |-  ( 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 bitrid
 |-  ( ( 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 ) } ) ) )