Metamath Proof Explorer

Theorem flimclslem

Description: Lemma for flimcls . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis flimcls.2 
|- F = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )
Assertion flimclslem 
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( F e. ( Fil ` X ) /\ S e. F /\ A e. ( J fLim F ) ) )

Proof

Step Hyp Ref Expression
1 flimcls.2 
 |-  F = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )
2 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
3 2 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> J e. Top )
4 eqid 
 |-  U. J = U. J
5 4 neisspw 
 |-  ( J e. Top -> ( ( nei ` J ) ` { A } ) C_ ~P U. J )
6 3 5 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P U. J )
7 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
8 7 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> X = U. J )
9 8 pweqd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ~P X = ~P U. J )
10 6 9 sseqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P X )
11 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
12 elpw2g 
 |-  ( X e. J -> ( S e. ~P X <-> S C_ X ) )
13 11 12 syl 
 |-  ( J e. ( TopOn ` X ) -> ( S e. ~P X <-> S C_ X ) )
14 13 biimpar 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> S e. ~P X )
15 14 3adant3 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. ~P X )
16 15 snssd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { S } C_ ~P X )
17 10 16 unssd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ~P X )
18 ssun2 
 |-  { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } )
19 11 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> X e. J )
20 simp2 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S C_ X )
21 19 20 ssexd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. _V )
22 snnzg 
 |-  ( S e. _V -> { S } =/= (/) )
23 21 22 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { S } =/= (/) )
24 ssn0 
 |-  ( ( { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } ) /\ { S } =/= (/) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) )
25 18 23 24 sylancr 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) )
26 20 8 sseqtrd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S C_ U. J )
27 simp3 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. ( ( cls ` J ) ` S ) )
28 4 neindisj 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ ( A e. ( ( cls ` J ) ` S ) /\ x e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i S ) =/= (/) )
29 28 expr 
 |-  ( ( ( J e. Top /\ S C_ U. J ) /\ A e. ( ( cls ` J ) ` S ) ) -> ( x e. ( ( nei ` J ) ` { A } ) -> ( x i^i S ) =/= (/) ) )
30 3 26 27 29 syl21anc 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( x e. ( ( nei ` J ) ` { A } ) -> ( x i^i S ) =/= (/) ) )
31 30 imp 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) /\ x e. ( ( nei ` J ) ` { A } ) ) -> ( x i^i S ) =/= (/) )
32 elsni 
 |-  ( y e. { S } -> y = S )
33 32 ineq2d 
 |-  ( y e. { S } -> ( x i^i y ) = ( x i^i S ) )
34 33 neeq1d 
 |-  ( y e. { S } -> ( ( x i^i y ) =/= (/) <-> ( x i^i S ) =/= (/) ) )
35 31 34 syl5ibrcom 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) /\ x e. ( ( nei ` J ) ` { A } ) ) -> ( y e. { S } -> ( x i^i y ) =/= (/) ) )
36 35 ralrimiv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) /\ x e. ( ( nei ` J ) ` { A } ) ) -> A. y e. { S } ( x i^i y ) =/= (/) )
37 36 ralrimiva 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A. x e. ( ( nei ` J ) ` { A } ) A. y e. { S } ( x i^i y ) =/= (/) )
38 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> J e. ( TopOn ` X ) )
39 4 clsss3 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
40 3 26 39 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` S ) C_ U. J )
41 40 27 sseldd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. U. J )
42 41 8 eleqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. X )
43 42 snssd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { A } C_ X )
44 snnzg 
 |-  ( A e. ( ( cls ` J ) ` S ) -> { A } =/= (/) )
45 44 3ad2ant3 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { A } =/= (/) )
46 neifil 
 |-  ( ( J e. ( TopOn ` X ) /\ { A } C_ X /\ { A } =/= (/) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
47 38 43 45 46 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
48 filfbas 
 |-  ( ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) )
49 47 48 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) )
50 ne0i 
 |-  ( A e. ( ( cls ` J ) ` S ) -> ( ( cls ` J ) ` S ) =/= (/) )
51 50 3ad2ant3 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` S ) =/= (/) )
52 cls0 
 |-  ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )
53 3 52 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` (/) ) = (/) )
54 51 53 neeqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` S ) =/= ( ( cls ` J ) ` (/) ) )
55 fveq2 
 |-  ( S = (/) -> ( ( cls ` J ) ` S ) = ( ( cls ` J ) ` (/) ) )
56 55 necon3i 
 |-  ( ( ( cls ` J ) ` S ) =/= ( ( cls ` J ) ` (/) ) -> S =/= (/) )
57 54 56 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S =/= (/) )
58 snfbas 
 |-  ( ( S C_ X /\ S =/= (/) /\ X e. J ) -> { S } e. ( fBas ` X ) )
59 20 57 19 58 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { S } e. ( fBas ` X ) )
60 fbunfip 
 |-  ( ( ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) /\ { S } e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) <-> A. x e. ( ( nei ` J ) ` { A } ) A. y e. { S } ( x i^i y ) =/= (/) ) )
61 49 59 60 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) <-> A. x e. ( ( nei ` J ) ` { A } ) A. y e. { S } ( x i^i y ) =/= (/) ) )
62 37 61 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )
63 fsubbas 
 |-  ( X e. J -> ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) <-> ( ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ~P X /\ ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) )
64 19 63 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) <-> ( ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ~P X /\ ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) )
65 17 25 62 64 mpbir3and 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) )
66 fgcl 
 |-  ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) )
67 65 66 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) )
68 1 67 eqeltrid 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> F e. ( Fil ` X ) )
69 fvex 
 |-  ( ( nei ` J ) ` { A } ) e. _V
70 snex 
 |-  { S } e. _V
71 69 70 unex 
 |-  ( ( ( nei ` J ) ` { A } ) u. { S } ) e. _V
72 ssfii 
 |-  ( ( ( ( nei ` J ) ` { A } ) u. { S } ) e. _V -> ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )
73 71 72 ax-mp 
 |-  ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) )
74 ssfg 
 |-  ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) )
75 65 74 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) )
76 75 1 sseqtrrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) C_ F )
77 73 76 sstrid 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ F )
78 snssg 
 |-  ( S e. _V -> ( S e. ( ( ( nei ` J ) ` { A } ) u. { S } ) <-> { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )
79 21 78 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( S e. ( ( ( nei ` J ) ` { A } ) u. { S } ) <-> { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } ) ) )
80 18 79 mpbiri 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. ( ( ( nei ` J ) ` { A } ) u. { S } ) )
81 77 80 sseldd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. F )
82 77 unssad 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) C_ F )
83 elflim 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
84 38 68 83 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
85 42 82 84 mpbir2and 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. ( J fLim F ) )
86 68 81 85 3jca 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( F e. ( Fil ` X ) /\ S e. F /\ A e. ( J fLim F ) ) )