Theorem compfipin0 15436

Description: If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty.

Assertion

Ref	Expression
compfipin0	|- (J e. Top -> (J e. Comp <-> A.x e. ~P (Clsd` J)((/) e/ ( fi ` x) -> |^|x =/= (/))))

Distinct variable group:   x,J

Proof of Theorem compfipin0

Step	Hyp	Ref	Expression
1		iscomp 10330	. . 3 |- (J e. Comp <-> (J e. Top /\ A.y e. ~P J(U.J = U.y -> E.z e. (~Py i^i Fin)U.J = U.z)))
2	1	baib 749	. 2 |- (J e. Top -> (J e. Comp <-> A.y e. ~P J(U.J = U.y -> E.z e. (~Py i^i Fin)U.J = U.z)))
3		con34b 183	. . . 4 |- ((U.J = U.y -> E.z e. (~Py i^i Fin)U.J = U.z) <-> (-. E.z e. (~Py i^i Fin)U.J = U.z -> -. U.J = U.y))
4	3	ralbii 2127	. . 3 |- (A.y e. ~P J(U.J = U.y -> E.z e. (~Py i^i Fin)U.J = U.z) <-> A.y e. ~P J(-. E.z e. (~Py i^i Fin)U.J = U.z -> -. U.J = U.y))
5	4	a1i 8	. 2 |- (J e. Top -> (A.y e. ~P J(U.J = U.y -> E.z e. (~Py i^i Fin)U.J = U.z) <-> A.y e. ~P J(-. E.z e. (~Py i^i Fin)U.J = U.z -> -. U.J = U.y)))
6		cnvimass 4286	. . . . . . . . . 10 |- (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))}
7		eqid 1884	. . . . . . . . . . . . 13 |- U.J = U.J
8		eqid 1884	. . . . . . . . . . . . 13 |- {<.r, s>. | (r e. J /\ s = (U.J \ r))} = {<.r, s>. | (r e. J /\ s = (U.J \ r))}
9	7, 8	opncldf1 15402	. . . . . . . . . . . 12 |- (J e. Top -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J))
10		f1ofn 4636	. . . . . . . . . . . 12 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))} Fn J)
11		fndm 4512	. . . . . . . . . . . 12 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))} Fn J -> dom {<.r, s>. | (r e. J /\ s = (U.J \ r))} = J)
12	9, 10, 11	3syl 24	. . . . . . . . . . 11 |- (J e. Top -> dom {<.r, s>. | (r e. J /\ s = (U.J \ r))} = J)
13	12	sseq2d 2645	. . . . . . . . . 10 |- (J e. Top -> ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))} <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) C_ J))
14	6, 13	mpbii 210	. . . . . . . . 9 |- (J e. Top -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) C_ J)
15		elpw2g 3463	. . . . . . . . 9 |- (J e. Top -> ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) e. ~PJ <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) C_ J))
16	14, 15	mpbird 213	. . . . . . . 8 |- (J e. Top -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) e. ~PJ)
17	16	adantr 425	. . . . . . 7 |- ((J e. Top /\ x e. ~P(Clsd` J)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) e. ~PJ)
18		pweq 3036	. . . . . . . . . . 11 |- (y = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> ~Py = ~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))
19	18	ineq1d 2795	. . . . . . . . . 10 |- (y = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> (~Py i^i Fin) = (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin))
20	19	raleqdv 2269	. . . . . . . . 9 |- (y = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> (A.z e. (~Py i^i Fin) -. U.J = U.z <-> A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z))
21		unieq 3185	. . . . . . . . . . 11 |- (y = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> U.y = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))
22	21	eqeq2d 1895	. . . . . . . . . 10 |- (y = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> (U.J = U.y <-> U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)))
23	22	notbid 673	. . . . . . . . 9 |- (y = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> (-. U.J = U.y <-> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)))
24	20, 23	imbi12d 688	. . . . . . . 8 |- (y = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> ((A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) <-> (A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))))
25	24	rcla4v 2376	. . . . . . 7 |- ((`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) e. ~PJ -> (A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) -> (A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))))
26	17, 25	syl 12	. . . . . 6 |- ((J e. Top /\ x e. ~P(Clsd` J)) -> (A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) -> (A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))))
27		pm2.1 718	. . . . . . . . . . 11 |- (-. x = (/) \/ x = (/))
28		neq0 2885	. . . . . . . . . . . . . . 15 |- (-. x = (/) <-> E.c c e. x)
29		ssel 2615	. . . . . . . . . . . . . . . . . . 19 |- (x C_ (Clsd` J) -> (c e. x -> c e. (Clsd` J)))
30	7	cldss 8947	. . . . . . . . . . . . . . . . . . . . . 22 |- ((J e. Top /\ c e. (Clsd` J)) -> c C_ U.J)
31		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (U.J = (/) -> (c C_ U.J <-> c C_ (/)))
32	31	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (U.J = (/) -> (c C_ U.J -> c C_ (/)))
33		ss0 2902	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c C_ (/) -> c = (/))
34		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (c = (/) -> (c e. x <-> (/) e. x))
35	34	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((c = (/) /\ c e. x) -> (/) e. x)
36		snssi 3129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((/) e. x -> {(/)} C_ x)
37		p0ex 3495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- {(/)} e. _V
38	37	elpw 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ({(/)} e. ~Px <-> {(/)} C_ x)
39	36, 38	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((/) e. x -> {(/)} e. ~Px)
40		snfi 5491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- {(/)} e. Fin
41	39, 40	jctir 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((/) e. x -> ({(/)} e. ~Px /\ {(/)} e. Fin))
42		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ({(/)} e. (~Px i^i Fin) <-> ({(/)} e. ~Px /\ {(/)} e. Fin))
43	41, 42	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((/) e. x -> {(/)} e. (~Px i^i Fin))
44		0ex 3446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (/) e. _V
45	44	intsn 3252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- |^|{(/)} = (/)
46	45	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (/) = |^|{(/)}
47	46	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((/) e. x -> (/) = |^|{(/)})
48		inteq 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (w = {(/)} -> |^|w = |^|{(/)})
49	48	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = {(/)} -> ((/) = |^|w <-> (/) = |^|{(/)}))
50	49	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (({(/)} e. (~Px i^i Fin) /\ (/) = |^|{(/)}) -> E.w e. (~Px i^i Fin)(/) = |^|w)
51	43, 47, 50	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((/) e. x -> E.w e. (~Px i^i Fin)(/) = |^|w)
52	35, 51	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((c = (/) /\ c e. x) -> E.w e. (~Px i^i Fin)(/) = |^|w)
53		dfrex2 2116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.w e. (~Px i^i Fin)(/) = |^|w <-> -. A.w e. (~Px i^i Fin) -. (/) = |^|w)
54	52, 53	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((c = (/) /\ c e. x) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w)
55	54	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (c = (/) -> (c e. x -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))
56	33, 55	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (c C_ (/) -> (c e. x -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))
57	32, 56	syl6com 64	. . . . . . . . . . . . . . . . . . . . . . 23 |- (c C_ U.J -> (U.J = (/) -> (c e. x -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w)))
58	57	com23 36	. . . . . . . . . . . . . . . . . . . . . 22 |- (c C_ U.J -> (c e. x -> (U.J = (/) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w)))
59	30, 58	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ c e. (Clsd` J)) -> (c e. x -> (U.J = (/) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w)))
60	59	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- (J e. Top -> (c e. (Clsd` J) -> (c e. x -> (U.J = (/) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))))
61	60	com13 37	. . . . . . . . . . . . . . . . . . 19 |- (c e. x -> (c e. (Clsd` J) -> (J e. Top -> (U.J = (/) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))))
62	29, 61	sylcom 62	. . . . . . . . . . . . . . . . . 18 |- (x C_ (Clsd` J) -> (c e. x -> (J e. Top -> (U.J = (/) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))))
63	62	com3l 38	. . . . . . . . . . . . . . . . 17 |- (c e. x -> (J e. Top -> (x C_ (Clsd` J) -> (U.J = (/) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))))
64	63	imp4c 393	. . . . . . . . . . . . . . . 16 |- (c e. x -> (((J e. Top /\ x C_ (Clsd` J)) /\ U.J = (/)) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))
65	64	19.23aiv 1674	. . . . . . . . . . . . . . 15 |- (E.c c e. x -> (((J e. Top /\ x C_ (Clsd` J)) /\ U.J = (/)) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))
66	28, 65	sylbi 216	. . . . . . . . . . . . . 14 |- (-. x = (/) -> (((J e. Top /\ x C_ (Clsd` J)) /\ U.J = (/)) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))
67	66	com12 14	. . . . . . . . . . . . 13 |- (((J e. Top /\ x C_ (Clsd` J)) /\ U.J = (/)) -> (-. x = (/) -> -. A.w e. (~Px i^i Fin) -. (/) = |^|w))
68		vn0 2882	. . . . . . . . . . . . . . . . 17 |- _V =/= (/)
69		df-ne 2019	. . . . . . . . . . . . . . . . 17 |- (_V =/= (/) <-> -. _V = (/))
70	68, 69	mpbi 206	. . . . . . . . . . . . . . . 16 |- -. _V = (/)
71		int0 3230	. . . . . . . . . . . . . . . . . . 19 |- |^|(/) = _V
72	71	eqeq1i 1891	. . . . . . . . . . . . . . . . . 18 |- (|^|(/) = (/) <-> _V = (/))
73	72	biimpi 168	. . . . . . . . . . . . . . . . 17 |- (|^|(/) = (/) -> _V = (/))
74	73	eqcoms 1887	. . . . . . . . . . . . . . . 16 |- ((/) = |^|(/) -> _V = (/))
75	70, 74	mto 121	. . . . . . . . . . . . . . 15 |- -. (/) = |^|(/)
76		inteq 3217	. . . . . . . . . . . . . . . 16 |- (x = (/) -> |^|x = |^|(/))
77	76	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (x = (/) -> ((/) = |^|x <-> (/) = |^|(/)))
78	75, 77	mtbiri 785	. . . . . . . . . . . . . 14 |- (x = (/) -> -. (/) = |^|x)
79	78	a1i 8	. . . . . . . . . . . . 13 |- (((J e. Top /\ x C_ (Clsd` J)) /\ U.J = (/)) -> (x = (/) -> -. (/) = |^|x))
80	67, 79	orim12d 624	. . . . . . . . . . . 12 |- (((J e. Top /\ x C_ (Clsd` J)) /\ U.J = (/)) -> ((-. x = (/) \/ x = (/)) -> (-. A.w e. (~Px i^i Fin) -. (/) = |^|w \/ -. (/) = |^|x)))
81	80	ex 402	. . . . . . . . . . 11 |- ((J e. Top /\ x C_ (Clsd` J)) -> (U.J = (/) -> ((-. x = (/) \/ x = (/)) -> (-. A.w e. (~Px i^i Fin) -. (/) = |^|w \/ -. (/) = |^|x))))
82	27, 81	mpii 56	. . . . . . . . . 10 |- ((J e. Top /\ x C_ (Clsd` J)) -> (U.J = (/) -> (-. A.w e. (~Px i^i Fin) -. (/) = |^|w \/ -. (/) = |^|x)))
83		pm4.62 254	. . . . . . . . . 10 |- ((A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) <-> (-. A.w e. (~Px i^i Fin) -. (/) = |^|w \/ -. (/) = |^|x))
84	82, 83	syl6ibr 230	. . . . . . . . 9 |- ((J e. Top /\ x C_ (Clsd` J)) -> (U.J = (/) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x)))
85		visset 2295	. . . . . . . . . 10 |- x e. _V
86	85	elpw 3037	. . . . . . . . 9 |- (x e. ~P(Clsd` J) <-> x C_ (Clsd` J))
87	84, 86	sylan2b 501	. . . . . . . 8 |- ((J e. Top /\ x e. ~P(Clsd` J)) -> (U.J = (/) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x)))
88	87	a1dd 53	. . . . . . 7 |- ((J e. Top /\ x e. ~P(Clsd` J)) -> (U.J = (/) -> ((A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x))))
89		elin 2786	. . . . . . . . . . . . . . . 16 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. (~Px i^i Fin) <-> (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. ~Px /\ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. Fin))
90		funimass2 4492	. . . . . . . . . . . . . . . . . . . 20 |- ((Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))} /\ z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) C_ x)
91		f1ofun 4637	. . . . . . . . . . . . . . . . . . . . 21 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))})
92	9, 91	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (J e. Top -> Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))})
93	90, 92	sylan 497	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) C_ x)
94	93	adantrr 431	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) C_ x)
95	94	3ad2antl1 1038	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) C_ x)
96		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. _V
97	96	funimaex 4496	. . . . . . . . . . . . . . . . . . . . 21 |- (Fun {<.r, s>. | (r e. J /\ s = (U.J \ r))} -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. _V)
98	9, 91, 97	3syl 24	. . . . . . . . . . . . . . . . . . . 20 |- (J e. Top -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. _V)
99	98	3ad2ant1 897	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. _V)
100	99	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. _V)
101		elpwg 3038	. . . . . . . . . . . . . . . . . 18 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. _V -> (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. ~Px <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) C_ x))
102	100, 101	syl 12	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. ~Px <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) C_ x))
103	95, 102	mpbird 213	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. ~Px)
104		simprr 451	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> z e. Fin)
105		f1of1 4634	. . . . . . . . . . . . . . . . . . . . . . 23 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J))
106	9, 105	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (J e. Top -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J))
107	106	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J))
108	107	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J))
109	12	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (J e. Top -> (z C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))} <-> z C_ J))
110	109	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ z C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))}) -> z C_ J)
111		sstr 2625	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))}) -> z C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))})
112	6, 111	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> z C_ dom {<.r, s>. | (r e. J /\ s = (U.J \ r))})
113	110, 112	sylan2 500	. . . . . . . . . . . . . . . . . . . . . 22 |- ((J e. Top /\ z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)) -> z C_ J)
114	113	adantrr 431	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> z C_ J)
115	114	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> z C_ J)
116		f1ores 4654	. . . . . . . . . . . . . . . . . . . 20 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1->(Clsd` J) /\ z C_ J) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))} |` z):z-1-1-onto->({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
117	108, 115, 116	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))} |` z):z-1-1-onto->({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
118	96	f1oen 5457	. . . . . . . . . . . . . . . . . . 19 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))} |` z):z-1-1-onto->({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) -> z ~~ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
119	117, 118	syl 12	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> z ~~ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
120		enfi 5627	. . . . . . . . . . . . . . . . . 18 |- ((({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. _V /\ z ~~ ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z)) -> (z e. Fin <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. Fin))
121	100, 119, 120	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> (z e. Fin <-> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. Fin))
122	104, 121	mpbid 212	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. Fin)
123	89, 103, 122	sylanbrc 527	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. (~Px i^i Fin))
124		inteq 3217	. . . . . . . . . . . . . . . . . 18 |- (w = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) -> |^|w = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
125	124	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (w = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) -> ((/) = |^|w <-> (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z)))
126	125	notbid 673	. . . . . . . . . . . . . . . 16 |- (w = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) -> (-. (/) = |^|w <-> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z)))
127	126	rcla4v 2376	. . . . . . . . . . . . . . 15 |- (({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) e. (~Px i^i Fin) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z)))
128	123, 127	syl 12	. . . . . . . . . . . . . 14 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z)))
129		difeq2 2719	. . . . . . . . . . . . . . . . . . 19 |- (U.J = U.z -> (U.J \ U.J) = (U.J \ U.z))
130	129	ad2antll 443	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (U.J \ U.J) = (U.J \ U.z))
131		difid 2942	. . . . . . . . . . . . . . . . . 18 |- (U.J \ U.J) = (/)
132		uniiun 3306	. . . . . . . . . . . . . . . . . . 19 |- U.z = U_v e. z v
133	132	difeq2i 2723	. . . . . . . . . . . . . . . . . 18 |- (U.J \ U.z) = (U.J \ U_v e. z v)
134	130, 131, 133	3eqtr3g 1952	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (/) = (U.J \ U_v e. z v))
135		simpr 350	. . . . . . . . . . . . . . . . . . . . . 22 |- ((-. U.J = (/) /\ U.J = U.z) -> U.J = U.z)
136		unieq 3185	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z = (/) -> U.z = U.(/))
137		uni0 3205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- U.(/) = (/)
138	136, 137	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z = (/) -> U.z = (/))
139		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((U.J = U.z /\ U.z = (/)) -> U.J = (/))
140	139	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (U.z = (/) -> (U.J = U.z -> U.J = (/)))
141	138, 140	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = (/) -> (U.J = U.z -> U.J = (/)))
142	141	con3d 111	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = (/) -> (-. U.J = (/) -> -. U.J = U.z))
143	142	com12 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- (-. U.J = (/) -> (z = (/) -> -. U.J = U.z))
144	143	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- ((-. U.J = (/) /\ U.J = U.z) -> (z = (/) -> -. U.J = U.z))
145	135, 144	mt2d 126	. . . . . . . . . . . . . . . . . . . . 21 |- ((-. U.J = (/) /\ U.J = U.z) -> -. z = (/))
146	145	adantrl 430	. . . . . . . . . . . . . . . . . . . 20 |- ((-. U.J = (/) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> -. z = (/))
147	146	3ad2antl3 1040	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> -. z = (/))
148		df-ne 2019	. . . . . . . . . . . . . . . . . . 19 |- (z =/= (/) <-> -. z = (/))
149	147, 148	sylibr 217	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> z =/= (/))
150		iindif2 3324	. . . . . . . . . . . . . . . . . 18 |- (z =/= (/) -> |^|_v e. z (U.J \ v) = (U.J \ U_v e. z v))
151	149, 150	syl 12	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> |^|_v e. z (U.J \ v) = (U.J \ U_v e. z v))
152		uniexg 3795	. . . . . . . . . . . . . . . . . . . . . . 23 |- (J e. Top -> U.J e. _V)
153		difexg 3458	. . . . . . . . . . . . . . . . . . . . . . 23 |- (U.J e. _V -> (U.J \ v) e. _V)
154	152, 153	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (J e. Top -> (U.J \ v) e. _V)
155	154	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> (U.J \ v) e. _V)
156	155	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (U.J \ v) e. _V)
157	156	a1d 15	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (v e. z -> (U.J \ v) e. _V))
158	157	r19.21aiv 2175	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> A.v e. z (U.J \ v) e. _V)
159		dfiin2g 3286	. . . . . . . . . . . . . . . . . 18 |- (A.v e. z (U.J \ v) e. _V -> |^|_v e. z (U.J \ v) = |^|{u | E.v e. z u = (U.J \ v)})
160	158, 159	syl 12	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> |^|_v e. z (U.J \ v) = |^|{u | E.v e. z u = (U.J \ v)})
161	134, 151, 160	3eqtr2d 1932	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (/) = |^|{u | E.v e. z u = (U.J \ v)})
162	114	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J e. Top /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> z C_ J)
163	162	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> z C_ J)
164		df-ss 2605	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z C_ J <-> (z i^i J) = z)
165	163, 164	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (z i^i J) = z)
166	165	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> z = (z i^i J))
167	166	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (v e. z <-> v e. (z i^i J)))
168		elin 2786	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. (z i^i J) <-> (v e. z /\ v e. J))
169	167, 168	syl6bb 595	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (v e. z <-> (v e. z /\ v e. J)))
170	169	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> ((v e. z /\ u = (U.J \ v)) <-> ((v e. z /\ v e. J) /\ u = (U.J \ v))))
171		anass 487	. . . . . . . . . . . . . . . . . . . . . 22 |- (((v e. z /\ v e. J) /\ u = (U.J \ v)) <-> (v e. z /\ (v e. J /\ u = (U.J \ v))))
172	170, 171	syl6bb 595	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> ((v e. z /\ u = (U.J \ v)) <-> (v e. z /\ (v e. J /\ u = (U.J \ v)))))
173		df-br 3339	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v{<.r, s>. | (r e. J /\ s = (U.J \ r))}u <-> <.v, u>. e. {<.r, s>. | (r e. J /\ s = (U.J \ r))})
174		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- v e. _V
175		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- u e. _V
176		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (r = v -> (r e. J <-> v e. J))
177		difeq2 2719	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (r = v -> (U.J \ r) = (U.J \ v))
178	177	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (r = v -> (s = (U.J \ r) <-> s = (U.J \ v)))
179	176, 178	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (r = v -> ((r e. J /\ s = (U.J \ r)) <-> (v e. J /\ s = (U.J \ v))))
180		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (s = u -> (s = (U.J \ v) <-> u = (U.J \ v)))
181	180	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (s = u -> ((v e. J /\ s = (U.J \ v)) <-> (v e. J /\ u = (U.J \ v))))
182	174, 175, 179, 181	opelopab 3570	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<.v, u>. e. {<.r, s>. | (r e. J /\ s = (U.J \ r))} <-> (v e. J /\ u = (U.J \ v)))
183	173, 182	bitr2i 191	. . . . . . . . . . . . . . . . . . . . . 22 |- ((v e. J /\ u = (U.J \ v)) <-> v{<.r, s>. | (r e. J /\ s = (U.J \ r))}u)
184	183	anbi2i 538	. . . . . . . . . . . . . . . . . . . . 21 |- ((v e. z /\ (v e. J /\ u = (U.J \ v))) <-> (v e. z /\ v{<.r, s>. | (r e. J /\ s = (U.J \ r))}u))
185	172, 184	syl6bb 595	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> ((v e. z /\ u = (U.J \ v)) <-> (v e. z /\ v{<.r, s>. | (r e. J /\ s = (U.J \ r))}u)))
186	185	rexbidv2 2126	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (E.v e. z u = (U.J \ v) <-> E.v e. z v{<.r, s>. | (r e. J /\ s = (U.J \ r))}u))
187	186	abbidv 2008	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> {u | E.v e. z u = (U.J \ v)} = {u | E.v e. z v{<.r, s>. | (r e. J /\ s = (U.J \ r))}u})
188		dfima2 4265	. . . . . . . . . . . . . . . . . 18 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z) = {u | E.v e. z v{<.r, s>. | (r e. J /\ s = (U.J \ r))}u}
189	187, 188	syl6eqr 1946	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> {u | E.v e. z u = (U.J \ v)} = ({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
190	189	inteqd 3219	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> |^|{u | E.v e. z u = (U.J \ v)} = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
191	161, 190	eqtrd 1925	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) /\ U.J = U.z)) -> (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z))
192	191	expr 418	. . . . . . . . . . . . . 14 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> (U.J = U.z -> (/) = |^|({<.r, s>. | (r e. J /\ s = (U.J \ r))}"z)))
193	128, 192	nsyld 132	. . . . . . . . . . . . 13 |- (((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) /\ (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. U.J = U.z))
194	193	ex 402	. . . . . . . . . . . 12 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> ((z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. U.J = U.z)))
195		elin 2786	. . . . . . . . . . . . 13 |- (z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) <-> (z e. ~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin))
196	96	elpw 3037	. . . . . . . . . . . . . 14 |- (z e. ~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) <-> z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))
197	196	anbi1i 539	. . . . . . . . . . . . 13 |- ((z e. ~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin) <-> (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin))
198	195, 197	bitri 190	. . . . . . . . . . . 12 |- (z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) <-> (z C_ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) /\ z e. Fin))
199	194, 198	syl5ib 223	. . . . . . . . . . 11 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> (z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. U.J = U.z)))
200	199	com23 36	. . . . . . . . . 10 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> (z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -> -. U.J = U.z)))
201	200	r19.21adv 2181	. . . . . . . . 9 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z))
202		difeq2 2719	. . . . . . . . . . . . . . 15 |- ((/) = |^|x -> (U.J \ (/)) = (U.J \ |^|x))
203	202	adantl 424	. . . . . . . . . . . . . 14 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> (U.J \ (/)) = (U.J \ |^|x))
204		dif0 2943	. . . . . . . . . . . . . 14 |- (U.J \ (/)) = U.J
205		intiin 3307	. . . . . . . . . . . . . . . 16 |- |^|x = |^|_v e. x v
206	205	difeq2i 2723	. . . . . . . . . . . . . . 15 |- (U.J \ |^|x) = (U.J \ |^|_v e. x v)
207		iundif2 3322	. . . . . . . . . . . . . . 15 |- U_v e. x (U.J \ v) = (U.J \ |^|_v e. x v)
208	206, 207	eqtr4i 1911	. . . . . . . . . . . . . 14 |- (U.J \ |^|x) = U_v e. x (U.J \ v)
209	203, 204, 208	3eqtr3g 1952	. . . . . . . . . . . . 13 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> U.J = U_v e. x (U.J \ v))
210	154	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) -> (U.J \ v) e. _V)
211	210	adantr 425	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> (U.J \ v) e. _V)
212	211	a1d 15	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> (v e. x -> (U.J \ v) e. _V))
213	212	r19.21aiv 2175	. . . . . . . . . . . . . 14 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> A.v e. x (U.J \ v) e. _V)
214		dfiun2g 3283	. . . . . . . . . . . . . 14 |- (A.v e. x (U.J \ v) e. _V -> U_v e. x (U.J \ v) = U.{u | E.v e. x u = (U.J \ v)})
215	213, 214	syl 12	. . . . . . . . . . . . 13 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> U_v e. x (U.J \ v) = U.{u | E.v e. x u = (U.J \ v)})
216		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) -> J e. Top)
217	216	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ ((/) = |^|x /\ v e. x)) -> J e. Top)
218		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x C_ (Clsd` J) /\ v e. x) -> v e. (Clsd` J))
219	218	adantrl 430	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x C_ (Clsd` J) /\ ((/) = |^|x /\ v e. x)) -> v e. (Clsd` J))
220	219	3ad2antl2 1039	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ ((/) = |^|x /\ v e. x)) -> v e. (Clsd` J))
221	7, 8	opncldf3 15404	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ v e. (Clsd` J)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = (U.J \ v))
222	217, 220, 221	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ ((/) = |^|x /\ v e. x)) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = (U.J \ v))
223	222	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ ((/) = |^|x /\ v e. x)) -> (U.J \ v) = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v))
224	223	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ ((/) = |^|x /\ v e. x)) -> ((U.J \ v) = u <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
225		eqcom 1886	. . . . . . . . . . . . . . . . . . . 20 |- (u = (U.J \ v) <-> (U.J \ v) = u)
226	224, 225	syl5bb 591	. . . . . . . . . . . . . . . . . . 19 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ ((/) = |^|x /\ v e. x)) -> (u = (U.J \ v) <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
227	226	expr 418	. . . . . . . . . . . . . . . . . 18 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> (v e. x -> (u = (U.J \ v) <-> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u)))
228	227	pm5.32d 709	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> ((v e. x /\ u = (U.J \ v)) <-> (v e. x /\ (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u)))
229	228	rexbidv2 2126	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> (E.v e. x u = (U.J \ v) <-> E.v e. x (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u))
230	229	abbidv 2008	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> {u | E.v e. x u = (U.J \ v)} = {u | E.v e. x (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
231		f1ocnv 4651	. . . . . . . . . . . . . . . . . . 19 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1-onto->J)
232		f1ofun 4637	. . . . . . . . . . . . . . . . . . 19 |- (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}:(Clsd` J)-1-1-onto->J -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
233	9, 231, 232	3syl 24	. . . . . . . . . . . . . . . . . 18 |- (J e. Top -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
234	233	3ad2ant1 897	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
235	234	adantr 425	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
236		f1ofo 4643	. . . . . . . . . . . . . . . . . . . . . 22 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-1-1-onto->(Clsd` J) -> {<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-onto->(Clsd` J))
237		forn 4620	. . . . . . . . . . . . . . . . . . . . . 22 |- ({<.r, s>. | (r e. J /\ s = (U.J \ r))}:J-onto->(Clsd` J) -> ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} = (Clsd` J))
238	9, 236, 237	3syl 24	. . . . . . . . . . . . . . . . . . . . 21 |- (J e. Top -> ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} = (Clsd` J))
239	238	sseq2d 2645	. . . . . . . . . . . . . . . . . . . 20 |- (J e. Top -> (x C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} <-> x C_ (Clsd` J)))
240	239	biimpar 461	. . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ x C_ (Clsd` J)) -> x C_ ran {<.r, s>. | (r e. J /\ s = (U.J \ r))})
241		df-rn 4005	. . . . . . . . . . . . . . . . . . 19 |- ran {<.r, s>. | (r e. J /\ s = (U.J \ r))} = dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}
242	240, 241	syl6ss 2663	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ x C_ (Clsd` J)) -> x C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
243	242	3adant3 896	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) -> x C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
244	243	adantr 425	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> x C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))})
245		dfimafn 4720	. . . . . . . . . . . . . . . 16 |- ((Fun `'{<.r, s>. | (r e. J /\ s = (U.J \ r))} /\ x C_ dom `'{<.r, s>. | (r e. J /\ s = (U.J \ r))}) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) = {u | E.v e. x (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
246	235, 244, 245	syl11anc 524	. . . . . . . . . . . . . . 15 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) = {u | E.v e. x (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}` v) = u})
247	230, 246	eqtr4d 1928	. . . . . . . . . . . . . 14 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> {u | E.v e. x u = (U.J \ v)} = (`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))
248	247	unieqd 3188	. . . . . . . . . . . . 13 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> U.{u | E.v e. x u = (U.J \ v)} = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))
249	209, 215, 248	3eqtrd 1929	. . . . . . . . . . . 12 |- (((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) /\ (/) = |^|x) -> U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x))
250	249	ex 402	. . . . . . . . . . 11 |- ((J e. Top /\ x C_ (Clsd` J) /\ -. U.J = (/)) -> ((/) = |^|x -> U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)))
251	250, 86	syl3an2b 1134	. . . . . . . . . 10 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> ((/) = |^|x -> U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)))
252	251	con3d 111	. . . . . . . . 9 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> (-. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) -> -. (/) = |^|x))
253	201, 252	imim12d 69	. . . . . . . 8 |- ((J e. Top /\ x e. ~P(Clsd` J) /\ -. U.J = (/)) -> ((A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x)))
254	253	3expia 1069	. . . . . . 7 |- ((J e. Top /\ x e. ~P(Clsd` J)) -> (-. U.J = (/) -> ((A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x))))
255	88, 254	pm2.61d 141	. . . . . 6 |- ((J e. Top /\ x e. ~P(Clsd` J)) -> ((A.z e. (~P(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x) i^i Fin) -. U.J = U.z -> -. U.J = U.(`'{<.r, s>. | (r e. J /\ s = (U.J \ r))}"x)) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x)))
256	26, 255	syld 30	. . . . 5 |- ((J e. Top /\ x e. ~P(Clsd` J)) -> (A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) -> (A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x)))
257	256	r19.21adva 2182	. . . 4 |- (J e. Top -> (A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) -> A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x)))
258		compfipin0lem 15435	. . . 4 |- (J e. Top -> (A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) -> A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y)))
259	257, 258	impbid 574	. . 3 |- (J e. Top -> (A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) <-> A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x)))
260		ralnex 2113	. . . . 5 |- (A.z e. (~Py i^i Fin) -. U.J = U.z <-> -. E.z e. (~Py i^i Fin)U.J = U.z)
261	260	imbi1i 203	. . . 4 |- ((A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) <-> (-. E.z e. (~Py i^i Fin)U.J = U.z -> -. U.J = U.y))
262	261	ralbii 2127	. . 3 |- (A.y e. ~P J(A.z e. (~Py i^i Fin) -. U.J = U.z -> -. U.J = U.y) <-> A.y e. ~P J(-. E.z e. (~Py i^i Fin)U.J = U.z -> -. U.J = U.y))
263		fiv 10212	. . . . . . . . . 10 |- (x e. _V -> ( fi ` x) = {z | E.w(w C_ x /\ w e. Fin /\ z = |^|w)})
264	85, 263	ax-mp 7	. . . . . . . . 9 |- ( fi ` x) = {z | E.w(w C_ x /\ w e. Fin /\ z = |^|w)}
265	264	eleq2i 1961	. . . . . . . 8 |- ((/) e. ( fi ` x) <-> (/) e. {z | E.w(w C_ x /\ w e. Fin /\ z = |^|w)})
266		eqeq1 1890	. . . . . . . . . . 11 |- (z = (/) -> (z = |^|w <-> (/) = |^|w))
267	266	3anbi3d 1174	. . . . . . . . . 10 |- (z = (/) -> ((w C_ x /\ w e. Fin /\ z = |^|w) <-> (w C_ x /\ w e. Fin /\ (/) = |^|w)))
268	267	exbidv 1657	. . . . . . . . 9 |- (z = (/) -> (E.w(w C_ x /\ w e. Fin /\ z = |^|w) <-> E.w(w C_ x /\ w e. Fin /\ (/) = |^|w)))
269	44, 268	elab 2403	. . . . . . . 8 |- ((/) e. {z | E.w(w C_ x /\ w e. Fin /\ z = |^|w)} <-> E.w(w C_ x /\ w e. Fin /\ (/) = |^|w))
270	265, 269	bitr2i 191	. . . . . . 7 |- (E.w(w C_ x /\ w e. Fin /\ (/) = |^|w) <-> (/) e. ( fi ` x))
271	270	notbii 204	. . . . . 6 |- (-. E.w(w C_ x /\ w e. Fin /\ (/) = |^|w) <-> -. (/) e. ( fi ` x))
272		ralnex 2113	. . . . . . 7 |- (A.w e. (~Px i^i Fin) -. (/) = |^|w <-> -. E.w e. (~Px i^i Fin)(/) = |^|w)
273		df-rex 2110	. . . . . . . 8 |- (E.w e. (~Px i^i Fin)(/) = |^|w <-> E.w(w e. (~Px i^i Fin) /\ (/) = |^|w))
274	273	notbii 204	. . . . . . 7 |- (-. E.w e. (~Px i^i Fin)(/) = |^|w <-> -. E.w(w e. (~Px i^i Fin) /\ (/) = |^|w))
275		elin 2786	. . . . . . . . . . 11 |- (w e. (~Px i^i Fin) <-> (w e. ~Px /\ w e. Fin))
276	275	anbi1i 539	. . . . . . . . . 10 |- ((w e. (~Px i^i Fin) /\ (/) = |^|w) <-> ((w e. ~Px /\ w e. Fin) /\ (/) = |^|w))
277		df-3an 860	. . . . . . . . . 10 |- ((w e. ~Px /\ w e. Fin /\ (/) = |^|w) <-> ((w e. ~Px /\ w e. Fin) /\ (/) = |^|w))
278		visset 2295	. . . . . . . . . . . 12 |- w e. _V
279	278	elpw 3037	. . . . . . . . . . 11 |- (w e. ~Px <-> w C_ x)
280	279	3anbi1i 1058	. . . . . . . . . 10 |- ((w e. ~Px /\ w e. Fin /\ (/) = |^|w) <-> (w C_ x /\ w e. Fin /\ (/) = |^|w))
281	276, 277, 280	3bitr2i 196	. . . . . . . . 9 |- ((w e. (~Px i^i Fin) /\ (/) = |^|w) <-> (w C_ x /\ w e. Fin /\ (/) = |^|w))
282	281	exbii 1398	. . . . . . . 8 |- (E.w(w e. (~Px i^i Fin) /\ (/) = |^|w) <-> E.w(w C_ x /\ w e. Fin /\ (/) = |^|w))
283	282	notbii 204	. . . . . . 7 |- (-. E.w(w e. (~Px i^i Fin) /\ (/) = |^|w) <-> -. E.w(w C_ x /\ w e. Fin /\ (/) = |^|w))
284	272, 274, 283	3bitri 194	. . . . . 6 |- (A.w e. (~Px i^i Fin) -. (/) = |^|w <-> -. E.w(w C_ x /\ w e. Fin /\ (/) = |^|w))
285		df-nel 2020	. . . . . 6 |- ((/) e/ ( fi ` x) <-> -. (/) e. ( fi ` x))
286	271, 284, 285	3bitr4i 200	. . . . 5 |- (A.w e. (~Px i^i Fin) -. (/) = |^|w <-> (/) e/ ( fi ` x))
287		eqcom 1886	. . . . . 6 |- ((/) = |^|x <-> |^|x = (/))
288	287	necon3bbii 2031	. . . . 5 |- (-. (/) = |^|x <-> |^|x =/= (/))
289	286, 288	imbi12i 205	. . . 4 |- ((A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) <-> ((/) e/ ( fi ` x) -> |^|x =/= (/)))
290	289	ralbii 2127	. . 3 |- (A.x e. ~P (Clsd` J)(A.w e. (~Px i^i Fin) -. (/) = |^|w -> -. (/) = |^|x) <-> A.x e. ~P (Clsd` J)((/) e/ ( fi ` x) -> |^|x =/= (/)))
291	259, 262, 290	3bitr3g 613	. 2 |- (J e. Top -> (A.y e. ~P J(-. E.z e. (~Py i^i Fin)U.J = U.z -> -. U.J = U.y) <-> A.x e. ~P (Clsd` J)((/) e/ ( fi ` x) -> |^|x =/= (/))))
292	2, 5, 291	3bitrd 603	1 |- (J e. Top -> (J e. Comp <-> A.x e. ~P (Clsd` J)((/) e/ ( fi ` x) -> |^|x =/= (/))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017   e/ wnel 2018  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  <.cop 3046  U.cuni 3177  |^|cint 3214  U_ciun 3255  |^|_ciin 3256   class class class wbr 3338  {copab 3395  `'ccnv 3985  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   ~~ cen 5423  Fincfn 5426  Topctop 8857  Clsdccld 8936   fi cfi 10210  Compccomp 10328

This theorem is referenced by:  fcluscomp 15621

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-rab 2112  df-v 2294  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-1o 5177  df-er 5318  df-en 5427  df-fin 5430  df-cld 8939  df-fi 10211  df-comp 10329

Copyright terms: Public domain