Metamath Proof Explorer

Theorem fmfnfmlem2

Description: Lemma for fmfnfm . (Contributed by Jeff Hankins, 19-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypotheses fmfnfm.b 
|- ( ph -> B e. ( fBas ` Y ) )
fmfnfm.l 
|- ( ph -> L e. ( Fil ` X ) )
fmfnfm.f 
|- ( ph -> F : Y --> X )
fmfnfm.fm 
|- ( ph -> ( ( X FilMap F ) ` B ) C_ L )
Assertion fmfnfmlem2 
|- ( ph -> ( E. x e. L s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )

Proof

Step Hyp Ref Expression
1 fmfnfm.b 
 |-  ( ph -> B e. ( fBas ` Y ) )
2 fmfnfm.l 
 |-  ( ph -> L e. ( Fil ` X ) )
3 fmfnfm.f 
 |-  ( ph -> F : Y --> X )
4 fmfnfm.fm 
 |-  ( ph -> ( ( X FilMap F ) ` B ) C_ L )
5 2 ad2antrr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> L e. ( Fil ` X ) )
6 simplr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> x e. L )
7 ffn 
 |-  ( F : Y --> X -> F Fn Y )
8 dffn4 
 |-  ( F Fn Y <-> F : Y -onto-> ran F )
9 7 8 sylib 
 |-  ( F : Y --> X -> F : Y -onto-> ran F )
10 foima 
 |-  ( F : Y -onto-> ran F -> ( F " Y ) = ran F )
11 3 9 10 3syl 
 |-  ( ph -> ( F " Y ) = ran F )
12 filtop 
 |-  ( L e. ( Fil ` X ) -> X e. L )
13 2 12 syl 
 |-  ( ph -> X e. L )
14 fgcl 
 |-  ( B e. ( fBas ` Y ) -> ( Y filGen B ) e. ( Fil ` Y ) )
15 filtop 
 |-  ( ( Y filGen B ) e. ( Fil ` Y ) -> Y e. ( Y filGen B ) )
16 1 14 15 3syl 
 |-  ( ph -> Y e. ( Y filGen B ) )
17 eqid 
 |-  ( Y filGen B ) = ( Y filGen B )
18 17 imaelfm 
 |-  ( ( ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ Y e. ( Y filGen B ) ) -> ( F " Y ) e. ( ( X FilMap F ) ` B ) )
19 13 1 3 16 18 syl31anc 
 |-  ( ph -> ( F " Y ) e. ( ( X FilMap F ) ` B ) )
20 11 19 eqeltrrd 
 |-  ( ph -> ran F e. ( ( X FilMap F ) ` B ) )
21 4 20 sseldd 
 |-  ( ph -> ran F e. L )
22 21 ad2antrr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ran F e. L )
23 filin 
 |-  ( ( L e. ( Fil ` X ) /\ x e. L /\ ran F e. L ) -> ( x i^i ran F ) e. L )
24 5 6 22 23 syl3anc 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( x i^i ran F ) e. L )
25 simprr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> t C_ X )
26 elin 
 |-  ( y e. ( x i^i ran F ) <-> ( y e. x /\ y e. ran F ) )
27 fvelrnb 
 |-  ( F Fn Y -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) )
28 3 7 27 3syl 
 |-  ( ph -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) )
29 28 ad2antrr 
 |-  ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) )
30 3 ffund 
 |-  ( ph -> Fun F )
31 30 ad2antrr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> Fun F )
32 simprr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> z e. Y )
33 3 fdmd 
 |-  ( ph -> dom F = Y )
34 33 ad2antrr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> dom F = Y )
35 32 34 eleqtrrd 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> z e. dom F )
36 fvimacnv 
 |-  ( ( Fun F /\ z e. dom F ) -> ( ( F ` z ) e. x <-> z e. ( `' F " x ) ) )
37 31 35 36 syl2anc 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) e. x <-> z e. ( `' F " x ) ) )
38 cnvimass 
 |-  ( `' F " x ) C_ dom F
39 funfvima2 
 |-  ( ( Fun F /\ ( `' F " x ) C_ dom F ) -> ( z e. ( `' F " x ) -> ( F ` z ) e. ( F " ( `' F " x ) ) ) )
40 31 38 39 sylancl 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( z e. ( `' F " x ) -> ( F ` z ) e. ( F " ( `' F " x ) ) ) )
41 ssel 
 |-  ( ( F " ( `' F " x ) ) C_ t -> ( ( F ` z ) e. ( F " ( `' F " x ) ) -> ( F ` z ) e. t ) )
42 41 ad2antrl 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) e. ( F " ( `' F " x ) ) -> ( F ` z ) e. t ) )
43 40 42 syld 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( z e. ( `' F " x ) -> ( F ` z ) e. t ) )
44 37 43 sylbid 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) e. x -> ( F ` z ) e. t ) )
45 eleq1 
 |-  ( ( F ` z ) = y -> ( ( F ` z ) e. x <-> y e. x ) )
46 eleq1 
 |-  ( ( F ` z ) = y -> ( ( F ` z ) e. t <-> y e. t ) )
47 45 46 imbi12d 
 |-  ( ( F ` z ) = y -> ( ( ( F ` z ) e. x -> ( F ` z ) e. t ) <-> ( y e. x -> y e. t ) ) )
48 44 47 syl5ibcom 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) = y -> ( y e. x -> y e. t ) ) )
49 48 expr 
 |-  ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( z e. Y -> ( ( F ` z ) = y -> ( y e. x -> y e. t ) ) ) )
50 49 rexlimdv 
 |-  ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( E. z e. Y ( F ` z ) = y -> ( y e. x -> y e. t ) ) )
51 29 50 sylbid 
 |-  ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( y e. ran F -> ( y e. x -> y e. t ) ) )
52 51 impcomd 
 |-  ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( ( y e. x /\ y e. ran F ) -> y e. t ) )
53 52 adantrr 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( ( y e. x /\ y e. ran F ) -> y e. t ) )
54 26 53 syl5bi 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( y e. ( x i^i ran F ) -> y e. t ) )
55 54 ssrdv 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( x i^i ran F ) C_ t )
56 filss 
 |-  ( ( L e. ( Fil ` X ) /\ ( ( x i^i ran F ) e. L /\ t C_ X /\ ( x i^i ran F ) C_ t ) ) -> t e. L )
57 5 24 25 55 56 syl13anc 
 |-  ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> t e. L )
58 57 exp32 
 |-  ( ( ph /\ x e. L ) -> ( ( F " ( `' F " x ) ) C_ t -> ( t C_ X -> t e. L ) ) )
59 imaeq2 
 |-  ( s = ( `' F " x ) -> ( F " s ) = ( F " ( `' F " x ) ) )
60 59 sseq1d 
 |-  ( s = ( `' F " x ) -> ( ( F " s ) C_ t <-> ( F " ( `' F " x ) ) C_ t ) )
61 60 imbi1d 
 |-  ( s = ( `' F " x ) -> ( ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) <-> ( ( F " ( `' F " x ) ) C_ t -> ( t C_ X -> t e. L ) ) ) )
62 58 61 syl5ibrcom 
 |-  ( ( ph /\ x e. L ) -> ( s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
63 62 rexlimdva 
 |-  ( ph -> ( E. x e. L s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )