Metamath Proof Explorer


Theorem tsmsfbas

Description: The collection of all sets of the form F ( z ) = { y e. S | z C_ y } , which can be read as the set of all finite subsets of A which contain z as a subset, for each finite subset z of A , form a filter base. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmsfbas.s
|- S = ( ~P A i^i Fin )
tsmsfbas.f
|- F = ( z e. S |-> { y e. S | z C_ y } )
tsmsfbas.l
|- L = ran F
tsmsfbas.a
|- ( ph -> A e. W )
Assertion tsmsfbas
|- ( ph -> L e. ( fBas ` S ) )

Proof

Step Hyp Ref Expression
1 tsmsfbas.s
 |-  S = ( ~P A i^i Fin )
2 tsmsfbas.f
 |-  F = ( z e. S |-> { y e. S | z C_ y } )
3 tsmsfbas.l
 |-  L = ran F
4 tsmsfbas.a
 |-  ( ph -> A e. W )
5 elex
 |-  ( A e. W -> A e. _V )
6 ssrab2
 |-  { y e. S | z C_ y } C_ S
7 pwexg
 |-  ( A e. _V -> ~P A e. _V )
8 inex1g
 |-  ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
9 7 8 syl
 |-  ( A e. _V -> ( ~P A i^i Fin ) e. _V )
10 1 9 eqeltrid
 |-  ( A e. _V -> S e. _V )
11 10 adantr
 |-  ( ( A e. _V /\ z e. S ) -> S e. _V )
12 elpw2g
 |-  ( S e. _V -> ( { y e. S | z C_ y } e. ~P S <-> { y e. S | z C_ y } C_ S ) )
13 11 12 syl
 |-  ( ( A e. _V /\ z e. S ) -> ( { y e. S | z C_ y } e. ~P S <-> { y e. S | z C_ y } C_ S ) )
14 6 13 mpbiri
 |-  ( ( A e. _V /\ z e. S ) -> { y e. S | z C_ y } e. ~P S )
15 14 2 fmptd
 |-  ( A e. _V -> F : S --> ~P S )
16 15 frnd
 |-  ( A e. _V -> ran F C_ ~P S )
17 0ss
 |-  (/) C_ A
18 0fin
 |-  (/) e. Fin
19 elfpw
 |-  ( (/) e. ( ~P A i^i Fin ) <-> ( (/) C_ A /\ (/) e. Fin ) )
20 17 18 19 mpbir2an
 |-  (/) e. ( ~P A i^i Fin )
21 20 1 eleqtrri
 |-  (/) e. S
22 0ss
 |-  (/) C_ y
23 22 rgenw
 |-  A. y e. S (/) C_ y
24 rabid2
 |-  ( S = { y e. S | z C_ y } <-> A. y e. S z C_ y )
25 sseq1
 |-  ( z = (/) -> ( z C_ y <-> (/) C_ y ) )
26 25 ralbidv
 |-  ( z = (/) -> ( A. y e. S z C_ y <-> A. y e. S (/) C_ y ) )
27 24 26 syl5bb
 |-  ( z = (/) -> ( S = { y e. S | z C_ y } <-> A. y e. S (/) C_ y ) )
28 27 rspcev
 |-  ( ( (/) e. S /\ A. y e. S (/) C_ y ) -> E. z e. S S = { y e. S | z C_ y } )
29 21 23 28 mp2an
 |-  E. z e. S S = { y e. S | z C_ y }
30 2 elrnmpt
 |-  ( S e. _V -> ( S e. ran F <-> E. z e. S S = { y e. S | z C_ y } ) )
31 10 30 syl
 |-  ( A e. _V -> ( S e. ran F <-> E. z e. S S = { y e. S | z C_ y } ) )
32 29 31 mpbiri
 |-  ( A e. _V -> S e. ran F )
33 32 ne0d
 |-  ( A e. _V -> ran F =/= (/) )
34 simpr
 |-  ( ( A e. _V /\ z e. S ) -> z e. S )
35 ssid
 |-  z C_ z
36 sseq2
 |-  ( y = z -> ( z C_ y <-> z C_ z ) )
37 36 rspcev
 |-  ( ( z e. S /\ z C_ z ) -> E. y e. S z C_ y )
38 34 35 37 sylancl
 |-  ( ( A e. _V /\ z e. S ) -> E. y e. S z C_ y )
39 rabn0
 |-  ( { y e. S | z C_ y } =/= (/) <-> E. y e. S z C_ y )
40 38 39 sylibr
 |-  ( ( A e. _V /\ z e. S ) -> { y e. S | z C_ y } =/= (/) )
41 40 necomd
 |-  ( ( A e. _V /\ z e. S ) -> (/) =/= { y e. S | z C_ y } )
42 41 neneqd
 |-  ( ( A e. _V /\ z e. S ) -> -. (/) = { y e. S | z C_ y } )
43 42 nrexdv
 |-  ( A e. _V -> -. E. z e. S (/) = { y e. S | z C_ y } )
44 0ex
 |-  (/) e. _V
45 2 elrnmpt
 |-  ( (/) e. _V -> ( (/) e. ran F <-> E. z e. S (/) = { y e. S | z C_ y } ) )
46 44 45 ax-mp
 |-  ( (/) e. ran F <-> E. z e. S (/) = { y e. S | z C_ y } )
47 43 46 sylnibr
 |-  ( A e. _V -> -. (/) e. ran F )
48 df-nel
 |-  ( (/) e/ ran F <-> -. (/) e. ran F )
49 47 48 sylibr
 |-  ( A e. _V -> (/) e/ ran F )
50 elfpw
 |-  ( u e. ( ~P A i^i Fin ) <-> ( u C_ A /\ u e. Fin ) )
51 50 simplbi
 |-  ( u e. ( ~P A i^i Fin ) -> u C_ A )
52 51 1 eleq2s
 |-  ( u e. S -> u C_ A )
53 elfpw
 |-  ( v e. ( ~P A i^i Fin ) <-> ( v C_ A /\ v e. Fin ) )
54 53 simplbi
 |-  ( v e. ( ~P A i^i Fin ) -> v C_ A )
55 54 1 eleq2s
 |-  ( v e. S -> v C_ A )
56 52 55 anim12i
 |-  ( ( u e. S /\ v e. S ) -> ( u C_ A /\ v C_ A ) )
57 unss
 |-  ( ( u C_ A /\ v C_ A ) <-> ( u u. v ) C_ A )
58 56 57 sylib
 |-  ( ( u e. S /\ v e. S ) -> ( u u. v ) C_ A )
59 elinel2
 |-  ( u e. ( ~P A i^i Fin ) -> u e. Fin )
60 59 1 eleq2s
 |-  ( u e. S -> u e. Fin )
61 elinel2
 |-  ( v e. ( ~P A i^i Fin ) -> v e. Fin )
62 61 1 eleq2s
 |-  ( v e. S -> v e. Fin )
63 unfi
 |-  ( ( u e. Fin /\ v e. Fin ) -> ( u u. v ) e. Fin )
64 60 62 63 syl2an
 |-  ( ( u e. S /\ v e. S ) -> ( u u. v ) e. Fin )
65 elfpw
 |-  ( ( u u. v ) e. ( ~P A i^i Fin ) <-> ( ( u u. v ) C_ A /\ ( u u. v ) e. Fin ) )
66 58 64 65 sylanbrc
 |-  ( ( u e. S /\ v e. S ) -> ( u u. v ) e. ( ~P A i^i Fin ) )
67 66 adantl
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( u u. v ) e. ( ~P A i^i Fin ) )
68 67 1 eleqtrrdi
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( u u. v ) e. S )
69 eqidd
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } = { y e. S | ( u u. v ) C_ y } )
70 sseq1
 |-  ( a = ( u u. v ) -> ( a C_ y <-> ( u u. v ) C_ y ) )
71 70 rabbidv
 |-  ( a = ( u u. v ) -> { y e. S | a C_ y } = { y e. S | ( u u. v ) C_ y } )
72 71 rspceeqv
 |-  ( ( ( u u. v ) e. S /\ { y e. S | ( u u. v ) C_ y } = { y e. S | ( u u. v ) C_ y } ) -> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } )
73 68 69 72 syl2anc
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } )
74 10 adantr
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> S e. _V )
75 rabexg
 |-  ( S e. _V -> { y e. S | ( u u. v ) C_ y } e. _V )
76 74 75 syl
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } e. _V )
77 sseq1
 |-  ( z = a -> ( z C_ y <-> a C_ y ) )
78 77 rabbidv
 |-  ( z = a -> { y e. S | z C_ y } = { y e. S | a C_ y } )
79 78 cbvmptv
 |-  ( z e. S |-> { y e. S | z C_ y } ) = ( a e. S |-> { y e. S | a C_ y } )
80 2 79 eqtri
 |-  F = ( a e. S |-> { y e. S | a C_ y } )
81 80 elrnmpt
 |-  ( { y e. S | ( u u. v ) C_ y } e. _V -> ( { y e. S | ( u u. v ) C_ y } e. ran F <-> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } ) )
82 76 81 syl
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( { y e. S | ( u u. v ) C_ y } e. ran F <-> E. a e. S { y e. S | ( u u. v ) C_ y } = { y e. S | a C_ y } ) )
83 73 82 mpbird
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } e. ran F )
84 pwidg
 |-  ( { y e. S | ( u u. v ) C_ y } e. _V -> { y e. S | ( u u. v ) C_ y } e. ~P { y e. S | ( u u. v ) C_ y } )
85 76 84 syl
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> { y e. S | ( u u. v ) C_ y } e. ~P { y e. S | ( u u. v ) C_ y } )
86 inelcm
 |-  ( ( { y e. S | ( u u. v ) C_ y } e. ran F /\ { y e. S | ( u u. v ) C_ y } e. ~P { y e. S | ( u u. v ) C_ y } ) -> ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) )
87 83 85 86 syl2anc
 |-  ( ( A e. _V /\ ( u e. S /\ v e. S ) ) -> ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) )
88 87 ralrimivva
 |-  ( A e. _V -> A. u e. S A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) )
89 rabexg
 |-  ( S e. _V -> { y e. S | u C_ y } e. _V )
90 10 89 syl
 |-  ( A e. _V -> { y e. S | u C_ y } e. _V )
91 90 ralrimivw
 |-  ( A e. _V -> A. u e. S { y e. S | u C_ y } e. _V )
92 sseq1
 |-  ( z = u -> ( z C_ y <-> u C_ y ) )
93 92 rabbidv
 |-  ( z = u -> { y e. S | z C_ y } = { y e. S | u C_ y } )
94 93 cbvmptv
 |-  ( z e. S |-> { y e. S | z C_ y } ) = ( u e. S |-> { y e. S | u C_ y } )
95 2 94 eqtri
 |-  F = ( u e. S |-> { y e. S | u C_ y } )
96 ineq1
 |-  ( a = { y e. S | u C_ y } -> ( a i^i { y e. S | v C_ y } ) = ( { y e. S | u C_ y } i^i { y e. S | v C_ y } ) )
97 inrab
 |-  ( { y e. S | u C_ y } i^i { y e. S | v C_ y } ) = { y e. S | ( u C_ y /\ v C_ y ) }
98 unss
 |-  ( ( u C_ y /\ v C_ y ) <-> ( u u. v ) C_ y )
99 98 rabbii
 |-  { y e. S | ( u C_ y /\ v C_ y ) } = { y e. S | ( u u. v ) C_ y }
100 97 99 eqtri
 |-  ( { y e. S | u C_ y } i^i { y e. S | v C_ y } ) = { y e. S | ( u u. v ) C_ y }
101 96 100 eqtrdi
 |-  ( a = { y e. S | u C_ y } -> ( a i^i { y e. S | v C_ y } ) = { y e. S | ( u u. v ) C_ y } )
102 101 pweqd
 |-  ( a = { y e. S | u C_ y } -> ~P ( a i^i { y e. S | v C_ y } ) = ~P { y e. S | ( u u. v ) C_ y } )
103 102 ineq2d
 |-  ( a = { y e. S | u C_ y } -> ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) = ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) )
104 103 neeq1d
 |-  ( a = { y e. S | u C_ y } -> ( ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) )
105 104 ralbidv
 |-  ( a = { y e. S | u C_ y } -> ( A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) )
106 95 105 ralrnmptw
 |-  ( A. u e. S { y e. S | u C_ y } e. _V -> ( A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> A. u e. S A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) )
107 91 106 syl
 |-  ( A e. _V -> ( A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) <-> A. u e. S A. v e. S ( ran F i^i ~P { y e. S | ( u u. v ) C_ y } ) =/= (/) ) )
108 88 107 mpbird
 |-  ( A e. _V -> A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) )
109 rabexg
 |-  ( S e. _V -> { y e. S | v C_ y } e. _V )
110 10 109 syl
 |-  ( A e. _V -> { y e. S | v C_ y } e. _V )
111 110 ralrimivw
 |-  ( A e. _V -> A. v e. S { y e. S | v C_ y } e. _V )
112 sseq1
 |-  ( z = v -> ( z C_ y <-> v C_ y ) )
113 112 rabbidv
 |-  ( z = v -> { y e. S | z C_ y } = { y e. S | v C_ y } )
114 113 cbvmptv
 |-  ( z e. S |-> { y e. S | z C_ y } ) = ( v e. S |-> { y e. S | v C_ y } )
115 2 114 eqtri
 |-  F = ( v e. S |-> { y e. S | v C_ y } )
116 ineq2
 |-  ( b = { y e. S | v C_ y } -> ( a i^i b ) = ( a i^i { y e. S | v C_ y } ) )
117 116 pweqd
 |-  ( b = { y e. S | v C_ y } -> ~P ( a i^i b ) = ~P ( a i^i { y e. S | v C_ y } ) )
118 117 ineq2d
 |-  ( b = { y e. S | v C_ y } -> ( ran F i^i ~P ( a i^i b ) ) = ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) )
119 118 neeq1d
 |-  ( b = { y e. S | v C_ y } -> ( ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) )
120 115 119 ralrnmptw
 |-  ( A. v e. S { y e. S | v C_ y } e. _V -> ( A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) )
121 111 120 syl
 |-  ( A e. _V -> ( A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) )
122 121 ralbidv
 |-  ( A e. _V -> ( A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) <-> A. a e. ran F A. v e. S ( ran F i^i ~P ( a i^i { y e. S | v C_ y } ) ) =/= (/) ) )
123 108 122 mpbird
 |-  ( A e. _V -> A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) )
124 33 49 123 3jca
 |-  ( A e. _V -> ( ran F =/= (/) /\ (/) e/ ran F /\ A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) ) )
125 isfbas
 |-  ( S e. _V -> ( ran F e. ( fBas ` S ) <-> ( ran F C_ ~P S /\ ( ran F =/= (/) /\ (/) e/ ran F /\ A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) ) ) ) )
126 10 125 syl
 |-  ( A e. _V -> ( ran F e. ( fBas ` S ) <-> ( ran F C_ ~P S /\ ( ran F =/= (/) /\ (/) e/ ran F /\ A. a e. ran F A. b e. ran F ( ran F i^i ~P ( a i^i b ) ) =/= (/) ) ) ) )
127 16 124 126 mpbir2and
 |-  ( A e. _V -> ran F e. ( fBas ` S ) )
128 3 127 eqeltrid
 |-  ( A e. _V -> L e. ( fBas ` S ) )
129 4 5 128 3syl
 |-  ( ph -> L e. ( fBas ` S ) )