Metamath Proof Explorer

Theorem fbasrn

Description: Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis fbasrn.c 
|- C = ran ( x e. B |-> ( F " x ) )
Assertion fbasrn 
|- ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> C e. ( fBas ` Y ) )

Proof

Step Hyp Ref Expression
1 fbasrn.c 
 |-  C = ran ( x e. B |-> ( F " x ) )
2 simpl3 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x e. B ) -> Y e. V )
3 simpl2 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x e. B ) -> F : X --> Y )
4 fimass 
 |-  ( F : X --> Y -> ( F " x ) C_ Y )
5 3 4 syl 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x e. B ) -> ( F " x ) C_ Y )
6 2 5 sselpwd 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x e. B ) -> ( F " x ) e. ~P Y )
7 6 fmpttd 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( x e. B |-> ( F " x ) ) : B --> ~P Y )
8 7 frnd 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ran ( x e. B |-> ( F " x ) ) C_ ~P Y )
9 1 8 eqsstrid 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> C C_ ~P Y )
10 1 a1i 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> C = ran ( x e. B |-> ( F " x ) ) )
11 ffun 
 |-  ( F : X --> Y -> Fun F )
12 11 3ad2ant2 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> Fun F )
13 funimaexg 
 |-  ( ( Fun F /\ x e. B ) -> ( F " x ) e. _V )
14 13 ralrimiva 
 |-  ( Fun F -> A. x e. B ( F " x ) e. _V )
15 dmmptg 
 |-  ( A. x e. B ( F " x ) e. _V -> dom ( x e. B |-> ( F " x ) ) = B )
16 12 14 15 3syl 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> dom ( x e. B |-> ( F " x ) ) = B )
17 fbasne0 
 |-  ( B e. ( fBas ` X ) -> B =/= (/) )
18 17 3ad2ant1 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> B =/= (/) )
19 16 18 eqnetrd 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> dom ( x e. B |-> ( F " x ) ) =/= (/) )
20 dm0rn0 
 |-  ( dom ( x e. B |-> ( F " x ) ) = (/) <-> ran ( x e. B |-> ( F " x ) ) = (/) )
21 20 necon3bii 
 |-  ( dom ( x e. B |-> ( F " x ) ) =/= (/) <-> ran ( x e. B |-> ( F " x ) ) =/= (/) )
22 19 21 sylib 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ran ( x e. B |-> ( F " x ) ) =/= (/) )
23 10 22 eqnetrd 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> C =/= (/) )
24 fbelss 
 |-  ( ( B e. ( fBas ` X ) /\ x e. B ) -> x C_ X )
25 24 ex 
 |-  ( B e. ( fBas ` X ) -> ( x e. B -> x C_ X ) )
26 25 3ad2ant1 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( x e. B -> x C_ X ) )
27 0nelfb 
 |-  ( B e. ( fBas ` X ) -> -. (/) e. B )
28 eleq1 
 |-  ( x = (/) -> ( x e. B <-> (/) e. B ) )
29 28 notbid 
 |-  ( x = (/) -> ( -. x e. B <-> -. (/) e. B ) )
30 27 29 syl5ibrcom 
 |-  ( B e. ( fBas ` X ) -> ( x = (/) -> -. x e. B ) )
31 30 con2d 
 |-  ( B e. ( fBas ` X ) -> ( x e. B -> -. x = (/) ) )
32 31 3ad2ant1 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( x e. B -> -. x = (/) ) )
33 26 32 jcad 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( x e. B -> ( x C_ X /\ -. x = (/) ) ) )
34 fdm 
 |-  ( F : X --> Y -> dom F = X )
35 34 3ad2ant2 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> dom F = X )
36 35 sseq2d 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( x C_ dom F <-> x C_ X ) )
37 36 biimpar 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x C_ X ) -> x C_ dom F )
38 sseqin2 
 |-  ( x C_ dom F <-> ( dom F i^i x ) = x )
39 37 38 sylib 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x C_ X ) -> ( dom F i^i x ) = x )
40 39 eqeq1d 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x C_ X ) -> ( ( dom F i^i x ) = (/) <-> x = (/) ) )
41 40 biimpd 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x C_ X ) -> ( ( dom F i^i x ) = (/) -> x = (/) ) )
42 41 con3d 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ x C_ X ) -> ( -. x = (/) -> -. ( dom F i^i x ) = (/) ) )
43 42 expimpd 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( ( x C_ X /\ -. x = (/) ) -> -. ( dom F i^i x ) = (/) ) )
44 eqcom 
 |-  ( (/) = ( F " x ) <-> ( F " x ) = (/) )
45 imadisj 
 |-  ( ( F " x ) = (/) <-> ( dom F i^i x ) = (/) )
46 44 45 bitri 
 |-  ( (/) = ( F " x ) <-> ( dom F i^i x ) = (/) )
47 46 notbii 
 |-  ( -. (/) = ( F " x ) <-> -. ( dom F i^i x ) = (/) )
48 43 47 imbitrrdi 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( ( x C_ X /\ -. x = (/) ) -> -. (/) = ( F " x ) ) )
49 33 48 syld 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( x e. B -> -. (/) = ( F " x ) ) )
50 49 ralrimiv 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> A. x e. B -. (/) = ( F " x ) )
51 1 eleq2i 
 |-  ( (/) e. C <-> (/) e. ran ( x e. B |-> ( F " x ) ) )
52 0ex 
 |-  (/) e. _V
53 eqid 
 |-  ( x e. B |-> ( F " x ) ) = ( x e. B |-> ( F " x ) )
54 53 elrnmpt 
 |-  ( (/) e. _V -> ( (/) e. ran ( x e. B |-> ( F " x ) ) <-> E. x e. B (/) = ( F " x ) ) )
55 52 54 ax-mp 
 |-  ( (/) e. ran ( x e. B |-> ( F " x ) ) <-> E. x e. B (/) = ( F " x ) )
56 51 55 bitri 
 |-  ( (/) e. C <-> E. x e. B (/) = ( F " x ) )
57 56 notbii 
 |-  ( -. (/) e. C <-> -. E. x e. B (/) = ( F " x ) )
58 df-nel 
 |-  ( (/) e/ C <-> -. (/) e. C )
59 ralnex 
 |-  ( A. x e. B -. (/) = ( F " x ) <-> -. E. x e. B (/) = ( F " x ) )
60 57 58 59 3bitr4i 
 |-  ( (/) e/ C <-> A. x e. B -. (/) = ( F " x ) )
61 50 60 sylibr 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> (/) e/ C )
62 1 eleq2i 
 |-  ( r e. C <-> r e. ran ( x e. B |-> ( F " x ) ) )
63 imaeq2 
 |-  ( x = u -> ( F " x ) = ( F " u ) )
64 63 cbvmptv 
 |-  ( x e. B |-> ( F " x ) ) = ( u e. B |-> ( F " u ) )
65 64 elrnmpt 
 |-  ( r e. _V -> ( r e. ran ( x e. B |-> ( F " x ) ) <-> E. u e. B r = ( F " u ) ) )
66 65 elv 
 |-  ( r e. ran ( x e. B |-> ( F " x ) ) <-> E. u e. B r = ( F " u ) )
67 62 66 bitri 
 |-  ( r e. C <-> E. u e. B r = ( F " u ) )
68 1 eleq2i 
 |-  ( s e. C <-> s e. ran ( x e. B |-> ( F " x ) ) )
69 imaeq2 
 |-  ( x = v -> ( F " x ) = ( F " v ) )
70 69 cbvmptv 
 |-  ( x e. B |-> ( F " x ) ) = ( v e. B |-> ( F " v ) )
71 70 elrnmpt 
 |-  ( s e. _V -> ( s e. ran ( x e. B |-> ( F " x ) ) <-> E. v e. B s = ( F " v ) ) )
72 71 elv 
 |-  ( s e. ran ( x e. B |-> ( F " x ) ) <-> E. v e. B s = ( F " v ) )
73 68 72 bitri 
 |-  ( s e. C <-> E. v e. B s = ( F " v ) )
74 67 73 anbi12i 
 |-  ( ( r e. C /\ s e. C ) <-> ( E. u e. B r = ( F " u ) /\ E. v e. B s = ( F " v ) ) )
75 reeanv 
 |-  ( E. u e. B E. v e. B ( r = ( F " u ) /\ s = ( F " v ) ) <-> ( E. u e. B r = ( F " u ) /\ E. v e. B s = ( F " v ) ) )
76 74 75 bitr4i 
 |-  ( ( r e. C /\ s e. C ) <-> E. u e. B E. v e. B ( r = ( F " u ) /\ s = ( F " v ) ) )
77 fbasssin 
 |-  ( ( B e. ( fBas ` X ) /\ u e. B /\ v e. B ) -> E. w e. B w C_ ( u i^i v ) )
78 77 3expb 
 |-  ( ( B e. ( fBas ` X ) /\ ( u e. B /\ v e. B ) ) -> E. w e. B w C_ ( u i^i v ) )
79 78 3ad2antl1 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( u e. B /\ v e. B ) ) -> E. w e. B w C_ ( u i^i v ) )
80 79 adantrr 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( ( u e. B /\ v e. B ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) ) -> E. w e. B w C_ ( u i^i v ) )
81 eqid 
 |-  ( F " w ) = ( F " w )
82 imaeq2 
 |-  ( x = w -> ( F " x ) = ( F " w ) )
83 82 rspceeqv 
 |-  ( ( w e. B /\ ( F " w ) = ( F " w ) ) -> E. x e. B ( F " w ) = ( F " x ) )
84 81 83 mpan2 
 |-  ( w e. B -> E. x e. B ( F " w ) = ( F " x ) )
85 84 ad2antrl 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> E. x e. B ( F " w ) = ( F " x ) )
86 1 eleq2i 
 |-  ( ( F " w ) e. C <-> ( F " w ) e. ran ( x e. B |-> ( F " x ) ) )
87 vex 
 |-  w e. _V
88 87 funimaex 
 |-  ( Fun F -> ( F " w ) e. _V )
89 53 elrnmpt 
 |-  ( ( F " w ) e. _V -> ( ( F " w ) e. ran ( x e. B |-> ( F " x ) ) <-> E. x e. B ( F " w ) = ( F " x ) ) )
90 12 88 89 3syl 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( ( F " w ) e. ran ( x e. B |-> ( F " x ) ) <-> E. x e. B ( F " w ) = ( F " x ) ) )
91 86 90 bitrid 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( ( F " w ) e. C <-> E. x e. B ( F " w ) = ( F " x ) ) )
92 91 ad2antrr 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> ( ( F " w ) e. C <-> E. x e. B ( F " w ) = ( F " x ) ) )
93 85 92 mpbird 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> ( F " w ) e. C )
94 imass2 
 |-  ( w C_ ( u i^i v ) -> ( F " w ) C_ ( F " ( u i^i v ) ) )
95 94 ad2antll 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> ( F " w ) C_ ( F " ( u i^i v ) ) )
96 inss1 
 |-  ( u i^i v ) C_ u
97 imass2 
 |-  ( ( u i^i v ) C_ u -> ( F " ( u i^i v ) ) C_ ( F " u ) )
98 96 97 ax-mp 
 |-  ( F " ( u i^i v ) ) C_ ( F " u )
99 inss2 
 |-  ( u i^i v ) C_ v
100 imass2 
 |-  ( ( u i^i v ) C_ v -> ( F " ( u i^i v ) ) C_ ( F " v ) )
101 99 100 ax-mp 
 |-  ( F " ( u i^i v ) ) C_ ( F " v )
102 98 101 ssini 
 |-  ( F " ( u i^i v ) ) C_ ( ( F " u ) i^i ( F " v ) )
103 ineq12 
 |-  ( ( r = ( F " u ) /\ s = ( F " v ) ) -> ( r i^i s ) = ( ( F " u ) i^i ( F " v ) ) )
104 103 ad2antlr 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> ( r i^i s ) = ( ( F " u ) i^i ( F " v ) ) )
105 102 104 sseqtrrid 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> ( F " ( u i^i v ) ) C_ ( r i^i s ) )
106 95 105 sstrd 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> ( F " w ) C_ ( r i^i s ) )
107 sseq1 
 |-  ( z = ( F " w ) -> ( z C_ ( r i^i s ) <-> ( F " w ) C_ ( r i^i s ) ) )
108 107 rspcev 
 |-  ( ( ( F " w ) e. C /\ ( F " w ) C_ ( r i^i s ) ) -> E. z e. C z C_ ( r i^i s ) )
109 93 106 108 syl2anc 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> E. z e. C z C_ ( r i^i s ) )
110 109 adantlrl 
 |-  ( ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( ( u e. B /\ v e. B ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) ) /\ ( w e. B /\ w C_ ( u i^i v ) ) ) -> E. z e. C z C_ ( r i^i s ) )
111 80 110 rexlimddv 
 |-  ( ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) /\ ( ( u e. B /\ v e. B ) /\ ( r = ( F " u ) /\ s = ( F " v ) ) ) ) -> E. z e. C z C_ ( r i^i s ) )
112 111 exp32 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( ( u e. B /\ v e. B ) -> ( ( r = ( F " u ) /\ s = ( F " v ) ) -> E. z e. C z C_ ( r i^i s ) ) ) )
113 112 rexlimdvv 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( E. u e. B E. v e. B ( r = ( F " u ) /\ s = ( F " v ) ) -> E. z e. C z C_ ( r i^i s ) ) )
114 76 113 biimtrid 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( ( r e. C /\ s e. C ) -> E. z e. C z C_ ( r i^i s ) ) )
115 114 ralrimivv 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> A. r e. C A. s e. C E. z e. C z C_ ( r i^i s ) )
116 23 61 115 3jca 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( C =/= (/) /\ (/) e/ C /\ A. r e. C A. s e. C E. z e. C z C_ ( r i^i s ) ) )
117 isfbas2 
 |-  ( Y e. V -> ( C e. ( fBas ` Y ) <-> ( C C_ ~P Y /\ ( C =/= (/) /\ (/) e/ C /\ A. r e. C A. s e. C E. z e. C z C_ ( r i^i s ) ) ) ) )
118 117 3ad2ant3 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> ( C e. ( fBas ` Y ) <-> ( C C_ ~P Y /\ ( C =/= (/) /\ (/) e/ C /\ A. r e. C A. s e. C E. z e. C z C_ ( r i^i s ) ) ) ) )
119 9 116 118 mpbir2and 
 |-  ( ( B e. ( fBas ` X ) /\ F : X --> Y /\ Y e. V ) -> C e. ( fBas ` Y ) )