This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isoselem

Description: Lemma for isose . (Contributed by Mario Carneiro, 23-Jun-2015)

Ref Expression
Hypotheses isofrlem.1 
|- ( ph -> H Isom R , S ( A , B ) )
isofrlem.2 
|- ( ph -> ( H " x ) e. _V )
Assertion isoselem 
|- ( ph -> ( R Se A -> S Se B ) )

Proof

Step Hyp Ref Expression
1 isofrlem.1 
 |-  ( ph -> H Isom R , S ( A , B ) )
2 isofrlem.2 
 |-  ( ph -> ( H " x ) e. _V )
3 dfse2 
 |-  ( R Se A <-> A. z e. A ( A i^i ( `' R " { z } ) ) e. _V )
4 3 biimpi 
 |-  ( R Se A -> A. z e. A ( A i^i ( `' R " { z } ) ) e. _V )
5 4 r19.21bi 
 |-  ( ( R Se A /\ z e. A ) -> ( A i^i ( `' R " { z } ) ) e. _V )
6 5 expcom 
 |-  ( z e. A -> ( R Se A -> ( A i^i ( `' R " { z } ) ) e. _V ) )
7 6 adantl 
 |-  ( ( ph /\ z e. A ) -> ( R Se A -> ( A i^i ( `' R " { z } ) ) e. _V ) )
8 imaeq2 
 |-  ( x = ( A i^i ( `' R " { z } ) ) -> ( H " x ) = ( H " ( A i^i ( `' R " { z } ) ) ) )
9 8 eleq1d 
 |-  ( x = ( A i^i ( `' R " { z } ) ) -> ( ( H " x ) e. _V <-> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
10 9 imbi2d 
 |-  ( x = ( A i^i ( `' R " { z } ) ) -> ( ( ph -> ( H " x ) e. _V ) <-> ( ph -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) ) )
11 10 2 vtoclg 
 |-  ( ( A i^i ( `' R " { z } ) ) e. _V -> ( ph -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
12 11 com12 
 |-  ( ph -> ( ( A i^i ( `' R " { z } ) ) e. _V -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
13 12 adantr 
 |-  ( ( ph /\ z e. A ) -> ( ( A i^i ( `' R " { z } ) ) e. _V -> ( H " ( A i^i ( `' R " { z } ) ) ) e. _V ) )
14 isoini 
 |-  ( ( H Isom R , S ( A , B ) /\ z e. A ) -> ( H " ( A i^i ( `' R " { z } ) ) ) = ( B i^i ( `' S " { ( H ` z ) } ) ) )
15 1 14 sylan 
 |-  ( ( ph /\ z e. A ) -> ( H " ( A i^i ( `' R " { z } ) ) ) = ( B i^i ( `' S " { ( H ` z ) } ) ) )
16 15 eleq1d 
 |-  ( ( ph /\ z e. A ) -> ( ( H " ( A i^i ( `' R " { z } ) ) ) e. _V <-> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
17 13 16 sylibd 
 |-  ( ( ph /\ z e. A ) -> ( ( A i^i ( `' R " { z } ) ) e. _V -> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
18 7 17 syld 
 |-  ( ( ph /\ z e. A ) -> ( R Se A -> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
19 18 ralrimdva 
 |-  ( ph -> ( R Se A -> A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
20 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
21 f1ofn 
 |-  ( H : A -1-1-onto-> B -> H Fn A )
22 sneq 
 |-  ( y = ( H ` z ) -> { y } = { ( H ` z ) } )
23 22 imaeq2d 
 |-  ( y = ( H ` z ) -> ( `' S " { y } ) = ( `' S " { ( H ` z ) } ) )
24 23 ineq2d 
 |-  ( y = ( H ` z ) -> ( B i^i ( `' S " { y } ) ) = ( B i^i ( `' S " { ( H ` z ) } ) ) )
25 24 eleq1d 
 |-  ( y = ( H ` z ) -> ( ( B i^i ( `' S " { y } ) ) e. _V <-> ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
26 25 ralrn 
 |-  ( H Fn A -> ( A. y e. ran H ( B i^i ( `' S " { y } ) ) e. _V <-> A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
27 1 20 21 26 4syl 
 |-  ( ph -> ( A. y e. ran H ( B i^i ( `' S " { y } ) ) e. _V <-> A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V ) )
28 f1ofo 
 |-  ( H : A -1-1-onto-> B -> H : A -onto-> B )
29 forn 
 |-  ( H : A -onto-> B -> ran H = B )
30 1 20 28 29 4syl 
 |-  ( ph -> ran H = B )
31 30 raleqdv 
 |-  ( ph -> ( A. y e. ran H ( B i^i ( `' S " { y } ) ) e. _V <-> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V ) )
32 27 31 bitr3d 
 |-  ( ph -> ( A. z e. A ( B i^i ( `' S " { ( H ` z ) } ) ) e. _V <-> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V ) )
33 19 32 sylibd 
 |-  ( ph -> ( R Se A -> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V ) )
34 dfse2 
 |-  ( S Se B <-> A. y e. B ( B i^i ( `' S " { y } ) ) e. _V )
35 33 34 imbitrrdi 
 |-  ( ph -> ( R Se A -> S Se B ) )