Metamath Proof Explorer

Theorem rnelfmlem

Description: Lemma for rnelfm . (Contributed by Jeff Hankins, 14-Nov-2009)

Ref Expression
Assertion rnelfmlem 
|- ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> Y e. A )
2 cnvimass 
 |-  ( `' F " x ) C_ dom F
3 simpl3 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> F : Y --> X )
4 2 3 fssdm 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( `' F " x ) C_ Y )
5 1 4 sselpwd 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( `' F " x ) e. ~P Y )
6 5 adantr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) -> ( `' F " x ) e. ~P Y )
7 6 fmpttd 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( x e. L |-> ( `' F " x ) ) : L --> ~P Y )
8 7 frnd 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ran ( x e. L |-> ( `' F " x ) ) C_ ~P Y )
9 filtop 
 |-  ( L e. ( Fil ` X ) -> X e. L )
10 9 3ad2ant2 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> X e. L )
11 10 adantr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> X e. L )
12 fimacnv 
 |-  ( F : Y --> X -> ( `' F " X ) = Y )
13 12 eqcomd 
 |-  ( F : Y --> X -> Y = ( `' F " X ) )
14 13 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> Y = ( `' F " X ) )
15 14 adantr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> Y = ( `' F " X ) )
16 imaeq2 
 |-  ( x = X -> ( `' F " x ) = ( `' F " X ) )
17 16 rspceeqv 
 |-  ( ( X e. L /\ Y = ( `' F " X ) ) -> E. x e. L Y = ( `' F " x ) )
18 11 15 17 syl2anc 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> E. x e. L Y = ( `' F " x ) )
19 eqid 
 |-  ( x e. L |-> ( `' F " x ) ) = ( x e. L |-> ( `' F " x ) )
20 19 elrnmpt 
 |-  ( Y e. A -> ( Y e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L Y = ( `' F " x ) ) )
21 20 3ad2ant1 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( Y e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L Y = ( `' F " x ) ) )
22 21 adantr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( Y e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L Y = ( `' F " x ) ) )
23 18 22 mpbird 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> Y e. ran ( x e. L |-> ( `' F " x ) ) )
24 23 ne0d 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ran ( x e. L |-> ( `' F " x ) ) =/= (/) )
25 0nelfil 
 |-  ( L e. ( Fil ` X ) -> -. (/) e. L )
26 25 3ad2ant2 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> -. (/) e. L )
27 26 adantr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> -. (/) e. L )
28 0ex 
 |-  (/) e. _V
29 19 elrnmpt 
 |-  ( (/) e. _V -> ( (/) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L (/) = ( `' F " x ) ) )
30 28 29 ax-mp 
 |-  ( (/) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L (/) = ( `' F " x ) )
31 ffn 
 |-  ( F : Y --> X -> F Fn Y )
32 fvelrnb 
 |-  ( F Fn Y -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) )
33 31 32 syl 
 |-  ( F : Y --> X -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) )
34 33 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) )
35 34 ad2antrr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) )
36 eleq1 
 |-  ( ( F ` z ) = y -> ( ( F ` z ) e. x <-> y e. x ) )
37 36 biimparc 
 |-  ( ( y e. x /\ ( F ` z ) = y ) -> ( F ` z ) e. x )
38 37 ad2ant2l 
 |-  ( ( ( x e. L /\ y e. x ) /\ ( z e. Y /\ ( F ` z ) = y ) ) -> ( F ` z ) e. x )
39 38 adantll 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) /\ ( z e. Y /\ ( F ` z ) = y ) ) -> ( F ` z ) e. x )
40 ffun 
 |-  ( F : Y --> X -> Fun F )
41 40 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> Fun F )
42 41 ad3antrrr 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) /\ ( z e. Y /\ ( F ` z ) = y ) ) -> Fun F )
43 fdm 
 |-  ( F : Y --> X -> dom F = Y )
44 43 eleq2d 
 |-  ( F : Y --> X -> ( z e. dom F <-> z e. Y ) )
45 44 biimpar 
 |-  ( ( F : Y --> X /\ z e. Y ) -> z e. dom F )
46 45 3ad2antl3 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ z e. Y ) -> z e. dom F )
47 46 adantlr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ z e. Y ) -> z e. dom F )
48 47 ad2ant2r 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) /\ ( z e. Y /\ ( F ` z ) = y ) ) -> z e. dom F )
49 fvimacnv 
 |-  ( ( Fun F /\ z e. dom F ) -> ( ( F ` z ) e. x <-> z e. ( `' F " x ) ) )
50 42 48 49 syl2anc 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) /\ ( z e. Y /\ ( F ` z ) = y ) ) -> ( ( F ` z ) e. x <-> z e. ( `' F " x ) ) )
51 39 50 mpbid 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) /\ ( z e. Y /\ ( F ` z ) = y ) ) -> z e. ( `' F " x ) )
52 n0i 
 |-  ( z e. ( `' F " x ) -> -. ( `' F " x ) = (/) )
53 eqcom 
 |-  ( ( `' F " x ) = (/) <-> (/) = ( `' F " x ) )
54 52 53 sylnib 
 |-  ( z e. ( `' F " x ) -> -. (/) = ( `' F " x ) )
55 51 54 syl 
 |-  ( ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) /\ ( z e. Y /\ ( F ` z ) = y ) ) -> -. (/) = ( `' F " x ) )
56 55 rexlimdvaa 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) -> ( E. z e. Y ( F ` z ) = y -> -. (/) = ( `' F " x ) ) )
57 35 56 sylbid 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) -> ( y e. ran F -> -. (/) = ( `' F " x ) ) )
58 57 con2d 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ y e. x ) ) -> ( (/) = ( `' F " x ) -> -. y e. ran F ) )
59 58 expr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) -> ( y e. x -> ( (/) = ( `' F " x ) -> -. y e. ran F ) ) )
60 59 com23 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ x e. L ) -> ( (/) = ( `' F " x ) -> ( y e. x -> -. y e. ran F ) ) )
61 60 impr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> ( y e. x -> -. y e. ran F ) )
62 61 alrimiv 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> A. y ( y e. x -> -. y e. ran F ) )
63 imnan 
 |-  ( ( y e. x -> -. y e. ran F ) <-> -. ( y e. x /\ y e. ran F ) )
64 elin 
 |-  ( y e. ( x i^i ran F ) <-> ( y e. x /\ y e. ran F ) )
65 63 64 xchbinxr 
 |-  ( ( y e. x -> -. y e. ran F ) <-> -. y e. ( x i^i ran F ) )
66 65 albii 
 |-  ( A. y ( y e. x -> -. y e. ran F ) <-> A. y -. y e. ( x i^i ran F ) )
67 eq0 
 |-  ( ( x i^i ran F ) = (/) <-> A. y -. y e. ( x i^i ran F ) )
68 eqcom 
 |-  ( ( x i^i ran F ) = (/) <-> (/) = ( x i^i ran F ) )
69 66 67 68 3bitr2i 
 |-  ( A. y ( y e. x -> -. y e. ran F ) <-> (/) = ( x i^i ran F ) )
70 62 69 sylib 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> (/) = ( x i^i ran F ) )
71 simpll2 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> L e. ( Fil ` X ) )
72 simprl 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> x e. L )
73 simplr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> ran F e. L )
74 filin 
 |-  ( ( L e. ( Fil ` X ) /\ x e. L /\ ran F e. L ) -> ( x i^i ran F ) e. L )
75 71 72 73 74 syl3anc 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> ( x i^i ran F ) e. L )
76 70 75 eqeltrd 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( x e. L /\ (/) = ( `' F " x ) ) ) -> (/) e. L )
77 76 rexlimdvaa 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( E. x e. L (/) = ( `' F " x ) -> (/) e. L ) )
78 30 77 syl5bi 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( (/) e. ran ( x e. L |-> ( `' F " x ) ) -> (/) e. L ) )
79 27 78 mtod 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> -. (/) e. ran ( x e. L |-> ( `' F " x ) ) )
80 df-nel 
 |-  ( (/) e/ ran ( x e. L |-> ( `' F " x ) ) <-> -. (/) e. ran ( x e. L |-> ( `' F " x ) ) )
81 79 80 sylibr 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> (/) e/ ran ( x e. L |-> ( `' F " x ) ) )
82 19 elrnmpt 
 |-  ( r e. _V -> ( r e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L r = ( `' F " x ) ) )
83 82 elv 
 |-  ( r e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L r = ( `' F " x ) )
84 imaeq2 
 |-  ( x = u -> ( `' F " x ) = ( `' F " u ) )
85 84 eqeq2d 
 |-  ( x = u -> ( r = ( `' F " x ) <-> r = ( `' F " u ) ) )
86 85 cbvrexvw 
 |-  ( E. x e. L r = ( `' F " x ) <-> E. u e. L r = ( `' F " u ) )
87 83 86 bitri 
 |-  ( r e. ran ( x e. L |-> ( `' F " x ) ) <-> E. u e. L r = ( `' F " u ) )
88 19 elrnmpt 
 |-  ( s e. _V -> ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) ) )
89 88 elv 
 |-  ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L s = ( `' F " x ) )
90 imaeq2 
 |-  ( x = v -> ( `' F " x ) = ( `' F " v ) )
91 90 eqeq2d 
 |-  ( x = v -> ( s = ( `' F " x ) <-> s = ( `' F " v ) ) )
92 91 cbvrexvw 
 |-  ( E. x e. L s = ( `' F " x ) <-> E. v e. L s = ( `' F " v ) )
93 89 92 bitri 
 |-  ( s e. ran ( x e. L |-> ( `' F " x ) ) <-> E. v e. L s = ( `' F " v ) )
94 87 93 anbi12i 
 |-  ( ( r e. ran ( x e. L |-> ( `' F " x ) ) /\ s e. ran ( x e. L |-> ( `' F " x ) ) ) <-> ( E. u e. L r = ( `' F " u ) /\ E. v e. L s = ( `' F " v ) ) )
95 reeanv 
 |-  ( E. u e. L E. v e. L ( r = ( `' F " u ) /\ s = ( `' F " v ) ) <-> ( E. u e. L r = ( `' F " u ) /\ E. v e. L s = ( `' F " v ) ) )
96 94 95 bitr4i 
 |-  ( ( r e. ran ( x e. L |-> ( `' F " x ) ) /\ s e. ran ( x e. L |-> ( `' F " x ) ) ) <-> E. u e. L E. v e. L ( r = ( `' F " u ) /\ s = ( `' F " v ) ) )
97 filin 
 |-  ( ( L e. ( Fil ` X ) /\ u e. L /\ v e. L ) -> ( u i^i v ) e. L )
98 97 3expb 
 |-  ( ( L e. ( Fil ` X ) /\ ( u e. L /\ v e. L ) ) -> ( u i^i v ) e. L )
99 98 adantlr 
 |-  ( ( ( L e. ( Fil ` X ) /\ F : Y --> X ) /\ ( u e. L /\ v e. L ) ) -> ( u i^i v ) e. L )
100 eqidd 
 |-  ( ( ( L e. ( Fil ` X ) /\ F : Y --> X ) /\ ( u e. L /\ v e. L ) ) -> ( `' F " ( u i^i v ) ) = ( `' F " ( u i^i v ) ) )
101 imaeq2 
 |-  ( x = ( u i^i v ) -> ( `' F " x ) = ( `' F " ( u i^i v ) ) )
102 101 rspceeqv 
 |-  ( ( ( u i^i v ) e. L /\ ( `' F " ( u i^i v ) ) = ( `' F " ( u i^i v ) ) ) -> E. x e. L ( `' F " ( u i^i v ) ) = ( `' F " x ) )
103 99 100 102 syl2anc 
 |-  ( ( ( L e. ( Fil ` X ) /\ F : Y --> X ) /\ ( u e. L /\ v e. L ) ) -> E. x e. L ( `' F " ( u i^i v ) ) = ( `' F " x ) )
104 103 3adantl1 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ( u e. L /\ v e. L ) ) -> E. x e. L ( `' F " ( u i^i v ) ) = ( `' F " x ) )
105 104 ad2ant2r 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> E. x e. L ( `' F " ( u i^i v ) ) = ( `' F " x ) )
106 simpll1 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> Y e. A )
107 cnvimass 
 |-  ( `' F " ( u i^i v ) ) C_ dom F
108 107 43 sseqtrid 
 |-  ( F : Y --> X -> ( `' F " ( u i^i v ) ) C_ Y )
109 108 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( `' F " ( u i^i v ) ) C_ Y )
110 109 ad2antrr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( `' F " ( u i^i v ) ) C_ Y )
111 106 110 ssexd 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( `' F " ( u i^i v ) ) e. _V )
112 19 elrnmpt 
 |-  ( ( `' F " ( u i^i v ) ) e. _V -> ( ( `' F " ( u i^i v ) ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " ( u i^i v ) ) = ( `' F " x ) ) )
113 111 112 syl 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( ( `' F " ( u i^i v ) ) e. ran ( x e. L |-> ( `' F " x ) ) <-> E. x e. L ( `' F " ( u i^i v ) ) = ( `' F " x ) ) )
114 105 113 mpbird 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( `' F " ( u i^i v ) ) e. ran ( x e. L |-> ( `' F " x ) ) )
115 simprrl 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> r = ( `' F " u ) )
116 simprrr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> s = ( `' F " v ) )
117 115 116 ineq12d 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( r i^i s ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
118 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
119 imain 
 |-  ( Fun `' `' F -> ( `' F " ( u i^i v ) ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
120 40 118 119 3syl 
 |-  ( F : Y --> X -> ( `' F " ( u i^i v ) ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
121 120 3ad2ant3 
 |-  ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) -> ( `' F " ( u i^i v ) ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
122 121 ad2antrr 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( `' F " ( u i^i v ) ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
123 117 122 eqtr4d 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( r i^i s ) = ( `' F " ( u i^i v ) ) )
124 eqimss2 
 |-  ( ( r i^i s ) = ( `' F " ( u i^i v ) ) -> ( `' F " ( u i^i v ) ) C_ ( r i^i s ) )
125 123 124 syl 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> ( `' F " ( u i^i v ) ) C_ ( r i^i s ) )
126 sseq1 
 |-  ( t = ( `' F " ( u i^i v ) ) -> ( t C_ ( r i^i s ) <-> ( `' F " ( u i^i v ) ) C_ ( r i^i s ) ) )
127 126 rspcev 
 |-  ( ( ( `' F " ( u i^i v ) ) e. ran ( x e. L |-> ( `' F " x ) ) /\ ( `' F " ( u i^i v ) ) C_ ( r i^i s ) ) -> E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) )
128 114 125 127 syl2anc 
 |-  ( ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) /\ ( ( u e. L /\ v e. L ) /\ ( r = ( `' F " u ) /\ s = ( `' F " v ) ) ) ) -> E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) )
129 128 exp32 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( ( u e. L /\ v e. L ) -> ( ( r = ( `' F " u ) /\ s = ( `' F " v ) ) -> E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) ) ) )
130 129 rexlimdvv 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( E. u e. L E. v e. L ( r = ( `' F " u ) /\ s = ( `' F " v ) ) -> E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) ) )
131 96 130 syl5bi 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( ( r e. ran ( x e. L |-> ( `' F " x ) ) /\ s e. ran ( x e. L |-> ( `' F " x ) ) ) -> E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) ) )
132 131 ralrimivv 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> A. r e. ran ( x e. L |-> ( `' F " x ) ) A. s e. ran ( x e. L |-> ( `' F " x ) ) E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) )
133 24 81 132 3jca 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( ran ( x e. L |-> ( `' F " x ) ) =/= (/) /\ (/) e/ ran ( x e. L |-> ( `' F " x ) ) /\ A. r e. ran ( x e. L |-> ( `' F " x ) ) A. s e. ran ( x e. L |-> ( `' F " x ) ) E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) ) )
134 isfbas2 
 |-  ( Y e. A -> ( ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) <-> ( ran ( x e. L |-> ( `' F " x ) ) C_ ~P Y /\ ( ran ( x e. L |-> ( `' F " x ) ) =/= (/) /\ (/) e/ ran ( x e. L |-> ( `' F " x ) ) /\ A. r e. ran ( x e. L |-> ( `' F " x ) ) A. s e. ran ( x e. L |-> ( `' F " x ) ) E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) ) ) ) )
135 1 134 syl 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ( ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) <-> ( ran ( x e. L |-> ( `' F " x ) ) C_ ~P Y /\ ( ran ( x e. L |-> ( `' F " x ) ) =/= (/) /\ (/) e/ ran ( x e. L |-> ( `' F " x ) ) /\ A. r e. ran ( x e. L |-> ( `' F " x ) ) A. s e. ran ( x e. L |-> ( `' F " x ) ) E. t e. ran ( x e. L |-> ( `' F " x ) ) t C_ ( r i^i s ) ) ) ) )
136 8 133 135 mpbir2and 
 |-  ( ( ( Y e. A /\ L e. ( Fil ` X ) /\ F : Y --> X ) /\ ran F e. L ) -> ran ( x e. L |-> ( `' F " x ) ) e. ( fBas ` Y ) )