Metamath Proof Explorer

Theorem rnelfm

Description: A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion rnelfm 
|- ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( L e. ran ( X FilMap F ) <-> ran F e. L ) )

Proof

Step Hyp Ref Expression
1 filtop 
 |-  ( L e. ( Fil ` X ) -> X e. L )
2 1 3ad2ant2 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> X e. L )
3 simp1 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> Y e. A )
4 simp3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> F : Y --> X )
5 fmf 
 |-  ( ( X e. L /\ Y e. A /\ F : Y --> X ) -> ( X FilMap F ) : ( fBas ` Y ) --> ( Fil ` X ) )
6 2 3 4 5 syl3anc 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( X FilMap F ) : ( fBas ` Y ) --> ( Fil ` X ) )
7 6 ffnd 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( X FilMap F ) Fn ( fBas ` Y ) )
8 fvelrnb 
 |-  ( ( X FilMap F ) Fn ( fBas ` Y ) -> ( L e. ran ( X FilMap F ) <-> E. b e. ( fBas ` Y ) ( ( X FilMap F ) ` b ) = L ) )
9 7 8 syl 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( L e. ran ( X FilMap F ) <-> E. b e. ( fBas ` Y ) ( ( X FilMap F ) ` b ) = L ) )
10 ffn 
 |-  ( F : Y --> X -> F Fn Y )
11 dffn4 
 |-  ( F Fn Y <-> F : Y -onto-> ran F )
12 10 11 sylib 
 |-  ( F : Y --> X -> F : Y -onto-> ran F )
13 foima 
 |-  ( F : Y -onto-> ran F -> ( F " Y ) = ran F )
14 12 13 syl 
 |-  ( F : Y --> X -> ( F " Y ) = ran F )
15 14 ad2antlr 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> ( F " Y ) = ran F )
16 simpll 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> X e. L )
17 simpr 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> b e. ( fBas ` Y ) )
18 simplr 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> F : Y --> X )
19 fgcl 
 |-  ( b e. ( fBas ` Y ) -> ( Y filGen b ) e. ( Fil ` Y ) )
20 filtop 
 |-  ( ( Y filGen b ) e. ( Fil ` Y ) -> Y e. ( Y filGen b ) )
21 19 20 syl 
 |-  ( b e. ( fBas ` Y ) -> Y e. ( Y filGen b ) )
22 21 adantl 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> Y e. ( Y filGen b ) )
23 eqid 
 |-  ( Y filGen b ) = ( Y filGen b )
24 23 imaelfm 
 |-  ( ( ( X e. L /\ b e. ( fBas ` Y ) /\ F : Y --> X ) /\ Y e. ( Y filGen b ) ) -> ( F " Y ) e. ( ( X FilMap F ) ` b ) )
25 16 17 18 22 24 syl31anc 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> ( F " Y ) e. ( ( X FilMap F ) ` b ) )
26 15 25 eqeltrrd 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> ran F e. ( ( X FilMap F ) ` b ) )
27 eleq2 
 |-  ( ( ( X FilMap F ) ` b ) = L -> ( ran F e. ( ( X FilMap F ) ` b ) <-> ran F e. L ) )
28 26 27 syl5ibcom 
 |-  ( ( ( X e. L /\ F : Y --> X ) /\ b e. ( fBas ` Y ) ) -> ( ( ( X FilMap F ) ` b ) = L -> ran F e. L ) )
29 28 ex 
 |-  ( ( X e. L /\ F : Y --> X ) -> ( b e. ( fBas ` Y ) -> ( ( ( X FilMap F ) ` b ) = L -> ran F e. L ) ) )
30 1 29 sylan 
 |-  ( ( L e. ( Fil ` X ) /\ F : Y --> X ) -> ( b e. ( fBas ` Y ) -> ( ( ( X FilMap F ) ` b ) = L -> ran F e. L ) ) )
31 30 3adant1 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( b e. ( fBas ` Y ) -> ( ( ( X FilMap F ) ` b ) = L -> ran F e. L ) ) )
32 31 rexlimdv 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( E. b e. ( fBas ` Y ) ( ( X FilMap F ) ` b ) = L -> ran F e. L ) )
33 9 32 sylbid 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( L e. ran ( X FilMap F ) -> ran F e. L ) )
34 simpl2 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> L e. ( Fil ` X ) )
35 filelss 
 |-  ( ( L e. ( Fil ` X ) /\ t e. L ) -> t C_ X )
