Metamath Proof Explorer

Theorem isofrlem

Description: Lemma for isofr . (Contributed by NM, 29-Apr-2004) (Revised by Mario Carneiro, 18-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 isofrlem.1 
 |-  ( ph -> H Isom R , S ( A , B ) )
2 isofrlem.2 
 |-  ( ph -> ( H " x ) e. _V )
3 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
4 1 3 syl 
 |-  ( ph -> H : A -1-1-onto-> B )
5 f1ofn 
 |-  ( H : A -1-1-onto-> B -> H Fn A )
6 n0 
 |-  ( x =/= (/) <-> E. y y e. x )
7 fnfvima 
 |-  ( ( H Fn A /\ x C_ A /\ y e. x ) -> ( H ` y ) e. ( H " x ) )
8 7 ne0d 
 |-  ( ( H Fn A /\ x C_ A /\ y e. x ) -> ( H " x ) =/= (/) )
9 8 3expia 
 |-  ( ( H Fn A /\ x C_ A ) -> ( y e. x -> ( H " x ) =/= (/) ) )
10 9 exlimdv 
 |-  ( ( H Fn A /\ x C_ A ) -> ( E. y y e. x -> ( H " x ) =/= (/) ) )
11 6 10 syl5bi 
 |-  ( ( H Fn A /\ x C_ A ) -> ( x =/= (/) -> ( H " x ) =/= (/) ) )
12 11 expimpd 
 |-  ( H Fn A -> ( ( x C_ A /\ x =/= (/) ) -> ( H " x ) =/= (/) ) )
13 5 12 syl 
 |-  ( H : A -1-1-onto-> B -> ( ( x C_ A /\ x =/= (/) ) -> ( H " x ) =/= (/) ) )
14 f1ofo 
 |-  ( H : A -1-1-onto-> B -> H : A -onto-> B )
15 imassrn 
 |-  ( H " x ) C_ ran H
16 forn 
 |-  ( H : A -onto-> B -> ran H = B )
17 15 16 sseqtrid 
 |-  ( H : A -onto-> B -> ( H " x ) C_ B )
18 14 17 syl 
 |-  ( H : A -1-1-onto-> B -> ( H " x ) C_ B )
19 13 18 jctild 
 |-  ( H : A -1-1-onto-> B -> ( ( x C_ A /\ x =/= (/) ) -> ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) ) )
20 4 19 syl 
 |-  ( ph -> ( ( x C_ A /\ x =/= (/) ) -> ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) ) )
21 dffr3 
 |-  ( S Fr B <-> A. z ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) )
22 sseq1 
 |-  ( z = ( H " x ) -> ( z C_ B <-> ( H " x ) C_ B ) )
23 neeq1 
 |-  ( z = ( H " x ) -> ( z =/= (/) <-> ( H " x ) =/= (/) ) )
24 22 23 anbi12d 
 |-  ( z = ( H " x ) -> ( ( z C_ B /\ z =/= (/) ) <-> ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) ) )
25 ineq1 
 |-  ( z = ( H " x ) -> ( z i^i ( `' S " { w } ) ) = ( ( H " x ) i^i ( `' S " { w } ) ) )
26 25 eqeq1d 
 |-  ( z = ( H " x ) -> ( ( z i^i ( `' S " { w } ) ) = (/) <-> ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) )
27 26 rexeqbi1dv 
 |-  ( z = ( H " x ) -> ( E. w e. z ( z i^i ( `' S " { w } ) ) = (/) <-> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) )
28 24 27 imbi12d 
 |-  ( z = ( H " x ) -> ( ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) <-> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
29 28 spcgv 
 |-  ( ( H " x ) e. _V -> ( A. z ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) -> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
30 2 29 syl 
 |-  ( ph -> ( A. z ( ( z C_ B /\ z =/= (/) ) -> E. w e. z ( z i^i ( `' S " { w } ) ) = (/) ) -> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
31 21 30 syl5bi 
 |-  ( ph -> ( S Fr B -> ( ( ( H " x ) C_ B /\ ( H " x ) =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
32 20 31 syl5d 
 |-  ( ph -> ( S Fr B -> ( ( x C_ A /\ x =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) )
33 4 adantr 
 |-  ( ( ph /\ x C_ A ) -> H : A -1-1-onto-> B )
34 f1ofun 
 |-  ( H : A -1-1-onto-> B -> Fun H )
35 33 34 syl 
 |-  ( ( ph /\ x C_ A ) -> Fun H )
36 simpl 
 |-  ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> w e. ( H " x ) )
37 fvelima 
 |-  ( ( Fun H /\ w e. ( H " x ) ) -> E. y e. x ( H ` y ) = w )
38 35 36 37 syl2an 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> E. y e. x ( H ` y ) = w )
39 simpr 
 |-  ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( ( H " x ) i^i ( `' S " { w } ) ) = (/) )
40 ssel 
 |-  ( x C_ A -> ( y e. x -> y e. A ) )
41 40 imdistani 
 |-  ( ( x C_ A /\ y e. x ) -> ( x C_ A /\ y e. A ) )
42 isomin 
 |-  ( ( H Isom R , S ( A , B ) /\ ( x C_ A /\ y e. A ) ) -> ( ( x i^i ( `' R " { y } ) ) = (/) <-> ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) ) )
43 1 41 42 syl2an 
 |-  ( ( ph /\ ( x C_ A /\ y e. x ) ) -> ( ( x i^i ( `' R " { y } ) ) = (/) <-> ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) ) )
44 sneq 
 |-  ( ( H ` y ) = w -> { ( H ` y ) } = { w } )
45 44 imaeq2d 
 |-  ( ( H ` y ) = w -> ( `' S " { ( H ` y ) } ) = ( `' S " { w } ) )
46 45 ineq2d 
 |-  ( ( H ` y ) = w -> ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = ( ( H " x ) i^i ( `' S " { w } ) ) )
47 46 eqeq1d 
 |-  ( ( H ` y ) = w -> ( ( ( H " x ) i^i ( `' S " { ( H ` y ) } ) ) = (/) <-> ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) )
48 43 47 sylan9bb 
 |-  ( ( ( ph /\ ( x C_ A /\ y e. x ) ) /\ ( H ` y ) = w ) -> ( ( x i^i ( `' R " { y } ) ) = (/) <-> ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) )
49 39 48 syl5ibr 
 |-  ( ( ( ph /\ ( x C_ A /\ y e. x ) ) /\ ( H ` y ) = w ) -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) )
50 49 exp42 
 |-  ( ph -> ( x C_ A -> ( y e. x -> ( ( H ` y ) = w -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) ) )
51 50 imp 
 |-  ( ( ph /\ x C_ A ) -> ( y e. x -> ( ( H ` y ) = w -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) )
52 51 com3l 
 |-  ( y e. x -> ( ( H ` y ) = w -> ( ( ph /\ x C_ A ) -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) )
53 52 com4t 
 |-  ( ( ph /\ x C_ A ) -> ( ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( y e. x -> ( ( H ` y ) = w -> ( x i^i ( `' R " { y } ) ) = (/) ) ) ) )
54 53 imp 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> ( y e. x -> ( ( H ` y ) = w -> ( x i^i ( `' R " { y } ) ) = (/) ) ) )
55 54 reximdvai 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> ( E. y e. x ( H ` y ) = w -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
56 38 55 mpd 
 |-  ( ( ( ph /\ x C_ A ) /\ ( w e. ( H " x ) /\ ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) )
57 56 rexlimdvaa 
 |-  ( ( ph /\ x C_ A ) -> ( E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
58 57 ex 
 |-  ( ph -> ( x C_ A -> ( E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
59 58 adantrd 
 |-  ( ph -> ( ( x C_ A /\ x =/= (/) ) -> ( E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
60 59 a2d 
 |-  ( ph -> ( ( ( x C_ A /\ x =/= (/) ) -> E. w e. ( H " x ) ( ( H " x ) i^i ( `' S " { w } ) ) = (/) ) -> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
61 32 60 syld 
 |-  ( ph -> ( S Fr B -> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
62 61 alrimdv 
 |-  ( ph -> ( S Fr B -> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) ) )
63 dffr3 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
64 62 63 syl6ibr 
 |-  ( ph -> ( S Fr B -> R Fr A ) )