Metamath Proof Explorer

Theorem isoini2

Description: Isomorphisms are isomorphisms on their initial segments. (Contributed by Mario Carneiro, 29-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 isoini2.1 
 |-  C = ( A i^i ( `' R " { X } ) )
2 isoini2.2 
 |-  D = ( B i^i ( `' S " { ( H ` X ) } ) )
3 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
4 f1of1 
 |-  ( H : A -1-1-onto-> B -> H : A -1-1-> B )
5 3 4 syl 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-> B )
6 5 adantr 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> H : A -1-1-> B )
7 inss1 
 |-  ( A i^i ( `' R " { X } ) ) C_ A
8 1 7 eqsstri 
 |-  C C_ A
9 f1ores 
 |-  ( ( H : A -1-1-> B /\ C C_ A ) -> ( H |` C ) : C -1-1-onto-> ( H " C ) )
10 6 8 9 sylancl 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( H |` C ) : C -1-1-onto-> ( H " C ) )
11 isoini 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( H " ( A i^i ( `' R " { X } ) ) ) = ( B i^i ( `' S " { ( H ` X ) } ) ) )
12 1 imaeq2i 
 |-  ( H " C ) = ( H " ( A i^i ( `' R " { X } ) ) )
13 11 12 2 3eqtr4g 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( H " C ) = D )
14 13 f1oeq3d 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( ( H |` C ) : C -1-1-onto-> ( H " C ) <-> ( H |` C ) : C -1-1-onto-> D ) )
15 10 14 mpbid 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( H |` C ) : C -1-1-onto-> D )
16 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 ) ) ) )
17 16 simprbi 
 |-  ( H Isom R , S ( A , B ) -> A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) )
18 17 adantr 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) )
19 ssralv 
 |-  ( C C_ A -> ( A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) -> A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
20 19 ralimdv 
 |-  ( C C_ A -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) -> A. x e. A A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
21 8 18 20 mpsyl 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> A. x e. A A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) )
22 ssralv 
 |-  ( C C_ A -> ( A. x e. A A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) -> A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
23 8 21 22 mpsyl 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) )
24 fvres 
 |-  ( x e. C -> ( ( H |` C ) ` x ) = ( H ` x ) )
25 fvres 
 |-  ( y e. C -> ( ( H |` C ) ` y ) = ( H ` y ) )
26 24 25 breqan12d 
 |-  ( ( x e. C /\ y e. C ) -> ( ( ( H |` C ) ` x ) S ( ( H |` C ) ` y ) <-> ( H ` x ) S ( H ` y ) ) )
27 26 bibi2d 
 |-  ( ( x e. C /\ y e. C ) -> ( ( x R y <-> ( ( H |` C ) ` x ) S ( ( H |` C ) ` y ) ) <-> ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
28 27 ralbidva 
 |-  ( x e. C -> ( A. y e. C ( x R y <-> ( ( H |` C ) ` x ) S ( ( H |` C ) ` y ) ) <-> A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
29 28 ralbiia 
 |-  ( A. x e. C A. y e. C ( x R y <-> ( ( H |` C ) ` x ) S ( ( H |` C ) ` y ) ) <-> A. x e. C A. y e. C ( x R y <-> ( H ` x ) S ( H ` y ) ) )
30 23 29 sylibr 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> A. x e. C A. y e. C ( x R y <-> ( ( H |` C ) ` x ) S ( ( H |` C ) ` y ) ) )
31 df-isom 
 |-  ( ( H |` C ) Isom R , S ( C , D ) <-> ( ( H |` C ) : C -1-1-onto-> D /\ A. x e. C A. y e. C ( x R y <-> ( ( H |` C ) ` x ) S ( ( H |` C ) ` y ) ) ) )
32 15 30 31 sylanbrc 
 |-  ( ( H Isom R , S ( A , B ) /\ X e. A ) -> ( H |` C ) Isom R , S ( C , D ) )