36 35 ex 
 |-  ( L e. ( Fil ` X ) -> ( t e. L -> t C_ X ) )
37 34 36 syl 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( t e. L -> t C_ X ) )
38 simpr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> t e. L )
39 eqidd 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> ( `' F " t ) = ( `' F " t ) )
40 imaeq2 
 |-  ( x = t -> ( `' F " x ) = ( `' F " t ) )
41 40 rspceeqv 
 |-  ( ( t e. L /\ ( `' F " t ) = ( `' F " t ) ) -> E. x e. L ( `' F " t ) = ( `' F " x ) )
42 38 39 41 syl2anc 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> E. x e. L ( `' F " t ) = ( `' F " x ) )
43 simpl1 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> Y e. A )
44 cnvimass 
 |-  ( `' F " t ) C_ dom F
45 fdm 
 |-  ( F : Y --> X -> dom F = Y )
46 44 45 sseqtrid 
 |-  ( F : Y --> X -> ( `' F " t ) C_ Y )
47 46 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( `' F " t ) C_ Y )
48 47 adantr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( `' F " t ) C_ Y )
49 43 48 ssexd 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( `' F " t ) e. _V )
50 eqid 
 |-  ( x e. L |-> ( `' F " x ) ) = ( x e. L |-> ( `' F " x ) )
51 50 elrnmpt 
 |-  ( ( `' F " t ) e. _V -> ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " t ) = ( `' F " x ) ) )
52 49 51 syl 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " t ) = ( `' F " x ) ) )
53 52 adantr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " t ) = ( `' F " x ) ) )
54 42 53 mpbird 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) )
55 ssid 
 |-  ( `' F " t ) C_ ( `' F " t )
56 ffun 
 |-  ( F : Y --> X -> Fun F )
57 56 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> Fun F )
58 57 ad2antrr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> Fun F )
59 funimass3 
 |-  ( ( Fun F /\ ( `' F " t ) C_ dom F ) -> ( ( F " ( `' F " t ) ) C_ t <-> ( `' F " t ) C_ ( `' F " t ) ) )
60 58 44 59 sylancl 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> ( ( F " ( `' F " t ) ) C_ t <-> ( `' F " t ) C_ ( `' F " t ) ) )
61 55 60 mpbiri 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> ( F " ( `' F " t ) ) C_ t )
62 imaeq2 
 |-  ( s = ( `' F " t ) -> ( F " s ) = ( F " ( `' F " t ) ) )
63 62 sseq1d 
 |-  ( s = ( `' F " t ) -> ( ( F " s ) C_ t <-> ( F " ( `' F " t ) ) C_ t ) )
64 63 rspcev 
 |-  ( ( ( `' F " t ) e. ran ( x e. L |-> ( `' F " x ) ) /\ ( F " ( `' F " t ) ) C_ t ) -> E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t )
65 54 61 64 syl2anc 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ t e. L ) -> E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t )
66 65 ex 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( t e. L -> E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t ) )
67 37 66 jcad 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( t e. L -> ( t C_ X /\ E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t ) ) )
68 34 adantr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ ( F " s ) C_ t ) /\ t C_ X ) ) -> L e. ( Fil ` X ) )
69 50 elrnmpt 
 |-  ( s e. _V -> ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) ) )
70 69 elv 
 |-  ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) )
71 ssid 
 |-  ( `' F " x ) C_ ( `' F " x )
72 57 ad3antrrr 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> Fun F )
73 cnvimass 
 |-  ( `' F " x ) C_ dom F
74 funimass3 
 |-  ( ( Fun F /\ ( `' F " x ) C_ dom F ) -> ( ( F " ( `' F " x ) ) C_ x <-> ( `' F " x ) C_ ( `' F " x ) ) )
75 72 73 74 sylancl 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( ( F " ( `' F " x ) ) C_ x <-> ( `' F " x ) C_ ( `' F " x ) ) )
76 71 75 mpbiri 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( F " ( `' F " x ) ) C_ x )
77 imassrn 
 |-  ( F " ( `' F " x ) ) C_ ran F
78 ssin 
 |-  ( ( ( F " ( `' F " x ) ) C_ x /\ ( F " ( `' F " x ) ) C_ ran F ) <-> ( F " ( `' F " x ) ) C_ ( x i^i ran F ) )
79 76 77 78 sylanblc 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( F " ( `' F " x ) ) C_ ( x i^i ran F ) )
80 elin 
 |-  ( z e. ( x i^i ran F ) <-> ( z e. x /\ z e. ran F ) )
