Theorem fcluscf 15612

Description: Characterization of fineness of topologies in terms of cluster points.

Hypotheses

Ref	Expression
fcluscf.1	|- X = U.J
fcluscf.2	|- Y = U.K

Assertion

Ref	Expression
fcluscf	|- ((J e. Top /\ K e. Top /\ X = Y) -> (J C_ K <-> A.f e. Fil (X = U.f -> ((fClus` K)` f) C_ ((fClus` J)` f))))

Distinct variable groups:   f,J   f,K   f,X   f,Y

Proof of Theorem fcluscf

Step	Hyp	Ref	Expression
1		fcluscf.1	. . 3 |- X = U.J
2		fcluscf.2	. . 3 |- Y = U.K
3	1, 2	topfne 15500	. 2 |- ((J e. Top /\ K e. Top /\ X = Y) -> (J C_ K <-> JFneK))
4		fnessex 15484	. . . . . . . . . . . . . . . . . . . 20 |- (((K e. Top /\ JFneK /\ o e. J) /\ a e. o) -> E.q e. K (a e. q /\ q C_ o))
5	4	ex 402	. . . . . . . . . . . . . . . . . . 19 |- ((K e. Top /\ JFneK /\ o e. J) -> (a e. o -> E.q e. K (a e. q /\ q C_ o)))
6	5	3expia 1069	. . . . . . . . . . . . . . . . . 18 |- ((K e. Top /\ JFneK) -> (o e. J -> (a e. o -> E.q e. K (a e. q /\ q C_ o))))
7	6	imp3a 388	. . . . . . . . . . . . . . . . 17 |- ((K e. Top /\ JFneK) -> ((o e. J /\ a e. o) -> E.q e. K (a e. q /\ q C_ o)))
8	7	3ad2antl2 1039	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) -> ((o e. J /\ a e. o) -> E.q e. K (a e. q /\ q C_ o)))
9	8	imp 377	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ JFneK) /\ (o e. J /\ a e. o)) -> E.q e. K (a e. q /\ q C_ o))
10	9	adantlrr 435	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ (o e. J /\ a e. o)) -> E.q e. K (a e. q /\ q C_ o))
11	10	adantlr 429	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ (o e. J /\ a e. o)) -> E.q e. K (a e. q /\ q C_ o))
12		simprl 450	. . . . . . . . . . . . . . . . . . 19 |- ((q e. K /\ (a e. q /\ q C_ o)) -> a e. q)
13	12	ad2antll 443	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ ((o e. J /\ a e. o) /\ (q e. K /\ (a e. q /\ q C_ o)))) -> a e. q)
14		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . 22 |- (p = q -> (a e. p <-> a e. q))
15		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (p = q -> (p i^i t) = (q i^i t))
16	15	neeq1d 2028	. . . . . . . . . . . . . . . . . . . . . . 23 |- (p = q -> ((p i^i t) =/= (/) <-> (q i^i t) =/= (/)))
17	16	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . 22 |- (p = q -> (A.t e. f (p i^i t) =/= (/) <-> A.t e. f (q i^i t) =/= (/)))
18	14, 17	imbi12d 688	. . . . . . . . . . . . . . . . . . . . 21 |- (p = q -> ((a e. p -> A.t e. f (p i^i t) =/= (/)) <-> (a e. q -> A.t e. f (q i^i t) =/= (/))))
19	18	rcla4v 2376	. . . . . . . . . . . . . . . . . . . 20 |- (q e. K -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> (a e. q -> A.t e. f (q i^i t) =/= (/))))
20	19	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((q e. K /\ (a e. q /\ q C_ o)) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> (a e. q -> A.t e. f (q i^i t) =/= (/))))
21	20	ad2antll 443	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ ((o e. J /\ a e. o) /\ (q e. K /\ (a e. q /\ q C_ o)))) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> (a e. q -> A.t e. f (q i^i t) =/= (/))))
22	13, 21	mpid 58	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ ((o e. J /\ a e. o) /\ (q e. K /\ (a e. q /\ q C_ o)))) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.t e. f (q i^i t) =/= (/)))
23		ineq2 2790	. . . . . . . . . . . . . . . . . . . . 21 |- (t = s -> (q i^i t) = (q i^i s))
24	23	neeq1d 2028	. . . . . . . . . . . . . . . . . . . 20 |- (t = s -> ((q i^i t) =/= (/) <-> (q i^i s) =/= (/)))
25	24	rcla4cv 2377	. . . . . . . . . . . . . . . . . . 19 |- (A.t e. f (q i^i t) =/= (/) -> (s e. f -> (q i^i s) =/= (/)))
26		ssrin 2817	. . . . . . . . . . . . . . . . . . . . . 22 |- (q C_ o -> (q i^i s) C_ (o i^i s))
27		ssn0 2905	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((q i^i s) C_ (o i^i s) /\ (q i^i s) =/= (/)) -> (o i^i s) =/= (/))
28	27	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- ((q i^i s) C_ (o i^i s) -> ((q i^i s) =/= (/) -> (o i^i s) =/= (/)))
29	26, 28	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (q C_ o -> ((q i^i s) =/= (/) -> (o i^i s) =/= (/)))
30	29	ad2antll 443	. . . . . . . . . . . . . . . . . . . 20 |- ((q e. K /\ (a e. q /\ q C_ o)) -> ((q i^i s) =/= (/) -> (o i^i s) =/= (/)))
31	30	ad2antll 443	. . . . . . . . . . . . . . . . . . 19 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ ((o e. J /\ a e. o) /\ (q e. K /\ (a e. q /\ q C_ o)))) -> ((q i^i s) =/= (/) -> (o i^i s) =/= (/)))
32	25, 31	syl9r 72	. . . . . . . . . . . . . . . . . 18 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ ((o e. J /\ a e. o) /\ (q e. K /\ (a e. q /\ q C_ o)))) -> (A.t e. f (q i^i t) =/= (/) -> (s e. f -> (o i^i s) =/= (/))))
33	32	r19.21adv 2181	. . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ ((o e. J /\ a e. o) /\ (q e. K /\ (a e. q /\ q C_ o)))) -> (A.t e. f (q i^i t) =/= (/) -> A.s e. f (o i^i s) =/= (/)))
34	22, 33	syld 30	. . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ ((o e. J /\ a e. o) /\ (q e. K /\ (a e. q /\ q C_ o)))) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.s e. f (o i^i s) =/= (/)))
35	34	expr 418	. . . . . . . . . . . . . . 15 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ (o e. J /\ a e. o)) -> ((q e. K /\ (a e. q /\ q C_ o)) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.s e. f (o i^i s) =/= (/))))
36	35	exp3a 405	. . . . . . . . . . . . . 14 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ (o e. J /\ a e. o)) -> (q e. K -> ((a e. q /\ q C_ o) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.s e. f (o i^i s) =/= (/)))))
37	36	r19.23adv 2215	. . . . . . . . . . . . 13 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ (o e. J /\ a e. o)) -> (E.q e. K (a e. q /\ q C_ o) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.s e. f (o i^i s) =/= (/))))
38	11, 37	mpd 29	. . . . . . . . . . . 12 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) /\ (o e. J /\ a e. o)) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.s e. f (o i^i s) =/= (/)))
39	38	exp32 408	. . . . . . . . . . 11 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) -> (o e. J -> (a e. o -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.s e. f (o i^i s) =/= (/)))))
40	39	com34 40	. . . . . . . . . 10 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) -> (o e. J -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> (a e. o -> A.s e. f (o i^i s) =/= (/)))))
41	40	com23 36	. . . . . . . . 9 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> (o e. J -> (a e. o -> A.s e. f (o i^i s) =/= (/)))))
42	41	r19.21adv 2181	. . . . . . . 8 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) /\ a e. X) -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))
43	42	ex 402	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) -> (a e. X -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) -> A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))
44	43	imdistand 493	. . . . . 6 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) -> ((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))
45	44	19.21aiv 1664	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (JFneK /\ (f e. Fil /\ X = U.f))) -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))
46	45	exp45 417	. . . 4 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK -> (f e. Fil -> (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))))))
47	46	r19.21adv 2181	. . 3 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK -> A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))))
48	1, 2	isfne2 15481	. . . . . . 7 |- (K e. Top -> (JFneK <-> (X = Y /\ A.j e. J A.b e. j E.k e. K (b e. k /\ k C_ j))))
49	48	3ad2ant2 898	. . . . . 6 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK <-> (X = Y /\ A.j e. J A.b e. j E.k e. K (b e. k /\ k C_ j))))
50	49	adantr 425	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))) -> (JFneK <-> (X = Y /\ A.j e. J A.b e. j E.k e. K (b e. k /\ k C_ j))))
51		simp3 878	. . . . . 6 |- ((J e. Top /\ K e. Top /\ X = Y) -> X = Y)
52	51	adantr 425	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))) -> X = Y)
53	2	topopn 8871	. . . . . . . . . . . . . . . 16 |- (K e. Top -> Y e. K)
54	53	3ad2ant2 898	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ K e. Top /\ X = Y) -> Y e. K)
55	51, 54	eqeltrd 1971	. . . . . . . . . . . . . 14 |- ((J e. Top /\ K e. Top /\ X = Y) -> X e. K)
56	55	ad2antrr 440	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) /\ j = X) -> X e. K)
57		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (j = X -> (b e. j <-> b e. X))
58	57	biimpac 462	. . . . . . . . . . . . . . 15 |- ((b e. j /\ j = X) -> b e. X)
59	58	adantll 428	. . . . . . . . . . . . . 14 |- (((j e. J /\ b e. j) /\ j = X) -> b e. X)
60	59	adantll 428	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) /\ j = X) -> b e. X)
61		eqimss2 2667	. . . . . . . . . . . . . 14 |- (j = X -> X C_ j)
62	61	adantl 424	. . . . . . . . . . . . 13 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) /\ j = X) -> X C_ j)
63		eleq2 1958	. . . . . . . . . . . . . . 15 |- (k = X -> (b e. k <-> b e. X))
64		sseq1 2637	. . . . . . . . . . . . . . 15 |- (k = X -> (k C_ j <-> X C_ j))
65	63, 64	anbi12d 690	. . . . . . . . . . . . . 14 |- (k = X -> ((b e. k /\ k C_ j) <-> (b e. X /\ X C_ j)))
66	65	rcla4ev 2381	. . . . . . . . . . . . 13 |- ((X e. K /\ (b e. X /\ X C_ j)) -> E.k e. K (b e. k /\ k C_ j))
67	56, 60, 62, 66	syl12anc 1098	. . . . . . . . . . . 12 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) /\ j = X) -> E.k e. K (b e. k /\ k C_ j))
68	67	ex 402	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> (j = X -> E.k e. K (b e. k /\ k C_ j)))
69	68	a1dd 53	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> (j = X -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> E.k e. K (b e. k /\ k C_ j))))
70		uniexg 3795	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> U.J e. _V)
71	70, 1	syl5eqel 1975	. . . . . . . . . . . . . . . 16 |- (J e. Top -> X e. _V)
72	71	3ad2ant1 897	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ K e. Top /\ X = Y) -> X e. _V)
73	72	adantr 425	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> X e. _V)
74		difss 2735	. . . . . . . . . . . . . . 15 |- (X \ j) C_ X
75	74	a1i 8	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (X \ j) C_ X)
76	1	eltopss 8872	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ j e. J) -> j C_ X)
77	76	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ X = Y) /\ j e. J) -> j C_ X)
78	77	adantrr 431	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> j C_ X)
79		dfss4 2827	. . . . . . . . . . . . . . . . . . 19 |- (j C_ X <-> (X \ (X \ j)) = j)
80	78, 79	sylib 215	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> (X \ (X \ j)) = j)
81		dif0 2943	. . . . . . . . . . . . . . . . . . 19 |- (X \ (/)) = X
82	81	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> (X \ (/)) = X)
83	80, 82	eqeq12d 1899	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> ((X \ (X \ j)) = (X \ (/)) <-> j = X))
84		difeq2 2719	. . . . . . . . . . . . . . . . 17 |- ((X \ j) = (/) -> (X \ (X \ j)) = (X \ (/)))
85	83, 84	syl5bi 225	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> ((X \ j) = (/) -> j = X))
86	85	necon3d 2041	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> (j =/= X -> (X \ j) =/= (/)))
87	86	impr 422	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (X \ j) =/= (/))
88		supfil 15560	. . . . . . . . . . . . . . 15 |- ((X e. _V /\ (X \ j) C_ X /\ (X \ j) =/= (/)) -> ({g | (g C_ X /\ (X \ j) C_ g)} e. Fil /\ X = U.{g | (g C_ X /\ (X \ j) C_ g)}))
89	88	simplld 348	. . . . . . . . . . . . . 14 |- ((X e. _V /\ (X \ j) C_ X /\ (X \ j) =/= (/)) -> {g | (g C_ X /\ (X \ j) C_ g)} e. Fil)
90	73, 75, 87, 89	syl111anc 1100	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> {g | (g C_ X /\ (X \ j) C_ g)} e. Fil)
91		unieq 3185	. . . . . . . . . . . . . . . 16 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> U.f = U.{g | (g C_ X /\ (X \ j) C_ g)})
92	91	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> (X = U.f <-> X = U.{g | (g C_ X /\ (X \ j) C_ g)}))
93		raleq 2266	. . . . . . . . . . . . . . . . . . . 20 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> (A.t e. f (p i^i t) =/= (/) <-> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)))
94	93	imbi2d 674	. . . . . . . . . . . . . . . . . . 19 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> ((a e. p -> A.t e. f (p i^i t) =/= (/)) <-> (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))))
95	94	ralbidv 2123	. . . . . . . . . . . . . . . . . 18 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> (A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)) <-> A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))))
96	95	anbi2d 678	. . . . . . . . . . . . . . . . 17 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> ((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) <-> (a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)))))
97		raleq 2266	. . . . . . . . . . . . . . . . . . . 20 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> (A.s e. f (o i^i s) =/= (/) <-> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))
98	97	imbi2d 674	. . . . . . . . . . . . . . . . . . 19 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> ((a e. o -> A.s e. f (o i^i s) =/= (/)) <-> (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))
99	98	ralbidv 2123	. . . . . . . . . . . . . . . . . 18 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> (A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)) <-> A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))
100	99	anbi2d 678	. . . . . . . . . . . . . . . . 17 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> ((a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))) <-> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))))
101	96, 100	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> (((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))) <-> ((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))))
102	101	albidv 1656	. . . . . . . . . . . . . . 15 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> (A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))) <-> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))))
103	92, 102	imbi12d 688	. . . . . . . . . . . . . 14 |- (f = {g | (g C_ X /\ (X \ j) C_ g)} -> ((X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) <-> (X = U.{g | (g C_ X /\ (X \ j) C_ g)} -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))))))
104	103	rcla4v 2376	. . . . . . . . . . . . 13 |- ({g | (g C_ X /\ (X \ j) C_ g)} e. Fil -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> (X = U.{g | (g C_ X /\ (X \ j) C_ g)} -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))))))
105	90, 104	syl 12	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> (X = U.{g | (g C_ X /\ (X \ j) C_ g)} -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))))))
106	88	simprd 352	. . . . . . . . . . . . . 14 |- ((X e. _V /\ (X \ j) C_ X /\ (X \ j) =/= (/)) -> X = U.{g | (g C_ X /\ (X \ j) C_ g)})
107	73, 75, 87, 106	syl111anc 1100	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> X = U.{g | (g C_ X /\ (X \ j) C_ g)})
108	77	sseld 2619	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ X = Y) /\ j e. J) -> (b e. j -> b e. X))
109	108	impr 422	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> b e. X)
110	109	adantrr 431	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> b e. X)
111		simprll 456	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> j e. J)
112		simprlr 457	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> b e. j)
113		ssid 2634	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X \ j) C_ (X \ j)
114	74, 113	pm3.2i 307	. . . . . . . . . . . . . . . . . . . . . 22 |- ((X \ j) C_ X /\ (X \ j) C_ (X \ j))
115		difexg 3458	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (X e. _V -> (X \ j) e. _V)
116		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (g = (X \ j) -> (g C_ X <-> (X \ j) C_ X))
117		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (g = (X \ j) -> ((X \ j) C_ g <-> (X \ j) C_ (X \ j)))
118	116, 117	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (g = (X \ j) -> ((g C_ X /\ (X \ j) C_ g) <-> ((X \ j) C_ X /\ (X \ j) C_ (X \ j))))
119	118	elabg 2405	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((X \ j) e. _V -> ((X \ j) e. {g | (g C_ X /\ (X \ j) C_ g)} <-> ((X \ j) C_ X /\ (X \ j) C_ (X \ j))))
120	71, 115, 119	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (J e. Top -> ((X \ j) e. {g | (g C_ X /\ (X \ j) C_ g)} <-> ((X \ j) C_ X /\ (X \ j) C_ (X \ j))))
121	120	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ K e. Top /\ X = Y) -> ((X \ j) e. {g | (g C_ X /\ (X \ j) C_ g)} <-> ((X \ j) C_ X /\ (X \ j) C_ (X \ j))))
122	121	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> ((X \ j) e. {g | (g C_ X /\ (X \ j) C_ g)} <-> ((X \ j) C_ X /\ (X \ j) C_ (X \ j))))
123	114, 122	mpbiri 211	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (X \ j) e. {g | (g C_ X /\ (X \ j) C_ g)})
124		difdisj 2945	. . . . . . . . . . . . . . . . . . . . . 22 |- (j i^i (X \ j)) = (/)
125	124	a1i 8	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (j i^i (X \ j)) = (/))
126		ineq2 2790	. . . . . . . . . . . . . . . . . . . . . . 23 |- (s = (X \ j) -> (j i^i s) = (j i^i (X \ j)))
127	126	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . 22 |- (s = (X \ j) -> ((j i^i s) = (/) <-> (j i^i (X \ j)) = (/)))
128	127	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . 21 |- (((X \ j) e. {g | (g C_ X /\ (X \ j) C_ g)} /\ (j i^i (X \ j)) = (/)) -> E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (j i^i s) = (/))
129	123, 125, 128	syl11anc 524	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (j i^i s) = (/))
130		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . 22 |- (o = j -> (b e. o <-> b e. j))
131		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (o = j -> (o i^i s) = (j i^i s))
132	131	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . 23 |- (o = j -> ((o i^i s) = (/) <-> (j i^i s) = (/)))
133	132	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . 22 |- (o = j -> (E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/) <-> E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (j i^i s) = (/)))
134	130, 133	anbi12d 690	. . . . . . . . . . . . . . . . . . . . 21 |- (o = j -> ((b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) <-> (b e. j /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (j i^i s) = (/))))
135	134	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . 20 |- ((j e. J /\ (b e. j /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (j i^i s) = (/))) -> E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)))
136	111, 112, 129, 135	syl12anc 1098	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)))
137		simprl 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> p e. K)
138		simprrl 458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> b e. p)
139		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- t e. _V
140		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (g = t -> (g C_ X <-> t C_ X))
141		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (g = t -> ((X \ j) C_ g <-> (X \ j) C_ t))
142	140, 141	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (g = t -> ((g C_ X /\ (X \ j) C_ g) <-> (t C_ X /\ (X \ j) C_ t)))
143	139, 142	elab 2403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (t e. {g | (g C_ X /\ (X \ j) C_ g)} <-> (t C_ X /\ (X \ j) C_ t))
144	143	simprbi 353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (t e. {g | (g C_ X /\ (X \ j) C_ g)} -> (X \ j) C_ t)
145	144	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) /\ (t e. {g | (g C_ X /\ (X \ j) C_ g)} /\ ((p i^i t) = (/) /\ b e. p))) -> (X \ j) C_ t)
146		sslin 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((X \ j) C_ t -> (p i^i (X \ j)) C_ (p i^i t))
147	145, 146	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) /\ (t e. {g | (g C_ X /\ (X \ j) C_ g)} /\ ((p i^i t) = (/) /\ b e. p))) -> (p i^i (X \ j)) C_ (p i^i t))
148		simprrl 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) /\ (t e. {g | (g C_ X /\ (X \ j) C_ g)} /\ ((p i^i t) = (/) /\ b e. p))) -> (p i^i t) = (/))
149	147, 148	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) /\ (t e. {g | (g C_ X /\ (X \ j) C_ g)} /\ ((p i^i t) = (/) /\ b e. p))) -> (p i^i (X \ j)) C_ (/))
150		ss0 2902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((p i^i (X \ j)) C_ (/) -> (p i^i (X \ j)) = (/))
151	149, 150	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) /\ (t e. {g | (g C_ X /\ (X \ j) C_ g)} /\ ((p i^i t) = (/) /\ b e. p))) -> (p i^i (X \ j)) = (/))
152	151	exp45 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) -> (t e. {g | (g C_ X /\ (X \ j) C_ g)} -> ((p i^i t) = (/) -> (b e. p -> (p i^i (X \ j)) = (/)))))
153	152	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) -> (E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/) -> (b e. p -> (p i^i (X \ j)) = (/))))
154	153	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) -> (b e. p -> (E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/) -> (p i^i (X \ j)) = (/))))
155	154	imp3a 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ p e. K) -> ((b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)) -> (p i^i (X \ j)) = (/)))
156	155	impr 422	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> (p i^i (X \ j)) = (/))
157	2	eltopss 8872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((K e. Top /\ p e. K) -> p C_ Y)
158	157	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ K e. Top /\ X = Y) /\ p e. K) -> p C_ Y)
159	51	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((J e. Top /\ K e. Top /\ X = Y) /\ p e. K) -> X = Y)
160	158, 159	sseqtr4d 2654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ K e. Top /\ X = Y) /\ p e. K) -> p C_ X)
161	160	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> p C_ X)
162		reldisj 2916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (p C_ X -> ((p i^i (X \ j)) = (/) <-> p C_ (X \ (X \ j))))
163	161, 162	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> ((p i^i (X \ j)) = (/) <-> p C_ (X \ (X \ j))))
164	156, 163	mpbid 212	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> p C_ (X \ (X \ j)))
165	78	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> j C_ X)
166	165	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> j C_ X)
167	166, 79	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> (X \ (X \ j)) = j)
168	164, 167	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> p C_ j)
169		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k = p -> (b e. k <-> b e. p))
170		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k = p -> (k C_ j <-> p C_ j))
171	169, 170	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k = p -> ((b e. k /\ k C_ j) <-> (b e. p /\ p C_ j)))
172	171	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((p e. K /\ (b e. p /\ p C_ j)) -> E.k e. K (b e. k /\ k C_ j))
173	137, 138, 168, 172	syl12anc 1098	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) /\ (p e. K /\ (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> E.k e. K (b e. k /\ k C_ j))
174	173	exp32 408	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (p e. K -> ((b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)) -> E.k e. K (b e. k /\ k C_ j))))
175	174	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)) -> E.k e. K (b e. k /\ k C_ j)))
176	175	imim2d 28	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> ((E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/))) -> (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.k e. K (b e. k /\ k C_ j))))
177	136, 176	mpid 58	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> ((E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/))) -> E.k e. K (b e. k /\ k C_ j)))
178	177	imim2d 28	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> ((b e. X -> (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> (b e. X -> E.k e. K (b e. k /\ k C_ j))))
179	110, 178	mpid 58	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> ((b e. X -> (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))) -> E.k e. K (b e. k /\ k C_ j)))
180		imdistan 490	. . . . . . . . . . . . . . . . 17 |- ((b e. X -> (A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)) -> A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))) <-> ((b e. X /\ A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (b e. X /\ A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))))
181		con3 110	. . . . . . . . . . . . . . . . . . 19 |- ((A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)) -> A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))) -> (-. A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)) -> -. A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))))
182		nne 2021	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (-. (o i^i s) =/= (/) <-> (o i^i s) = (/))
183	182	rexbii 2128	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.s e. {g | (g C_ X /\ (X \ j) C_ g)} -. (o i^i s) =/= (/) <-> E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/))
184		rexnal 2114	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.s e. {g | (g C_ X /\ (X \ j) C_ g)} -. (o i^i s) =/= (/) <-> -. A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))
185	183, 184	bitr3i 192	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/) <-> -. A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))
186	185	anbi2i 538	. . . . . . . . . . . . . . . . . . . . 21 |- ((b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) <-> (b e. o /\ -. A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))
187	186	rexbii 2128	. . . . . . . . . . . . . . . . . . . 20 |- (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) <-> E.o e. J (b e. o /\ -. A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))
188		rexanali 2144	. . . . . . . . . . . . . . . . . . . 20 |- (E.o e. J (b e. o /\ -. A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)) <-> -. A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))
189	187, 188	bitri 190	. . . . . . . . . . . . . . . . . . 19 |- (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) <-> -. A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))
190		nne 2021	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (-. (p i^i t) =/= (/) <-> (p i^i t) = (/))
191	190	rexbii 2128	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.t e. {g | (g C_ X /\ (X \ j) C_ g)} -. (p i^i t) =/= (/) <-> E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/))
192		rexnal 2114	. . . . . . . . . . . . . . . . . . . . . . 23 |- (E.t e. {g | (g C_ X /\ (X \ j) C_ g)} -. (p i^i t) =/= (/) <-> -. A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))
193	191, 192	bitr3i 192	. . . . . . . . . . . . . . . . . . . . . 22 |- (E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/) <-> -. A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))
194	193	anbi2i 538	. . . . . . . . . . . . . . . . . . . . 21 |- ((b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)) <-> (b e. p /\ -. A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)))
195	194	rexbii 2128	. . . . . . . . . . . . . . . . . . . 20 |- (E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)) <-> E.p e. K (b e. p /\ -. A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)))
196		rexanali 2144	. . . . . . . . . . . . . . . . . . . 20 |- (E.p e. K (b e. p /\ -. A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)) <-> -. A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)))
197	195, 196	bitri 190	. . . . . . . . . . . . . . . . . . 19 |- (E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)) <-> -. A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)))
198	181, 189, 197	3imtr4g 612	. . . . . . . . . . . . . . . . . 18 |- ((A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)) -> A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))) -> (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/))))
199	198	imim2i 11	. . . . . . . . . . . . . . . . 17 |- ((b e. X -> (A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)) -> A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))) -> (b e. X -> (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))))
200	180, 199	sylbir 218	. . . . . . . . . . . . . . . 16 |- (((b e. X /\ A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (b e. X /\ A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))) -> (b e. X -> (E.o e. J (b e. o /\ E.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) = (/)) -> E.p e. K (b e. p /\ E.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) = (/)))))
201	179, 200	syl5 20	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (((b e. X /\ A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (b e. X /\ A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))) -> E.k e. K (b e. k /\ k C_ j)))
202		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- (a = b -> (a e. X <-> b e. X))
203		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (a = b -> (a e. p <-> b e. p))
204	203	imbi1d 675	. . . . . . . . . . . . . . . . . . 19 |- (a = b -> ((a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)) <-> (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))))
205	204	ralbidv 2123	. . . . . . . . . . . . . . . . . 18 |- (a = b -> (A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)) <-> A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))))
206	202, 205	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (a = b -> ((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) <-> (b e. X /\ A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/)))))
207		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (a = b -> (a e. o <-> b e. o))
208	207	imbi1d 675	. . . . . . . . . . . . . . . . . . 19 |- (a = b -> ((a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)) <-> (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))
209	208	ralbidv 2123	. . . . . . . . . . . . . . . . . 18 |- (a = b -> (A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)) <-> A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))
210	202, 209	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (a = b -> ((a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))) <-> (b e. X /\ A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))))
211	206, 210	imbi12d 688	. . . . . . . . . . . . . . . 16 |- (a = b -> (((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))) <-> ((b e. X /\ A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (b e. X /\ A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))))
212	211	a4v 1649	. . . . . . . . . . . . . . 15 |- (A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))) -> ((b e. X /\ A.p e. K (b e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (b e. X /\ A.o e. J (b e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))))
213	201, 212	syl5 20	. . . . . . . . . . . . . 14 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/)))) -> E.k e. K (b e. k /\ k C_ j)))
214	213	imim2d 28	. . . . . . . . . . . . 13 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> ((X = U.{g | (g C_ X /\ (X \ j) C_ g)} -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))) -> (X = U.{g | (g C_ X /\ (X \ j) C_ g)} -> E.k e. K (b e. k /\ k C_ j))))
215	107, 214	mpid 58	. . . . . . . . . . . 12 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> ((X = U.{g | (g C_ X /\ (X \ j) C_ g)} -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. {g | (g C_ X /\ (X \ j) C_ g)} (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. {g | (g C_ X /\ (X \ j) C_ g)} (o i^i s) =/= (/))))) -> E.k e. K (b e. k /\ k C_ j)))
216	105, 215	syld 30	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ X = Y) /\ ((j e. J /\ b e. j) /\ j =/= X)) -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> E.k e. K (b e. k /\ k C_ j)))
217	216	expr 418	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> (j =/= X -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> E.k e. K (b e. k /\ k C_ j))))
218	69, 217	pm2.61dne 2091	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (j e. J /\ b e. j)) -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> E.k e. K (b e. k /\ k C_ j)))
219	218	ex 402	. . . . . . . 8 |- ((J e. Top /\ K e. Top /\ X = Y) -> ((j e. J /\ b e. j) -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> E.k e. K (b e. k /\ k C_ j))))
220	219	com23 36	. . . . . . 7 |- ((J e. Top /\ K e. Top /\ X = Y) -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> ((j e. J /\ b e. j) -> E.k e. K (b e. k /\ k C_ j))))
221	220	imp 377	. . . . . 6 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))) -> ((j e. J /\ b e. j) -> E.k e. K (b e. k /\ k C_ j)))
222	221	r19.21aivv 2183	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))) -> A.j e. J A.b e. j E.k e. K (b e. k /\ k C_ j))
223	50, 52, 222	mpbir2and 802	. . . 4 |- (((J e. Top /\ K e. Top /\ X = Y) /\ A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))) -> JFneK)
224	223	ex 402	. . 3 |- ((J e. Top /\ K e. Top /\ X = Y) -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) -> JFneK))
225	47, 224	impbid 574	. 2 |- ((J e. Top /\ K e. Top /\ X = Y) -> (JFneK <-> A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))))
226		eleq2 1958	. . . . . . . . . . . 12 |- (X = Y -> (a e. X <-> a e. Y))
227	226	3ad2ant3 899	. . . . . . . . . . 11 |- ((J e. Top /\ K e. Top /\ X = Y) -> (a e. X <-> a e. Y))
228	227	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> (a e. X <-> a e. Y))
229	228	anbi1d 679	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> ((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) <-> (a e. Y /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)))))
230		simp2 877	. . . . . . . . . . 11 |- ((J e. Top /\ K e. Top /\ X = Y) -> K e. Top)
231	230	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> K e. Top)
232		simprl 450	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> f e. Fil)
233	51	adantr 425	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> X = Y)
234		simprr 451	. . . . . . . . . . 11 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> X = U.f)
235	233, 234	eqtr3d 1927	. . . . . . . . . 10 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> Y = U.f)
236		eqid 1884	. . . . . . . . . . 11 |- U.f = U.f
237	2, 236	isfclus 15606	. . . . . . . . . 10 |- ((K e. Top /\ f e. Fil /\ Y = U.f) -> (a e. ((fClus` K)` f) <-> (a e. Y /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)))))
238	231, 232, 235, 237	syl111anc 1100	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> (a e. ((fClus` K)` f) <-> (a e. Y /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/)))))
239	229, 238	bitr4d 590	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> ((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) <-> a e. ((fClus` K)` f)))
240	1, 236	isfclus 15606	. . . . . . . . . . 11 |- ((J e. Top /\ f e. Fil /\ X = U.f) -> (a e. ((fClus` J)` f) <-> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))
241	240	3expb 1068	. . . . . . . . . 10 |- ((J e. Top /\ (f e. Fil /\ X = U.f)) -> (a e. ((fClus` J)` f) <-> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))
242	241	3ad2antl1 1038	. . . . . . . . 9 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> (a e. ((fClus` J)` f) <-> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))))
243	242	bicomd 580	. . . . . . . 8 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> ((a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))) <-> a e. ((fClus` J)` f)))
244	239, 243	imbi12d 688	. . . . . . 7 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> (((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))) <-> (a e. ((fClus` K)` f) -> a e. ((fClus` J)` f))))
245	244	albidv 1656	. . . . . 6 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> (A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))) <-> A.a(a e. ((fClus` K)` f) -> a e. ((fClus` J)` f))))
246		dfss2 2610	. . . . . 6 |- (((fClus` K)` f) C_ ((fClus` J)` f) <-> A.a(a e. ((fClus` K)` f) -> a e. ((fClus` J)` f)))
247	245, 246	syl6bbr 597	. . . . 5 |- (((J e. Top /\ K e. Top /\ X = Y) /\ (f e. Fil /\ X = U.f)) -> (A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))) <-> ((fClus` K)` f) C_ ((fClus` J)` f)))
248	247	anassrs 489	. . . 4 |- ((((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) /\ X = U.f) -> (A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/)))) <-> ((fClus` K)` f) C_ ((fClus` J)` f)))
249	248	pm5.74da 646	. . 3 |- (((J e. Top /\ K e. Top /\ X = Y) /\ f e. Fil) -> ((X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) <-> (X = U.f -> ((fClus` K)` f) C_ ((fClus` J)` f))))
250	249	ralbidva 2119	. 2 |- ((J e. Top /\ K e. Top /\ X = Y) -> (A.f e. Fil (X = U.f -> A.a((a e. X /\ A.p e. K (a e. p -> A.t e. f (p i^i t) =/= (/))) -> (a e. X /\ A.o e. J (a e. o -> A.s e. f (o i^i s) =/= (/))))) <-> A.f e. Fil (X = U.f -> ((fClus` K)` f) C_ ((fClus` J)` f))))
251	3, 225, 250	3bitrd 603	1 |- ((J e. Top /\ K e. Top /\ X = Y) -> (J C_ K <-> A.f e. Fil (X = U.f -> ((fClus` K)` f) C_ ((fClus` J)` f))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177   class class class wbr 3338  ` cfv 3998  Topctop 8857  Filcfil 10264  Fnecfne 15457  fCluscfclus 15582

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-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-ral 2109  df-rex 2110  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-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-id 3586  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-fv 4014  df-top 8861  df-bases 8863  df-topgen 8864  df-cld 8939  df-ntr 8940  df-cls 8941  df-fil 10265  df-fne 15463  df-fclus 15584

Copyright terms: Public domain