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 ) ) ) )