81 fvelrnb 
 |-  ( F Fn Y -> ( z e. ran F <-> E. y e. Y ( F ` y ) = z ) )
82 10 81 syl 
 |-  ( F : Y --> X -> ( z e. ran F <-> E. y e. Y ( F ` y ) = z ) )
83 82 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( z e. ran F <-> E. y e. Y ( F ` y ) = z ) )
84 83 ad3antrrr 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( z e. ran F <-> E. y e. Y ( F ` y ) = z ) )
85 72 ad2antrr 
 |-  ( ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) /\ ( F ` y ) e. x ) -> Fun F )
86 85 73 jctir 
 |-  ( ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) /\ ( F ` y ) e. x ) -> ( Fun F /\ ( `' F " x ) C_ dom F ) )
87 57 ad2antrr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) -> Fun F )
88 87 ad2antrr 
 |-  ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) -> Fun F )
89 45 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> dom F = Y )
90 89 ad3antrrr 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> dom F = Y )
91 90 eleq2d 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( y e. dom F <-> y e. Y ) )
92 91 biimpar 
 |-  ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) -> y e. dom F )
93 fvimacnv 
 |-  ( ( Fun F /\ y e. dom F ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
94 88 92 93 syl2anc 
 |-  ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) -> ( ( F ` y ) e. x <-> y e. ( `' F " x ) ) )
95 94 biimpa 
 |-  ( ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) /\ ( F ` y ) e. x ) -> y e. ( `' F " x ) )
96 funfvima2 
 |-  ( ( Fun F /\ ( `' F " x ) C_ dom F ) -> ( y e. ( `' F " x ) -> ( F ` y ) e. ( F " ( `' F " x ) ) ) )
97 86 95 96 sylc 
 |-  ( ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) /\ ( F ` y ) e. x ) -> ( F ` y ) e. ( F " ( `' F " x ) ) )
98 97 ex 
 |-  ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) -> ( ( F ` y ) e. x -> ( F ` y ) e. ( F " ( `' F " x ) ) ) )
99 eleq1 
 |-  ( ( F ` y ) = z -> ( ( F ` y ) e. x <-> z e. x ) )
100 eleq1 
 |-  ( ( F ` y ) = z -> ( ( F ` y ) e. ( F " ( `' F " x ) ) <-> z e. ( F " ( `' F " x ) ) ) )
