Theorem flimfnfcls 15615

Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 15614, this theorem illustrates the duality between convergence and clustering.

Hypotheses

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

Assertion

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

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

Proof of Theorem flimfnfcls

Step	Hyp	Ref	Expression
1		simp1 876	. . . . . . . . 9 |- ((J e. Top /\ F e. Fil /\ X = Y) -> J e. Top)
2	1	adantr 425	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> J e. Top)
3		simp2 877	. . . . . . . . 9 |- ((J e. Top /\ F e. Fil /\ X = Y) -> F e. Fil)
4	3	adantr 425	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> F e. Fil)
5		simprr 451	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> g e. Fil)
6	2, 4, 5	3jca 1050	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> (J e. Top /\ F e. Fil /\ g e. Fil))
7		simp3 878	. . . . . . . 8 |- ((J e. Top /\ F e. Fil /\ X = Y) -> X = Y)
8	7	adantr 425	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> X = Y)
9		simprll 456	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> X = U.g)
10		simprlr 457	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> F C_ g)
11		flimfnfcls.1	. . . . . . . . 9 |- X = U.J
12		flimfnfcls.2	. . . . . . . . 9 |- Y = U.F
13		eqid 1884	. . . . . . . . 9 |- U.g = U.g
14	11, 12, 13	limfilss 10299	. . . . . . . 8 |- ((((J e. Top /\ F e. Fil /\ g e. Fil) /\ X = Y /\ X = U.g) /\ F C_ g /\ A e. ((fLim1` J)` F)) -> A e. ((fLim1` J)` g))
15	14	3expia 1069	. . . . . . 7 |- ((((J e. Top /\ F e. Fil /\ g e. Fil) /\ X = Y /\ X = U.g) /\ F C_ g) -> (A e. ((fLim1` J)` F) -> A e. ((fLim1` J)` g)))
16	6, 8, 9, 10, 15	syl31anc 1103	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> (A e. ((fLim1` J)` F) -> A e. ((fLim1` J)` g)))
17	11, 13	flimfcls 15613	. . . . . . . 8 |- ((J e. Top /\ g e. Fil /\ X = U.g) -> ((fLim1` J)` g) C_ ((fClus` J)` g))
18	2, 5, 9, 17	syl111anc 1100	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> ((fLim1` J)` g) C_ ((fClus` J)` g))
19	18	sseld 2619	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> (A e. ((fLim1` J)` g) -> A e. ((fClus` J)` g)))
20	16, 19	syld 30	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((X = U.g /\ F C_ g) /\ g e. Fil)) -> (A e. ((fLim1` J)` F) -> A e. ((fClus` J)` g)))
21	20	exp32 408	. . . 4 |- ((J e. Top /\ F e. Fil /\ X = Y) -> ((X = U.g /\ F C_ g) -> (g e. Fil -> (A e. ((fLim1` J)` F) -> A e. ((fClus` J)` g)))))
22	21	com24 41	. . 3 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fLim1` J)` F) -> (g e. Fil -> ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)))))
23	22	r19.21adv 2181	. 2 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fLim1` J)` F) -> A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g))))
24	12	eqeq2i 1894	. . . . . . . 8 |- (X = Y <-> X = U.F)
25	24	biimpi 168	. . . . . . 7 |- (X = Y -> X = U.F)
26	25	3ad2ant3 899	. . . . . 6 |- ((J e. Top /\ F e. Fil /\ X = Y) -> X = U.F)
27		ssid 2634	. . . . . 6 |- F C_ F
28	26, 27	jctir 317	. . . . 5 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (X = U.F /\ F C_ F))
29		unieq 3185	. . . . . . . . . 10 |- (g = F -> U.g = U.F)
30	29	eqeq2d 1895	. . . . . . . . 9 |- (g = F -> (X = U.g <-> X = U.F))
31		sseq2 2639	. . . . . . . . 9 |- (g = F -> (F C_ g <-> F C_ F))
32	30, 31	anbi12d 690	. . . . . . . 8 |- (g = F -> ((X = U.g /\ F C_ g) <-> (X = U.F /\ F C_ F)))
33		fveq2 4681	. . . . . . . . 9 |- (g = F -> ((fClus` J)` g) = ((fClus` J)` F))
34	33	eleq2d 1964	. . . . . . . 8 |- (g = F -> (A e. ((fClus` J)` g) <-> A e. ((fClus` J)` F)))
35	32, 34	imbi12d 688	. . . . . . 7 |- (g = F -> (((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) <-> ((X = U.F /\ F C_ F) -> A e. ((fClus` J)` F))))
36	35	rcla4v 2376	. . . . . 6 |- (F e. Fil -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> ((X = U.F /\ F C_ F) -> A e. ((fClus` J)` F))))
37	36	3ad2ant2 898	. . . . 5 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> ((X = U.F /\ F C_ F) -> A e. ((fClus` J)` F))))
38	28, 37	mpid 58	. . . 4 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> A e. ((fClus` J)` F)))
39	11, 12	fclselbas 15608	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. ((fClus` J)` F)) -> A e. X)
40	39	ex 402	. . . 4 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fClus` J)` F) -> A e. X))
41	38, 40	syld 30	. . 3 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> A e. X))
42	11, 12	flimopn 10321	. . . . . . . . . 10 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (A e. ((fLim1` J)` F) <-> A.o e. J (A e. o -> o e. F)))
43	42	notbid 673	. . . . . . . . 9 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (-. A e. ((fLim1` J)` F) <-> -. A.o e. J (A e. o -> o e. F)))
44		rexanali 2144	. . . . . . . . 9 |- (E.o e. J (A e. o /\ -. o e. F) <-> -. A.o e. J (A e. o -> o e. F))
45	43, 44	syl6bbr 597	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (-. A e. ((fLim1` J)` F) <-> E.o e. J (A e. o /\ -. o e. F)))
46		simpll2 916	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> F e. Fil)
47		uniexg 3795	. . . . . . . . . . . . . . . . . . 19 |- (J e. Top -> U.J e. _V)
48	47, 11	syl5eqel 1975	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> X e. _V)
49		abssexg 3490	. . . . . . . . . . . . . . . . . 18 |- (X e. _V -> {x | (x C_ X /\ (X \ o) C_ x)} e. _V)
50	48, 49	syl 12	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> {x | (x C_ X /\ (X \ o) C_ x)} e. _V)
51	50	3ad2ant1 897	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ F e. Fil /\ X = Y) -> {x | (x C_ X /\ (X \ o) C_ x)} e. _V)
52	51	ad2antrr 440	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> {x | (x C_ X /\ (X \ o) C_ x)} e. _V)
53		unexg 3798	. . . . . . . . . . . . . . 15 |- ((F e. Fil /\ {x | (x C_ X /\ (X \ o) C_ x)} e. _V) -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) e. _V)
54	46, 52, 53	syl11anc 524	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) e. _V)
55		fsubbas 10281	. . . . . . . . . . . . . 14 |- ((F u. {x | (x C_ X /\ (X \ o) C_ x)}) e. _V -> (( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) e. fBas <-> ((F u. {x | (x C_ X /\ (X \ o) C_ x)}) =/= (/) /\ (/) e/ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))
56	54, 55	syl 12	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) e. fBas <-> ((F u. {x | (x C_ X /\ (X \ o) C_ x)}) =/= (/) /\ (/) e/ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))
57	12	filusb 10267	. . . . . . . . . . . . . . . 16 |- (F e. Fil -> Y e. F)
58		ne0i 2881	. . . . . . . . . . . . . . . 16 |- (Y e. F -> F =/= (/))
59		ssun1 2767	. . . . . . . . . . . . . . . . 17 |- F C_ (F u. {x | (x C_ X /\ (X \ o) C_ x)})
60		ssn0 2905	. . . . . . . . . . . . . . . . 17 |- ((F C_ (F u. {x | (x C_ X /\ (X \ o) C_ x)}) /\ F =/= (/)) -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) =/= (/))
61	59, 60	mpan 759	. . . . . . . . . . . . . . . 16 |- (F =/= (/) -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) =/= (/))
62	57, 58, 61	3syl 24	. . . . . . . . . . . . . . 15 |- (F e. Fil -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) =/= (/))
63	62	3ad2ant2 898	. . . . . . . . . . . . . 14 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) =/= (/))
64	63	ad2antrr 440	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) =/= (/))
65		visset 2295	. . . . . . . . . . . . . . . . . . . . 21 |- z e. _V
66		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> (x C_ X <-> z C_ X))
67		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> ((X \ o) C_ x <-> (X \ o) C_ z))
68	66, 67	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> ((x C_ X /\ (X \ o) C_ x) <-> (z C_ X /\ (X \ o) C_ z)))
69	65, 68	elab 2403	. . . . . . . . . . . . . . . . . . . 20 |- (z e. {x | (x C_ X /\ (X \ o) C_ x)} <-> (z C_ X /\ (X \ o) C_ z))
70	69	simprbi 353	. . . . . . . . . . . . . . . . . . 19 |- (z e. {x | (x C_ X /\ (X \ o) C_ x)} -> (X \ o) C_ z)
71	70	ad2antll 443	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) /\ (y e. F /\ z e. {x | (x C_ X /\ (X \ o) C_ x)})) -> (X \ o) C_ z)
72		sslin 2819	. . . . . . . . . . . . . . . . . 18 |- ((X \ o) C_ z -> (y i^i (X \ o)) C_ (y i^i z))
73	71, 72	syl 12	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) /\ (y e. F /\ z e. {x | (x C_ X /\ (X \ o) C_ x)})) -> (y i^i (X \ o)) C_ (y i^i z))
74		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y e. F -> y C_ U.F)
75	74, 12	syl6ssr 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y e. F -> y C_ Y)
76	75	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((X = Y /\ y e. F) -> y C_ Y)
77		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((X = Y /\ y e. F) -> X = Y)
78	76, 77	sseqtr4d 2654	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((X = Y /\ y e. F) -> y C_ X)
79	78	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ y e. F) -> y C_ X)
80	79	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> y C_ X)
81		reldisj 2916	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y C_ X -> ((y i^i (X \ o)) = (/) <-> y C_ (X \ (X \ o))))
82	80, 81	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> ((y i^i (X \ o)) = (/) <-> y C_ (X \ (X \ o))))
83	11	eltopss 8872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Top /\ o e. J) -> o C_ X)
84	83	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ o e. J) -> o C_ X)
85	84	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ (o e. J /\ A e. o)) -> o C_ X)
86	85	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> o C_ X)
87		dfss4 2827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (o C_ X <-> (X \ (X \ o)) = o)
88	86, 87	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> (X \ (X \ o)) = o)
89	88	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> (y C_ (X \ (X \ o)) <-> y C_ o))
90		simpll2 916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> F e. Fil)
91		simprlr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> y e. F)
92	85	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ ((o e. J /\ A e. o) /\ y e. F)) -> o C_ X)
93	92	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> o C_ X)
94		simpll3 917	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> X = Y)
95	93, 94	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> o C_ Y)
96		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> y C_ o)
97	91, 95, 96	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> (y e. F /\ o C_ Y /\ y C_ o))
98	12	fillsb 10270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F e. Fil -> ((y e. F /\ o C_ Y /\ y C_ o) -> o e. F))
99	90, 97, 98	sylc 83	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (((o e. J /\ A e. o) /\ y e. F) /\ y C_ o)) -> o e. F)
100	99	expr 418	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> (y C_ o -> o e. F))
101	89, 100	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> (y C_ (X \ (X \ o)) -> o e. F))
102	82, 101	sylbid 220	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> ((y i^i (X \ o)) = (/) -> o e. F))
103	102	necon3bd 2039	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ ((o e. J /\ A e. o) /\ y e. F)) -> (-. o e. F -> (y i^i (X \ o)) =/= (/)))
104	103	exp44 416	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (o e. J -> (A e. o -> (y e. F -> (-. o e. F -> (y i^i (X \ o)) =/= (/))))))
105	104	com45 46	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (o e. J -> (A e. o -> (-. o e. F -> (y e. F -> (y i^i (X \ o)) =/= (/))))))
106	105	imp55 15333	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) /\ y e. F) -> (y i^i (X \ o)) =/= (/))
107	106	adantrr 431	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) /\ (y e. F /\ z e. {x | (x C_ X /\ (X \ o) C_ x)})) -> (y i^i (X \ o)) =/= (/))
108		ssn0 2905	. . . . . . . . . . . . . . . . 17 |- (((y i^i (X \ o)) C_ (y i^i z) /\ (y i^i (X \ o)) =/= (/)) -> (y i^i z) =/= (/))
109	73, 107, 108	syl11anc 524	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) /\ (y e. F /\ z e. {x | (x C_ X /\ (X \ o) C_ x)})) -> (y i^i z) =/= (/))
110	109	ex 402	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> ((y e. F /\ z e. {x | (x C_ X /\ (X \ o) C_ x)}) -> (y i^i z) =/= (/)))
111	110	r19.21aivv 2183	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> A.y e. F A.z e. {x | (x C_ X /\ (X \ o) C_ x)} (y i^i z) =/= (/))
112		filfbas 10276	. . . . . . . . . . . . . . . . 17 |- (F e. Fil -> F e. fBas)
113	112	3ad2ant2 898	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ F e. Fil /\ X = Y) -> F e. fBas)
114	113	ad2antrr 440	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> F e. fBas)
115	48	3ad2ant1 897	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ F e. Fil /\ X = Y) -> X e. _V)
116	115	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> X e. _V)
117		difss 2735	. . . . . . . . . . . . . . . . . 18 |- (X \ o) C_ X
118	117	a1i 8	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (X \ o) C_ X)
119	84	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> o C_ X)
120	119, 87	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> (X \ (X \ o)) = o)
121	120	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> ((X \ (X \ o)) = X <-> o = X))
122		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (o = X -> (o e. F <-> X e. F))
123		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (X = Y -> (X e. F <-> Y e. F))
124	123, 57	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F e. Fil -> (X = Y -> X e. F))
125	124	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F e. Fil /\ X = Y) -> X e. F)
126	125	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Top /\ F e. Fil /\ X = Y) -> X e. F)
127	126	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> X e. F)
128	122, 127	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> (o = X -> o e. F))
129	121, 128	sylbid 220	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> ((X \ (X \ o)) = X -> o e. F))
130		difeq2 2719	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((X \ o) = (/) -> (X \ (X \ o)) = (X \ (/)))
131		dif0 2943	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X \ (/)) = X
132	130, 131	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X \ o) = (/) -> (X \ (X \ o)) = X)
133	129, 132	syl5 20	. . . . . . . . . . . . . . . . . . . . 21 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> ((X \ o) = (/) -> o e. F))
134	133	necon3bd 2039	. . . . . . . . . . . . . . . . . . . 20 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ A e. o)) -> (-. o e. F -> (X \ o) =/= (/)))
135	134	expr 418	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ o e. J) -> (A e. o -> (-. o e. F -> (X \ o) =/= (/))))
136	135	imp3a 388	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ o e. J) -> ((A e. o /\ -. o e. F) -> (X \ o) =/= (/)))
137	136	impr 422	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (X \ o) =/= (/))
138		supfil 15560	. . . . . . . . . . . . . . . . . 18 |- ((X e. _V /\ (X \ o) C_ X /\ (X \ o) =/= (/)) -> ({x | (x C_ X /\ (X \ o) C_ x)} e. Fil /\ X = U.{x | (x C_ X /\ (X \ o) C_ x)}))
139	138	simplld 348	. . . . . . . . . . . . . . . . 17 |- ((X e. _V /\ (X \ o) C_ X /\ (X \ o) =/= (/)) -> {x | (x C_ X /\ (X \ o) C_ x)} e. Fil)
140	116, 118, 137, 139	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> {x | (x C_ X /\ (X \ o) C_ x)} e. Fil)
141		filfbas 10276	. . . . . . . . . . . . . . . 16 |- ({x | (x C_ X /\ (X \ o) C_ x)} e. Fil -> {x | (x C_ X /\ (X \ o) C_ x)} e. fBas)
142	140, 141	syl 12	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> {x | (x C_ X /\ (X \ o) C_ x)} e. fBas)
143		fbunfip 10282	. . . . . . . . . . . . . . 15 |- ((F e. fBas /\ {x | (x C_ X /\ (X \ o) C_ x)} e. fBas) -> ((/) e/ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) <-> A.y e. F A.z e. {x | (x C_ X /\ (X \ o) C_ x)} (y i^i z) =/= (/)))
144	114, 142, 143	syl11anc 524	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> ((/) e/ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) <-> A.y e. F A.z e. {x | (x C_ X /\ (X \ o) C_ x)} (y i^i z) =/= (/)))
145	111, 144	mpbird 213	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (/) e/ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
146	56, 64, 145	mpbir2and 802	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) e. fBas)
147		fgfil 10290	. . . . . . . . . . . 12 |- (( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) e. fBas -> (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) e. Fil)
148	146, 147	syl 12	. . . . . . . . . . 11 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) e. Fil)
149		simpll3 917	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> X = Y)
150	149, 12	syl6eq 1944	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> X = U.F)
151	138	simprd 352	. . . . . . . . . . . . . . 15 |- ((X e. _V /\ (X \ o) C_ X /\ (X \ o) =/= (/)) -> X = U.{x | (x C_ X /\ (X \ o) C_ x)})
152	116, 118, 137, 151	syl111anc 1100	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> X = U.{x | (x C_ X /\ (X \ o) C_ x)})
153	150, 152	uneq12d 2756	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (X u. X) = (U.F u. U.{x | (x C_ X /\ (X \ o) C_ x)}))
154		unidm 2743	. . . . . . . . . . . . . 14 |- (X u. X) = X
155	154	eqcomi 1888	. . . . . . . . . . . . 13 |- X = (X u. X)
156		uniun 3196	. . . . . . . . . . . . 13 |- U.(F u. {x | (x C_ X /\ (X \ o) C_ x)}) = (U.F u. U.{x | (x C_ X /\ (X \ o) C_ x)})
157	153, 155, 156	3eqtr4g 1953	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> X = U.(F u. {x | (x C_ X /\ (X \ o) C_ x)}))
158		fiuni 10219	. . . . . . . . . . . . 13 |- ((F u. {x | (x C_ X /\ (X \ o) C_ x)}) e. _V -> U.(F u. {x | (x C_ X /\ (X \ o) C_ x)}) = U.( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
159	54, 158	syl 12	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> U.(F u. {x | (x C_ X /\ (X \ o) C_ x)}) = U.( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
160		eqid 1884	. . . . . . . . . . . . . 14 |- U.( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) = U.( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))
161	160	fgbas 10286	. . . . . . . . . . . . 13 |- (( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) e. fBas -> U.( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
162	146, 161	syl 12	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> U.( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
163	157, 159, 162	3eqtrd 1929	. . . . . . . . . . 11 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> X = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
164	59	a1i 8	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> F C_ (F u. {x | (x C_ X /\ (X \ o) C_ x)}))
165		abfi2 10216	. . . . . . . . . . . . . 14 |- ((F u. {x | (x C_ X /\ (X \ o) C_ x)}) e. _V -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) C_ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
166	54, 165	syl 12	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (F u. {x | (x C_ X /\ (X \ o) C_ x)}) C_ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
167	164, 166	sstrd 2627	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> F C_ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
168		fbssfg 10285	. . . . . . . . . . . . 13 |- (( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) e. fBas -> ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) C_ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
169	146, 168	syl 12	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})) C_ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
170	167, 169	sstrd 2627	. . . . . . . . . . 11 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> F C_ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
171		simprl 450	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> o e. J)
172		simprrl 458	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> A e. o)
173		ssun2 2768	. . . . . . . . . . . . . . . . . . . 20 |- {x | (x C_ X /\ (X \ o) C_ x)} C_ (F u. {x | (x C_ X /\ (X \ o) C_ x)})
174	173	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> {x | (x C_ X /\ (X \ o) C_ x)} C_ (F u. {x | (x C_ X /\ (X \ o) C_ x)}))
175	174, 166	sstrd 2627	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> {x | (x C_ X /\ (X \ o) C_ x)} C_ ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
176	175, 169	sstrd 2627	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> {x | (x C_ X /\ (X \ o) C_ x)} C_ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
177		ssid 2634	. . . . . . . . . . . . . . . . . . 19 |- (X \ o) C_ (X \ o)
178	117, 177	pm3.2i 307	. . . . . . . . . . . . . . . . . 18 |- ((X \ o) C_ X /\ (X \ o) C_ (X \ o))
179		difexg 3458	. . . . . . . . . . . . . . . . . . . . 21 |- (X e. _V -> (X \ o) e. _V)
180		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (X \ o) -> (x C_ X <-> (X \ o) C_ X))
181		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (X \ o) -> ((X \ o) C_ x <-> (X \ o) C_ (X \ o)))
182	180, 181	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (X \ o) -> ((x C_ X /\ (X \ o) C_ x) <-> ((X \ o) C_ X /\ (X \ o) C_ (X \ o))))
183	182	elabg 2405	. . . . . . . . . . . . . . . . . . . . 21 |- ((X \ o) e. _V -> ((X \ o) e. {x | (x C_ X /\ (X \ o) C_ x)} <-> ((X \ o) C_ X /\ (X \ o) C_ (X \ o))))
184	48, 179, 183	3syl 24	. . . . . . . . . . . . . . . . . . . 20 |- (J e. Top -> ((X \ o) e. {x | (x C_ X /\ (X \ o) C_ x)} <-> ((X \ o) C_ X /\ (X \ o) C_ (X \ o))))
185	184	3ad2ant1 897	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ F e. Fil /\ X = Y) -> ((X \ o) e. {x | (x C_ X /\ (X \ o) C_ x)} <-> ((X \ o) C_ X /\ (X \ o) C_ (X \ o))))
186	185	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> ((X \ o) e. {x | (x C_ X /\ (X \ o) C_ x)} <-> ((X \ o) C_ X /\ (X \ o) C_ (X \ o))))
187	178, 186	mpbiri 211	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (X \ o) e. {x | (x C_ X /\ (X \ o) C_ x)})
188	176, 187	sseldd 2620	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (X \ o) e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
189		difdisj 2945	. . . . . . . . . . . . . . . . 17 |- (o i^i (X \ o)) = (/)
190	189	a1i 8	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (o i^i (X \ o)) = (/))
191		ineq2 2790	. . . . . . . . . . . . . . . . . 18 |- (s = (X \ o) -> (o i^i s) = (o i^i (X \ o)))
192	191	eqeq1d 1892	. . . . . . . . . . . . . . . . 17 |- (s = (X \ o) -> ((o i^i s) = (/) <-> (o i^i (X \ o)) = (/)))
193	192	rcla4ev 2381	. . . . . . . . . . . . . . . 16 |- (((X \ o) e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) /\ (o i^i (X \ o)) = (/)) -> E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(o i^i s) = (/))
194	188, 190, 193	syl11anc 524	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(o i^i s) = (/))
195		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (j = o -> (A e. j <-> A e. o))
196		ineq1 2789	. . . . . . . . . . . . . . . . . . 19 |- (j = o -> (j i^i s) = (o i^i s))
197	196	eqeq1d 1892	. . . . . . . . . . . . . . . . . 18 |- (j = o -> ((j i^i s) = (/) <-> (o i^i s) = (/)))
198	197	rexbidv 2124	. . . . . . . . . . . . . . . . 17 |- (j = o -> (E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/) <-> E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(o i^i s) = (/)))
199	195, 198	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (j = o -> ((A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/)) <-> (A e. o /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(o i^i s) = (/))))
200	199	rcla4ev 2381	. . . . . . . . . . . . . . 15 |- ((o e. J /\ (A e. o /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(o i^i s) = (/))) -> E.j e. J (A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/)))
201	171, 172, 194, 200	syl12anc 1098	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> E.j e. J (A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/)))
202	201	a1d 15	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (A e. X -> E.j e. J (A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/))))
203		nne 2021	. . . . . . . . . . . . . . . . . . . 20 |- (-. (j i^i s) =/= (/) <-> (j i^i s) = (/))
204	203	rexbii 2128	. . . . . . . . . . . . . . . . . . 19 |- (E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -. (j i^i s) =/= (/) <-> E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/))
205		rexnal 2114	. . . . . . . . . . . . . . . . . . 19 |- (E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -. (j i^i s) =/= (/) <-> -. A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/))
206	204, 205	bitr3i 192	. . . . . . . . . . . . . . . . . 18 |- (E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/) <-> -. A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/))
207	206	anbi2i 538	. . . . . . . . . . . . . . . . 17 |- ((A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/)) <-> (A e. j /\ -. A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/)))
208	207	rexbii 2128	. . . . . . . . . . . . . . . 16 |- (E.j e. J (A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/)) <-> E.j e. J (A e. j /\ -. A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/)))
209		rexanali 2144	. . . . . . . . . . . . . . . 16 |- (E.j e. J (A e. j /\ -. A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/)) <-> -. A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/)))
210	208, 209	bitri 190	. . . . . . . . . . . . . . 15 |- (E.j e. J (A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/)) <-> -. A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/)))
211	210	imbi2i 202	. . . . . . . . . . . . . 14 |- ((A e. X -> E.j e. J (A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/))) <-> (A e. X -> -. A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/))))
212		imnan 261	. . . . . . . . . . . . . 14 |- ((A e. X -> -. A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/))) <-> -. (A e. X /\ A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/))))
213	211, 212	bitri 190	. . . . . . . . . . . . 13 |- ((A e. X -> E.j e. J (A e. j /\ E.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) = (/))) <-> -. (A e. X /\ A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/))))
214	202, 213	sylib 215	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> -. (A e. X /\ A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/))))
215		simpll1 915	. . . . . . . . . . . . 13 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> J e. Top)
216		eqid 1884	. . . . . . . . . . . . . 14 |- U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))
217	11, 216	isfclus 15606	. . . . . . . . . . . . 13 |- ((J e. Top /\ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) e. Fil /\ X = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))) -> (A e. ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))) <-> (A e. X /\ A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/)))))
218	215, 148, 163, 217	syl111anc 1100	. . . . . . . . . . . 12 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> (A e. ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))) <-> (A e. X /\ A.j e. J (A e. j -> A.s e. (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))(j i^i s) =/= (/)))))
219	214, 218	mtbird 783	. . . . . . . . . . 11 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> -. A e. ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))
220		unieq 3185	. . . . . . . . . . . . . 14 |- (g = (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -> U.g = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))
221	220	eqeq2d 1895	. . . . . . . . . . . . 13 |- (g = (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -> (X = U.g <-> X = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))
222		sseq2 2639	. . . . . . . . . . . . 13 |- (g = (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -> (F C_ g <-> F C_ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))
223		fveq2 4681	. . . . . . . . . . . . . . 15 |- (g = (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -> ((fClus` J)` g) = ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))
224	223	eleq2d 1964	. . . . . . . . . . . . . 14 |- (g = (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -> (A e. ((fClus` J)` g) <-> A e. ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))))
225	224	notbid 673	. . . . . . . . . . . . 13 |- (g = (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -> (-. A e. ((fClus` J)` g) <-> -. A e. ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))))))
226	221, 222, 225	3anbi123d 1168	. . . . . . . . . . . 12 |- (g = (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) -> ((X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g)) <-> (X = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) /\ F C_ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) /\ -. A e. ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))))
227	226	rcla4ev 2381	. . . . . . . . . . 11 |- (((filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) e. Fil /\ (X = U.(filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) /\ F C_ (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)}))) /\ -. A e. ((fClus` J)` (filGen` ( fi ` (F u. {x | (x C_ X /\ (X \ o) C_ x)})))))) -> E.g e. Fil (X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g)))
228	148, 163, 170, 219, 227	syl13anc 1102	. . . . . . . . . 10 |- ((((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) /\ (o e. J /\ (A e. o /\ -. o e. F))) -> E.g e. Fil (X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g)))
229	228	exp32 408	. . . . . . . . 9 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (o e. J -> ((A e. o /\ -. o e. F) -> E.g e. Fil (X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g)))))
230	229	r19.23adv 2215	. . . . . . . 8 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (E.o e. J (A e. o /\ -. o e. F) -> E.g e. Fil (X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g))))
231	45, 230	sylbid 220	. . . . . . 7 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (-. A e. ((fLim1` J)` F) -> E.g e. Fil (X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g))))
232		df-3an 860	. . . . . . . . 9 |- ((X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g)) <-> ((X = U.g /\ F C_ g) /\ -. A e. ((fClus` J)` g)))
233	232	rexbii 2128	. . . . . . . 8 |- (E.g e. Fil (X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g)) <-> E.g e. Fil ((X = U.g /\ F C_ g) /\ -. A e. ((fClus` J)` g)))
234		rexanali 2144	. . . . . . . 8 |- (E.g e. Fil ((X = U.g /\ F C_ g) /\ -. A e. ((fClus` J)` g)) <-> -. A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)))
235	233, 234	bitri 190	. . . . . . 7 |- (E.g e. Fil (X = U.g /\ F C_ g /\ -. A e. ((fClus` J)` g)) <-> -. A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)))
236	231, 235	syl6ib 229	. . . . . 6 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (-. A e. ((fLim1` J)` F) -> -. A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g))))
237	236	con4d 91	. . . . 5 |- (((J e. Top /\ F e. Fil /\ X = Y) /\ A e. X) -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> A e. ((fLim1` J)` F)))
238	237	ex 402	. . . 4 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. X -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> A e. ((fLim1` J)` F))))
239	238	com23 36	. . 3 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> (A e. X -> A e. ((fLim1` J)` F))))
240	41, 239	mpdd 57	. 2 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g)) -> A e. ((fLim1` J)` F)))
241	23, 240	impbid 574	1 |- ((J e. Top /\ F e. Fil /\ X = Y) -> (A e. ((fLim1` J)` F) <-> A.g e. Fil ((X = U.g /\ F C_ g) -> A e. ((fClus` J)` g))))

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

This theorem is referenced by:  fcluscnp 15618

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