Theorem fclsfnflim 15614

Description: A filter clusters at a point iff a finer filter converges to it.

Hypotheses

Ref	Expression
fclsfnflim.1	|- X = U.J
fclsfnflim.2	|- Y = U.F

Assertion

Ref	Expression
fclsfnflim	|- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fClus` J)` F) <-> E.g e. Fil (X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g))))

Distinct variable groups:   A,g   g,F   g,J   g,X   g,Y

Proof of Theorem fclsfnflim

Step	Hyp	Ref	Expression
1		fvex 4689	. . . . . . . . . 10 |- ((nei` J)` {A}) e. _V
2		unexg 3798	. . . . . . . . . 10 |- ((F e. Fil /\ ((nei` J)` {A}) e. _V) -> (F u. ((nei` J)` {A})) e. _V)
3	1, 2	mpan2 760	. . . . . . . . 9 |- (F e. Fil -> (F u. ((nei` J)` {A})) e. _V)
4	3	3ad2ant2 898	. . . . . . . 8 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (F u. ((nei` J)` {A})) e. _V)
5	4	adantr 425	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (F u. ((nei` J)` {A})) e. _V)
6		fsubbas 10281	. . . . . . 7 |- ((F u. ((nei` J)` {A})) e. _V -> (( fi ` (F u. ((nei` J)` {A}))) e. fBas <-> ((F u. ((nei` J)` {A})) =/= (/) /\ (/) e/ ( fi ` (F u. ((nei` J)` {A}))))))
7	5, 6	syl 12	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (( fi ` (F u. ((nei` J)` {A}))) e. fBas <-> ((F u. ((nei` J)` {A})) =/= (/) /\ (/) e/ ( fi ` (F u. ((nei` J)` {A}))))))
8		fclsfnflim.2	. . . . . . . . . 10 |- Y = U.F
9	8	filusb 10267	. . . . . . . . 9 |- (F e. Fil -> Y e. F)
10		ne0i 2881	. . . . . . . . 9 |- (Y e. F -> F =/= (/))
11		ssun1 2767	. . . . . . . . . 10 |- F C_ (F u. ((nei` J)` {A}))
12		ssn0 2905	. . . . . . . . . 10 |- ((F C_ (F u. ((nei` J)` {A})) /\ F =/= (/)) -> (F u. ((nei` J)` {A})) =/= (/))
13	11, 12	mpan 759	. . . . . . . . 9 |- (F =/= (/) -> (F u. ((nei` J)` {A})) =/= (/))
14	9, 10, 13	3syl 24	. . . . . . . 8 |- (F e. Fil -> (F u. ((nei` J)` {A})) =/= (/))
15	14	3ad2ant2 898	. . . . . . 7 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (F u. ((nei` J)` {A})) =/= (/))
16	15	adantr 425	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (F u. ((nei` J)` {A})) =/= (/))
17		simpl 346	. . . . . . . . . . 11 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ (A e. ((fClus` J)` F) /\ (x e. F /\ y e. ((nei` J)` {A})))) -> (J e. Top /\ F e. Fil /\ X = Y))
18		simprl 450	. . . . . . . . . . 11 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ (A e. ((fClus` J)` F) /\ (x e. F /\ y e. ((nei` J)` {A})))) -> A e. ((fClus` J)` F))
19		simprrr 459	. . . . . . . . . . 11 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ (A e. ((fClus` J)` F) /\ (x e. F /\ y e. ((nei` J)` {A})))) -> y e. ((nei` J)` {A}))
20		simprrl 458	. . . . . . . . . . 11 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ (A e. ((fClus` J)` F) /\ (x e. F /\ y e. ((nei` J)` {A})))) -> x e. F)
21		fclsfnflim.1	. . . . . . . . . . . 12 |- X = U.J
22	21, 8	fclusneii 15609	. . . . . . . . . . 11 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F) /\ y e. ((nei` J)` {A})) /\ x e. F) -> (y i^i x) =/= (/))
23	17, 18, 19, 20, 22	syl31anc 1103	. . . . . . . . . 10 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ (A e. ((fClus` J)` F) /\ (x e. F /\ y e. ((nei` J)` {A})))) -> (y i^i x) =/= (/))
24		incom 2787	. . . . . . . . . . 11 |- (y i^i x) = (x i^i y)
25	24	neeq1i 2026	. . . . . . . . . 10 |- ((y i^i x) =/= (/) <-> (x i^i y) =/= (/))
26	23, 25	sylib 215	. . . . . . . . 9 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ (A e. ((fClus` J)` F) /\ (x e. F /\ y e. ((nei` J)` {A})))) -> (x i^i y) =/= (/))
27	26	expr 418	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ((x e. F /\ y e. ((nei` J)` {A})) -> (x i^i y) =/= (/)))
28	27	r19.21aivv 2183	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> A.x e. F A.y e. ((nei` J)` {A})(x i^i y) =/= (/))
29		filfbas 10276	. . . . . . . . . 10 |- (F e. Fil -> F e. fBas)
30	29	3ad2ant2 898	. . . . . . . . 9 |- ((J e. Top /\ F e. Fil /\ X = Y) -> F e. fBas)
31	30	adantr 425	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> F e. fBas)
32		simp1 876	. . . . . . . . . . 11 |- ((J e. Top /\ F e. Fil /\ X = Y) -> J e. Top)
33	32	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> J e. Top)
34	21, 8	fclselbas 15608	. . . . . . . . . . 11 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> A e. X)
35	34	snssd 3130	. . . . . . . . . 10 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> {A} C_ X)
36		snnzg 3118	. . . . . . . . . . 11 |- (A e. ((fClus` J)` F) -> {A} =/= (/))
37	36	adantl 424	. . . . . . . . . 10 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> {A} =/= (/))
38	21	neifil 10302	. . . . . . . . . 10 |- ((J e. Top /\ {A} C_ X /\ {A} =/= (/)) -> ((nei` J)` {A}) e. Fil)
39	33, 35, 37, 38	syl111anc 1100	. . . . . . . . 9 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ((nei` J)` {A}) e. Fil)
40		filfbas 10276	. . . . . . . . 9 |- (((nei` J)` {A}) e. Fil -> ((nei` J)` {A}) e. fBas)
41	39, 40	syl 12	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ((nei` J)` {A}) e. fBas)
42		fbunfip 10282	. . . . . . . 8 |- ((F e. fBas /\ ((nei` J)` {A}) e. fBas) -> ((/) e/ ( fi ` (F u. ((nei` J)` {A}))) <-> A.x e. F A.y e. ((nei` J)` {A})(x i^i y) =/= (/)))
43	31, 41, 42	syl11anc 524	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ((/) e/ ( fi ` (F u. ((nei` J)` {A}))) <-> A.x e. F A.y e. ((nei` J)` {A})(x i^i y) =/= (/)))
44	28, 43	mpbird 213	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (/) e/ ( fi ` (F u. ((nei` J)` {A}))))
45	7, 16, 44	mpbir2and 802	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ( fi ` (F u. ((nei` J)` {A}))) e. fBas)
46		fgfil 10290	. . . . 5 |- (( fi ` (F u. ((nei` J)` {A}))) e. fBas -> (filGen` ( fi ` (F u. ((nei` J)` {A})))) e. Fil)
47	45, 46	syl 12	. . . 4 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (filGen` ( fi ` (F u. ((nei` J)` {A})))) e. Fil)
48	8	eqeq2i 1894	. . . . . . . . . . 11 |- (X = Y <-> X = U.F)
49	48	biimpi 168	. . . . . . . . . 10 |- (X = Y -> X = U.F)
50	49	3ad2ant3 899	. . . . . . . . 9 |- ((J e. Top /\ F e. Fil /\ X = Y) -> X = U.F)
51	50	adantr 425	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> X = U.F)
52	21	unnei 9011	. . . . . . . . . 10 |- ((J e. Top /\ {A} C_ X) -> U.((nei` J)` {A}) = X)
53	33, 35, 52	syl11anc 524	. . . . . . . . 9 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> U.((nei` J)` {A}) = X)
54	53	eqcomd 1889	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> X = U.((nei` J)` {A}))
55	51, 54	uneq12d 2756	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (X u. X) = (U.F u. U.((nei` J)` {A})))
56		unidm 2743	. . . . . . 7 |- (X u. X) = X
57	55, 56	syl5eqr 1942	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> X = (U.F u. U.((nei` J)` {A})))
58		uniun 3196	. . . . . 6 |- U.(F u. ((nei` J)` {A})) = (U.F u. U.((nei` J)` {A}))
59	57, 58	syl6eqr 1946	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> X = U.(F u. ((nei` J)` {A})))
60		fiuni 10219	. . . . . . . 8 |- ((F u. ((nei` J)` {A})) e. _V -> U.(F u. ((nei` J)` {A})) = U.( fi ` (F u. ((nei` J)` {A}))))
61	3, 60	syl 12	. . . . . . 7 |- (F e. Fil -> U.(F u. ((nei` J)` {A})) = U.( fi ` (F u. ((nei` J)` {A}))))
62	61	3ad2ant2 898	. . . . . 6 |- ((J e. Top /\ F e. Fil /\ X = Y) -> U.(F u. ((nei` J)` {A})) = U.( fi ` (F u. ((nei` J)` {A}))))
63	62	adantr 425	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> U.(F u. ((nei` J)` {A})) = U.( fi ` (F u. ((nei` J)` {A}))))
64		eqid 1884	. . . . . . 7 |- U.( fi ` (F u. ((nei` J)` {A}))) = U.( fi ` (F u. ((nei` J)` {A})))
65	64	fgbas 10286	. . . . . 6 |- (( fi ` (F u. ((nei` J)` {A}))) e. fBas -> U.( fi ` (F u. ((nei` J)` {A}))) = U.(filGen` ( fi ` (F u. ((nei` J)` {A})))))
66	45, 65	syl 12	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> U.( fi ` (F u. ((nei` J)` {A}))) = U.(filGen` ( fi ` (F u. ((nei` J)` {A})))))
67	59, 63, 66	3eqtrd 1929	. . . 4 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> X = U.(filGen` ( fi ` (F u. ((nei` J)` {A})))))
68	11	a1i 8	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> F C_ (F u. ((nei` J)` {A})))
69		abfi2 10216	. . . . . . . . 9 |- ((F u. ((nei` J)` {A})) e. _V -> (F u. ((nei` J)` {A})) C_ ( fi ` (F u. ((nei` J)` {A}))))
70	3, 69	syl 12	. . . . . . . 8 |- (F e. Fil -> (F u. ((nei` J)` {A})) C_ ( fi ` (F u. ((nei` J)` {A}))))
71	70	3ad2ant2 898	. . . . . . 7 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (F u. ((nei` J)` {A})) C_ ( fi ` (F u. ((nei` J)` {A}))))
72	71	adantr 425	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (F u. ((nei` J)` {A})) C_ ( fi ` (F u. ((nei` J)` {A}))))
73	68, 72	sstrd 2627	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> F C_ ( fi ` (F u. ((nei` J)` {A}))))
74		fbssfg 10285	. . . . . 6 |- (( fi ` (F u. ((nei` J)` {A}))) e. fBas -> ( fi ` (F u. ((nei` J)` {A}))) C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))))
75	45, 74	syl 12	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ( fi ` (F u. ((nei` J)` {A}))) C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))))
76	73, 75	sstrd 2627	. . . 4 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> F C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))))
77		eqid 1884	. . . . . . 7 |- U.(filGen` ( fi ` (F u. ((nei` J)` {A})))) = U.(filGen` ( fi ` (F u. ((nei` J)` {A}))))
78	21, 77	isfillim 10298	. . . . . 6 |- ((J e. Top /\ (filGen` ( fi ` (F u. ((nei` J)` {A})))) e. Fil /\ X = U.(filGen` ( fi ` (F u. ((nei` J)` {A}))))) -> (A e. ((fLim1` J)` (filGen` ( fi ` (F u. ((nei` J)` {A}))))) <-> (A e. X /\ ((nei` J)` {A}) C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))))))
79	33, 47, 67, 78	syl111anc 1100	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> (A e. ((fLim1` J)` (filGen` ( fi ` (F u. ((nei` J)` {A}))))) <-> (A e. X /\ ((nei` J)` {A}) C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))))))
80		ssun2 2768	. . . . . . . 8 |- ((nei` J)` {A}) C_ (F u. ((nei` J)` {A}))
81	80	a1i 8	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ((nei` J)` {A}) C_ (F u. ((nei` J)` {A})))
82	81, 72	sstrd 2627	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ((nei` J)` {A}) C_ ( fi ` (F u. ((nei` J)` {A}))))
83	82, 75	sstrd 2627	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> ((nei` J)` {A}) C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))))
84	79, 34, 83	mpbir2and 802	. . . 4 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> A e. ((fLim1` J)` (filGen` ( fi ` (F u. ((nei` J)` {A}))))))
85		unieq 3185	. . . . . . 7 |- (g = (filGen` ( fi ` (F u. ((nei` J)` {A})))) -> U.g = U.(filGen` ( fi ` (F u. ((nei` J)` {A})))))
86	85	eqeq2d 1895	. . . . . 6 |- (g = (filGen` ( fi ` (F u. ((nei` J)` {A})))) -> (X = U.g <-> X = U.(filGen` ( fi ` (F u. ((nei` J)` {A}))))))
87		sseq2 2639	. . . . . 6 |- (g = (filGen` ( fi ` (F u. ((nei` J)` {A})))) -> (F C_ g <-> F C_ (filGen` ( fi ` (F u. ((nei` J)` {A}))))))
88		fveq2 4681	. . . . . . 7 |- (g = (filGen` ( fi ` (F u. ((nei` J)` {A})))) -> ((fLim1` J)` g) = ((fLim1` J)` (filGen` ( fi ` (F u. ((nei` J)` {A}))))))
89	88	eleq2d 1964	. . . . . 6 |- (g = (filGen` ( fi ` (F u. ((nei` J)` {A})))) -> (A e. ((fLim1` J)` g) <-> A e. ((fLim1` J)` (filGen` ( fi ` (F u. ((nei` J)` {A})))))))
90	86, 87, 89	3anbi123d 1168	. . . . 5 |- (g = (filGen` ( fi ` (F u. ((nei` J)` {A})))) -> ((X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g)) <-> (X = U.(filGen` ( fi ` (F u. ((nei` J)` {A})))) /\ F C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))) /\ A e. ((fLim1` J)` (filGen` ( fi ` (F u. ((nei` J)` {A}))))))))
91	90	rcla4ev 2381	. . . 4 |- (((filGen` ( fi ` (F u. ((nei` J)` {A})))) e. Fil /\ (X = U.(filGen` ( fi ` (F u. ((nei` J)` {A})))) /\ F C_ (filGen` ( fi ` (F u. ((nei` J)` {A})))) /\ A e. ((fLim1` J)` (filGen` ( fi ` (F u. ((nei` J)` {A}))))))) -> E.g e. Fil (X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g)))
92	47, 67, 76, 84, 91	syl13anc 1102	. . 3 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> E.g e. Fil (X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g)))
93	92	ex 402	. 2 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fClus` J)` F) -> E.g e. Fil (X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g))))
94		eqid 1884	. . . . . . . . . . . . . . 15 |- U.g = U.g
95	21, 94	flimfcls 15613	. . . . . . . . . . . . . 14 |- ((J e. Top /\ g e. Fil /\ X = U.g) -> ((fLim1` J)` g) C_ ((fClus` J)` g))
96	95	3expia 1069	. . . . . . . . . . . . 13 |- ((J e. Top /\ g e. Fil) -> (X = U.g -> ((fLim1` J)` g) C_ ((fClus` J)` g)))
97	96	3ad2antl1 1038	. . . . . . . . . . . 12 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil) -> (X = U.g -> ((fLim1` J)` g) C_ ((fClus` J)` g)))
98	97	com12 14	. . . . . . . . . . 11 |- (X = U.g -> (((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil) -> ((fLim1` J)` g) C_ ((fClus` J)` g)))
99	98	adantr 425	. . . . . . . . . 10 |- ((X = U.g /\ F C_ g) -> (((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil) -> ((fLim1` J)` g) C_ ((fClus` J)` g)))
100	99	imp 377	. . . . . . . . 9 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> ((fLim1` J)` g) C_ ((fClus` J)` g))
101		df-3an 860	. . . . . . . . . . . . 13 |- ((J e. Top /\ F e. Fil /\ g e. Fil) <-> ((J e. Top /\ F e. Fil) /\ g e. Fil))
102	101	biimpri 169	. . . . . . . . . . . 12 |- (((J e. Top /\ F e. Fil) /\ g e. Fil) -> (J e. Top /\ F e. Fil /\ g e. Fil))
103	102	3adantl3 1034	. . . . . . . . . . 11 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil) -> (J e. Top /\ F e. Fil /\ g e. Fil))
104	103	adantl 424	. . . . . . . . . 10 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> (J e. Top /\ F e. Fil /\ g e. Fil))
105		simprl3 923	. . . . . . . . . 10 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> X = Y)
106		simpll 448	. . . . . . . . . 10 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> X = U.g)
107		simplr 449	. . . . . . . . . 10 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> F C_ g)
108	21, 8, 94	fclusss 15611	. . . . . . . . . 10 |- ((((J e. Top /\ F e. Fil /\ g e. Fil) /\ X = Y /\ X = U.g) /\ F C_ g) -> ((fClus` J)` g) C_ ((fClus` J)` F))
109	104, 105, 106, 107, 108	syl31anc 1103	. . . . . . . . 9 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> ((fClus` J)` g) C_ ((fClus` J)` F))
110	100, 109	sstrd 2627	. . . . . . . 8 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> ((fLim1` J)` g) C_ ((fClus` J)` F))
111	110	sseld 2619	. . . . . . 7 |- (((X = U.g /\ F C_ g) /\ ((J e. Top /\ F e. Fil /\ X = Y) /\ g e. Fil)) -> (A e. ((fLim1` J)` g) -> A e. ((fClus` J)` F)))
112	111	exp32 408	. . . . . 6 |- ((X = U.g /\ F C_ g) -> ((J e. Top /\ F e. Fil /\ X = Y) -> (g e. Fil -> (A e. ((fLim1` J)` g) -> A e. ((fClus` J)` F)))))
113	112	com24 41	. . . . 5 |- ((X = U.g /\ F C_ g) -> (A e. ((fLim1` J)` g) -> (g e. Fil -> ((J e. Top /\ F e. Fil /\ X = Y) -> A e. ((fClus` J)` F)))))
114	113	3impia 1064	. . . 4 |- ((X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g)) -> (g e. Fil -> ((J e. Top /\ F e. Fil /\ X = Y) -> A e. ((fClus` J)` F))))
115	114	com13 37	. . 3 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (g e. Fil -> ((X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g)) -> A e. ((fClus` J)` F))))
116	115	r19.23adv 2215	. 2 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (E.g e. Fil (X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g)) -> A e. ((fClus` J)` F)))
117	93, 116	impbid 574	1 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fClus` J)` F) <-> E.g e. Fil (X = U.g /\ F C_ g /\ A e. ((fLim1` J)` g))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017   e/ wnel 2018  A.wral 2105  E.wrex 2106  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  U.cuni 3177  ` cfv 3998  Topctop 8857  neicnei 8988   fi cfi 10210  fBascfbas 10257  filGencfg 10258  Filcfil 10264  fLim1cflim1 10294  fCluscfclus 15582

This theorem is referenced by:  uffclsflim 15616  fcluscnplem 15617

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-top 8861  df-cld 8939  df-ntr 8940  df-cls 8941  df-nei 8989  df-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-flim1 10295  df-fclus 15584

Copyright terms: Public domain