101 99 100 imbi12d 
 |-  ( ( F ` y ) = z -> ( ( ( F ` y ) e. x -> ( F ` y ) e. ( F " ( `' F " x ) ) ) <-> ( z e. x -> z e. ( F " ( `' F " x ) ) ) ) )
102 98 101 syl5ibcom 
 |-  ( ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) /\ y e. Y ) -> ( ( F ` y ) = z -> ( z e. x -> z e. ( F " ( `' F " x ) ) ) ) )
103 102 rexlimdva 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( E. y e. Y ( F ` y ) = z -> ( z e. x -> z e. ( F " ( `' F " x ) ) ) ) )
104 84 103 sylbid 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( z e. ran F -> ( z e. x -> z e. ( F " ( `' F " x ) ) ) ) )
105 104 impcomd 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( ( z e. x /\ z e. ran F ) -> z e. ( F " ( `' F " x ) ) ) )
106 80 105 syl5bi 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( z e. ( x i^i ran F ) -> z e. ( F " ( `' F " x ) ) ) )
107 106 ssrdv 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( x i^i ran F ) C_ ( F " ( `' F " x ) ) )
108 79 107 eqssd 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( F " ( `' F " x ) ) = ( x i^i ran F ) )
109 filin 
 |-  ( ( L e. ( Fil ` X ) /\ x e. L /\ ran F e. L ) -> ( x i^i ran F ) e. L )
110 109 3exp 
 |-  ( L e. ( Fil ` X ) -> ( x e. L -> ( ran F e. L -> ( x i^i ran F ) e. L ) ) )
111 110 com23 
 |-  ( L e. ( Fil ` X ) -> ( ran F e. L -> ( x e. L -> ( x i^i ran F ) e. L ) ) )
112 111 3ad2ant2 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( ran F e. L -> ( x e. L -> ( x i^i ran F ) e. L ) ) )
113 112 imp31 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) -> ( x i^i ran F ) e. L )
114 113 adantr 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( x i^i ran F ) e. L )
115 108 114 eqeltrd 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( F " ( `' F " x ) ) e. L )
116 115 exp32 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) -> ( ( F " ( `' F " x ) ) C_ t -> ( t C_ X -> ( F " ( `' F " x ) ) e. L ) ) )
117 imaeq2 
 |-  ( s = ( `' F " x ) -> ( F " s ) = ( F " ( `' F " x ) ) )
118 117 sseq1d 
 |-  ( s = ( `' F " x ) -> ( ( F " s ) C_ t <-> ( F " ( `' F " x ) ) C_ t ) )
119 117 eleq1d 
 |-  ( s = ( `' F " x ) -> ( ( F " s ) e. L <-> ( F " ( `' F " x ) ) e. L ) )
120 119 imbi2d 
 |-  ( s = ( `' F " x ) -> ( ( t C_ X -> ( F " s ) e. L ) <-> ( t C_ X -> ( F " ( `' F " x ) ) e. L ) ) )
121 118 120 imbi12d 
 |-  ( s = ( `' F " x ) -> ( ( ( F " s ) C_ t -> ( t C_ X -> ( F " s ) e. L ) ) <-> ( ( F " ( `' F " x ) ) C_ t -> ( t C_ X -> ( F " ( `' F " x ) ) e. L ) ) ) )
122 116 121 syl5ibrcom 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) -> ( s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> ( F " s ) e. L ) ) ) )
123 122 rexlimdva 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( E. x e. L s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> ( F " s ) e. L ) ) ) )
124 70 123 syl5bi 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( s e. ran ( x e. L |-> ( `' F " x ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> ( F " s ) e. L ) ) ) )
125 124 imp44 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ ( F " s ) C_ t ) /\ t C_ X ) ) -> ( F " s ) e. L )
126 simprr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ ( F " s ) C_ t ) /\ t C_ X ) ) -> t C_ X )
127 simprlr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ ( F " s ) C_ t ) /\ t C_ X ) ) -> ( F " s ) C_ t )
128 filss 
 |-  ( ( L e. ( Fil ` X ) /\ ( ( F " s ) e. L /\ t C_ X /\ ( F " s ) C_ t ) ) -> t e. L )
129 68 125 126 127 128 syl13anc 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( s e. ran ( x e. L |-> ( `' F " x ) ) /\ ( F " s ) C_ t ) /\ t C_ X ) ) -> t e. L )
130 129 exp44 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( s e. ran ( x e. L |-> ( `' F " x ) ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) )
131 130 rexlimdv 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) )
132 131 impcomd 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( ( t C_ X /\ E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t ) -> t e. L ) )
133 67 132 impbid 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( t e. L <-> ( t C_ X /\ E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t ) ) )
134 2 adantr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> X e. L )
135 rnelfmlem 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) )
136 simpl3 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> F : Y --> X )
137 elfm 
 |-  ( ( X e. L /\ ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) /\ F : Y --> X ) -> ( t e. ( ( X FilMap F ) ` ran ( x e. L |-> ( `' F " x ) ) ) <-> ( t C_ X /\ E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t ) ) )
138 134 135 136 137 syl3anc 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( t e. ( ( X FilMap F ) ` ran ( x e. L |-> ( `' F " x ) ) ) <-> ( t C_ X /\ E. s e. ran ( x e. L |-> ( `' F " x ) ) ( F " s ) C_ t ) ) )
139 133 138 bitr4d 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( t e. L <-> t e. ( ( X FilMap F ) ` ran ( x e. L |-> ( `' F " x ) ) ) ) )
140 139 eqrdv 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> L = ( ( X FilMap F ) ` ran ( x e. L |-> ( `' F " x ) ) ) )
141 7 adantr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( X FilMap F ) Fn ( fBas ` Y ) )
142 fnfvelrn 
 |-  ( ( ( X FilMap F ) Fn ( fBas ` Y ) /\ ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) ) -> ( ( X FilMap F ) ` ran ( x e. L |-> ( `' F " x ) ) ) e. ran ( X FilMap F ) )
143 141 135 142 syl2anc 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( ( X FilMap F ) ` ran ( x e. L |-> ( `' F " x ) ) ) e. ran ( X FilMap F ) )
144 140 143 eqeltrd 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> L e. ran ( X FilMap F ) )
145 144 ex 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( ran F e. L -> L e. ran ( X FilMap F ) ) )
146 33 145 impbid 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( L e. ran ( X FilMap F ) <-> ran F e. L ) )