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 0fi 
 |-  (/) 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 bitrid 
 |-  ( 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 ) )