cmpfi

Description: If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009) (Proof shortened by Mario Carneiro, 1-Sep-2015)

		Ref	Expression
	Assertion	cmpfi	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		elpwi	$⊢ y \in 𝒫 J \to y \subseteq J$
2		0ss	$⊢ \emptyset \subseteq y$
3		0fi	$⊢ \emptyset \in Fin$
4		elfpw	$⊢ \emptyset \in (𝒫 y \cap Fin) \leftrightarrow (\emptyset \subseteq y \land \emptyset \in Fin)$
5	2 3 4	mpbir2an	$⊢ \emptyset \in (𝒫 y \cap Fin)$
6		simprr	$⊢ ((J \in Top \land y \subseteq J) \land (y = \emptyset \land ⋃ J = ⋃ y)) \to ⋃ J = ⋃ y$
7		simprl	$⊢ ((J \in Top \land y \subseteq J) \land (y = \emptyset \land ⋃ J = ⋃ y)) \to y = \emptyset$
8	7	unieqd	$⊢ ((J \in Top \land y \subseteq J) \land (y = \emptyset \land ⋃ J = ⋃ y)) \to ⋃ y = ⋃ \emptyset$
9	6 8	eqtrd	$⊢ ((J \in Top \land y \subseteq J) \land (y = \emptyset \land ⋃ J = ⋃ y)) \to ⋃ J = ⋃ \emptyset$
10		unieq	$⊢ z = \emptyset \to ⋃ z = ⋃ \emptyset$
11	10	rspceeqv	$⊢ (\emptyset \in (𝒫 y \cap Fin) \land ⋃ J = ⋃ \emptyset) \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z$
12	5 9 11	sylancr	$⊢ ((J \in Top \land y \subseteq J) \land (y = \emptyset \land ⋃ J = ⋃ y)) \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z$
13	12	expr	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z)$
14		vn0	$⊢ V \neq \emptyset$
15		iineq1	$⊢ y = \emptyset \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂_{r \in \emptyset} (⋃ J ∖ r)$
16	15	adantl	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂_{r \in \emptyset} (⋃ J ∖ r)$
17		0iin	$⊢ ⋂_{r \in \emptyset} (⋃ J ∖ r) = V$
18	16 17	eqtrdi	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to ⋂_{r \in y} (⋃ J ∖ r) = V$
19	18	eqeq1d	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \leftrightarrow V = \emptyset)$
20	19	necon3bbid	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to (\neg ⋂_{r \in y} (⋃ J ∖ r) = \emptyset \leftrightarrow V \neq \emptyset)$
21	14 20	mpbiri	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to \neg ⋂_{r \in y} (⋃ J ∖ r) = \emptyset$
22	21	pm2.21d	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]))$
23	13 22	2thd	$⊢ ((J \in Top \land y \subseteq J) \land y = \emptyset) \to ((⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z) \leftrightarrow (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y])))$
24		uniss	$⊢ y \subseteq J \to ⋃ y \subseteq ⋃ J$
25	24	ad2antlr	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to ⋃ y \subseteq ⋃ J$
26		eqss	$⊢ ⋃ y = ⋃ J \leftrightarrow (⋃ y \subseteq ⋃ J \land ⋃ J \subseteq ⋃ y)$
27	26	baib	$⊢ ⋃ y \subseteq ⋃ J \to (⋃ y = ⋃ J \leftrightarrow ⋃ J \subseteq ⋃ y)$
28	25 27	syl	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (⋃ y = ⋃ J \leftrightarrow ⋃ J \subseteq ⋃ y)$
29		eqcom	$⊢ ⋃ y = ⋃ J \leftrightarrow ⋃ J = ⋃ y$
30		ssdif0	$⊢ ⋃ J \subseteq ⋃ y \leftrightarrow ⋃ J ∖ ⋃ y = \emptyset$
31	28 29 30	3bitr3g	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (⋃ J = ⋃ y \leftrightarrow ⋃ J ∖ ⋃ y = \emptyset)$
32		iindif2	$⊢ y \neq \emptyset \to ⋂_{r \in y} (⋃ J ∖ r) = ⋃ J ∖ ⋃_{r \in y} r$
33	32	adantl	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to ⋂_{r \in y} (⋃ J ∖ r) = ⋃ J ∖ ⋃_{r \in y} r$
34		uniiun	$⊢ ⋃ y = ⋃_{r \in y} r$
35	34	difeq2i	$⊢ ⋃ J ∖ ⋃ y = ⋃ J ∖ ⋃_{r \in y} r$
36	33 35	eqtr4di	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to ⋂_{r \in y} (⋃ J ∖ r) = ⋃ J ∖ ⋃ y$
37	36	eqeq1d	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \leftrightarrow ⋃ J ∖ ⋃ y = \emptyset)$
38	31 37	bitr4d	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (⋃ J = ⋃ y \leftrightarrow ⋂_{r \in y} (⋃ J ∖ r) = \emptyset)$
39		imassrn	$⊢ (r \in y ⟼ ⋃ J ∖ r) [z] \subseteq ran (r \in y ⟼ ⋃ J ∖ r)$
40		df-ima	$⊢ (r \in J ⟼ ⋃ J ∖ r) [y] = ran ({(r \in J ⟼ ⋃ J ∖ r) ↾}_{y})$
41		resmpt	$⊢ y \subseteq J \to {(r \in J ⟼ ⋃ J ∖ r) ↾}_{y} = (r \in y ⟼ ⋃ J ∖ r)$
42	41	adantl	$⊢ (J \in Top \land y \subseteq J) \to {(r \in J ⟼ ⋃ J ∖ r) ↾}_{y} = (r \in y ⟼ ⋃ J ∖ r)$
43	42	rneqd	$⊢ (J \in Top \land y \subseteq J) \to ran ({(r \in J ⟼ ⋃ J ∖ r) ↾}_{y}) = ran (r \in y ⟼ ⋃ J ∖ r)$
44	40 43	eqtrid	$⊢ (J \in Top \land y \subseteq J) \to (r \in J ⟼ ⋃ J ∖ r) [y] = ran (r \in y ⟼ ⋃ J ∖ r)$
45	44	ad2antrr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in (𝒫 y \cap Fin)) \to (r \in J ⟼ ⋃ J ∖ r) [y] = ran (r \in y ⟼ ⋃ J ∖ r)$
46	39 45	sseqtrrid	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in (𝒫 y \cap Fin)) \to (r \in y ⟼ ⋃ J ∖ r) [z] \subseteq (r \in J ⟼ ⋃ J ∖ r) [y]$
47		funmpt	$⊢ Fun (r \in y ⟼ ⋃ J ∖ r)$
48		elinel2	$⊢ z \in (𝒫 y \cap Fin) \to z \in Fin$
49	48	adantl	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in (𝒫 y \cap Fin)) \to z \in Fin$
50		imafi	$⊢ (Fun (r \in y ⟼ ⋃ J ∖ r) \land z \in Fin) \to (r \in y ⟼ ⋃ J ∖ r) [z] \in Fin$
51	47 49 50	sylancr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in (𝒫 y \cap Fin)) \to (r \in y ⟼ ⋃ J ∖ r) [z] \in Fin$
52		elfpw	$⊢ (r \in y ⟼ ⋃ J ∖ r) [z] \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin) \leftrightarrow ((r \in y ⟼ ⋃ J ∖ r) [z] \subseteq (r \in J ⟼ ⋃ J ∖ r) [y] \land (r \in y ⟼ ⋃ J ∖ r) [z] \in Fin)$
53	46 51 52	sylanbrc	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in (𝒫 y \cap Fin)) \to (r \in y ⟼ ⋃ J ∖ r) [z] \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)$
54		eqid	$⊢ ⋃ J = ⋃ J$
55	54	topopn	$⊢ J \in Top \to ⋃ J \in J$
56	55	difexd	$⊢ J \in Top \to ⋃ J ∖ r \in V$
57	56	ralrimivw	$⊢ J \in Top \to \forall r \in y ⋃ J ∖ r \in V$
58		eqid	$⊢ (r \in y ⟼ ⋃ J ∖ r) = (r \in y ⟼ ⋃ J ∖ r)$
59	58	fnmpt	$⊢ \forall r \in y ⋃ J ∖ r \in V \to (r \in y ⟼ ⋃ J ∖ r) Fn y$
60	57 59	syl	$⊢ J \in Top \to (r \in y ⟼ ⋃ J ∖ r) Fn y$
61	60	ad3antrrr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to (r \in y ⟼ ⋃ J ∖ r) Fn y$
62		elfpw	$⊢ w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin) \leftrightarrow (w \subseteq (r \in J ⟼ ⋃ J ∖ r) [y] \land w \in Fin)$
63	62	bilani	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to (w \subseteq (r \in J ⟼ ⋃ J ∖ r) [y] \land w \in Fin)$
64	63	simpld	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to w \subseteq (r \in J ⟼ ⋃ J ∖ r) [y]$
65	44	ad2antrr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to (r \in J ⟼ ⋃ J ∖ r) [y] = ran (r \in y ⟼ ⋃ J ∖ r)$
66	64 65	sseqtrd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to w \subseteq ran (r \in y ⟼ ⋃ J ∖ r)$
67	63	simprd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to w \in Fin$
68		fipreima	$⊢ ((r \in y ⟼ ⋃ J ∖ r) Fn y \land w \subseteq ran (r \in y ⟼ ⋃ J ∖ r) \land w \in Fin) \to \exists z \in (𝒫 y \cap Fin) (r \in y ⟼ ⋃ J ∖ r) [z] = w$
69	61 66 67 68	syl3anc	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to \exists z \in (𝒫 y \cap Fin) (r \in y ⟼ ⋃ J ∖ r) [z] = w$
70		eqcom	$⊢ (r \in y ⟼ ⋃ J ∖ r) [z] = w \leftrightarrow w = (r \in y ⟼ ⋃ J ∖ r) [z]$
71	70	rexbii	$⊢ \exists z \in (𝒫 y \cap Fin) (r \in y ⟼ ⋃ J ∖ r) [z] = w \leftrightarrow \exists z \in (𝒫 y \cap Fin) w = (r \in y ⟼ ⋃ J ∖ r) [z]$
72	69 71	sylib	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)) \to \exists z \in (𝒫 y \cap Fin) w = (r \in y ⟼ ⋃ J ∖ r) [z]$
73		simpr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w = (r \in y ⟼ ⋃ J ∖ r) [z]) \to w = (r \in y ⟼ ⋃ J ∖ r) [z]$
74	73	inteqd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w = (r \in y ⟼ ⋃ J ∖ r) [z]) \to ⋂ w = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z]$
75	74	eqeq2d	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land w = (r \in y ⟼ ⋃ J ∖ r) [z]) \to (\emptyset = ⋂ w \leftrightarrow \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z])$
76	53 72 75	rexxfrd	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin) \emptyset = ⋂ w \leftrightarrow \exists z \in (𝒫 y \cap Fin) \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z])$
77		0ex	$⊢ \emptyset \in V$
78		imassrn	$⊢ (r \in J ⟼ ⋃ J ∖ r) [y] \subseteq ran (r \in J ⟼ ⋃ J ∖ r)$
79		eqid	$⊢ (r \in J ⟼ ⋃ J ∖ r) = (r \in J ⟼ ⋃ J ∖ r)$
80	54 79	opncldf1	$⊢ J \in Top \to ((r \in J ⟼ ⋃ J ∖ r) : J \underset{1-1 onto}{⟶} Clsd (J) \land {(r \in J ⟼ ⋃ J ∖ r)}^{-1} = (v \in Clsd (J) ⟼ ⋃ J ∖ v))$
81	80	simpld	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) : J \underset{1-1 onto}{⟶} Clsd (J)$
82		f1ofo	$⊢ (r \in J ⟼ ⋃ J ∖ r) : J \underset{1-1 onto}{⟶} Clsd (J) \to (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J)$
83	81 82	syl	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J)$
84		forn	$⊢ (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J) \to ran (r \in J ⟼ ⋃ J ∖ r) = Clsd (J)$
85	83 84	syl	$⊢ J \in Top \to ran (r \in J ⟼ ⋃ J ∖ r) = Clsd (J)$
86	78 85	sseqtrid	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) [y] \subseteq Clsd (J)$
87		fvex	$⊢ Clsd (J) \in V$
88	87	elpw2	$⊢ (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J) \leftrightarrow (r \in J ⟼ ⋃ J ∖ r) [y] \subseteq Clsd (J)$
89	86 88	sylibr	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J)$
90	89	ad2antrr	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J)$
91		elfi	$⊢ (\emptyset \in V \land (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J)) \to (\emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \leftrightarrow \exists w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin) \emptyset = ⋂ w)$
92	77 90 91	sylancr	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \leftrightarrow \exists w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin) \emptyset = ⋂ w)$
93		inundif	$⊢ ((𝒫 y \cap Fin) \cap \{\emptyset\}) \cup ((𝒫 y \cap Fin) ∖ \{\emptyset\}) = 𝒫 y \cap Fin$
94	93	rexeqi	$⊢ \exists z \in (((𝒫 y \cap Fin) \cap \{\emptyset\}) \cup ((𝒫 y \cap Fin) ∖ \{\emptyset\})) ⋃ J = ⋃ z \leftrightarrow \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z$
95		rexun	$⊢ \exists z \in (((𝒫 y \cap Fin) \cap \{\emptyset\}) \cup ((𝒫 y \cap Fin) ∖ \{\emptyset\})) ⋃ J = ⋃ z \leftrightarrow (\exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \lor \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
96	94 95	bitr3i	$⊢ \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z \leftrightarrow (\exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \lor \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
97		elinel2	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to z \in \{\emptyset\}$
98		elsni	$⊢ z \in \{\emptyset\} \to z = \emptyset$
99	97 98	syl	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to z = \emptyset$
100	99	unieqd	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to ⋃ z = ⋃ \emptyset$
101		uni0	$⊢ ⋃ \emptyset = \emptyset$
102	100 101	eqtrdi	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to ⋃ z = \emptyset$
103	102	eqeq2d	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to (⋃ J = ⋃ z \leftrightarrow ⋃ J = \emptyset)$
104	103	biimpd	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to (⋃ J = ⋃ z \to ⋃ J = \emptyset)$
105	104	rexlimiv	$⊢ \exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \to ⋃ J = \emptyset$
106		ssidd	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \subseteq y$
107		simprr	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ J = \emptyset$
108		0ss	$⊢ \emptyset \subseteq ⋃ y$
109	107 108	eqsstrdi	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ J \subseteq ⋃ y$
110	24	ad2antlr	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ y \subseteq ⋃ J$
111	109 110	eqssd	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ J = ⋃ y$
112	111 107	eqtr3d	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ y = \emptyset$
113	112 3	eqeltrdi	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ y \in Fin$
114		pwfi	$⊢ ⋃ y \in Fin \leftrightarrow 𝒫 ⋃ y \in Fin$
115	113 114	sylib	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to 𝒫 ⋃ y \in Fin$
116		pwuni	$⊢ y \subseteq 𝒫 ⋃ y$
117		ssfi	$⊢ (𝒫 ⋃ y \in Fin \land y \subseteq 𝒫 ⋃ y) \to y \in Fin$
118	115 116 117	sylancl	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \in Fin$
119		elfpw	$⊢ y \in (𝒫 y \cap Fin) \leftrightarrow (y \subseteq y \land y \in Fin)$
120	106 118 119	sylanbrc	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \in (𝒫 y \cap Fin)$
121		simprl	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \neq \emptyset$
122		eldifsn	$⊢ y \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (y \in (𝒫 y \cap Fin) \land y \neq \emptyset)$
123	120 121 122	sylanbrc	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})$
124		unieq	$⊢ z = y \to ⋃ z = ⋃ y$
125	124	rspceeqv	$⊢ (y \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \land ⋃ J = ⋃ y) \to \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z$
126	123 111 125	syl2anc	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z$
127	126	expr	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (⋃ J = \emptyset \to \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
128	105 127	syl5	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \to \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
129		idd	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z \to \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
130	128 129	jaod	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to ((\exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \lor \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z) \to \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
131		olc	$⊢ \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z \to (\exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \lor \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
132	130 131	impbid1	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to ((\exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \lor \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z) \leftrightarrow \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
133	96 132	bitrid	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z \leftrightarrow \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z)$
134		eldifi	$⊢ z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \to z \in (𝒫 y \cap Fin)$
135	134	adantl	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to z \in (𝒫 y \cap Fin)$
136		elfpw	$⊢ z \in (𝒫 y \cap Fin) \leftrightarrow (z \subseteq y \land z \in Fin)$
137	135 136	sylib	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to (z \subseteq y \land z \in Fin)$
138	137	simpld	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to z \subseteq y$
139		simpllr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to y \subseteq J$
140	138 139	sstrd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to z \subseteq J$
141	140	unissd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ⋃ z \subseteq ⋃ J$
142		eqss	$⊢ ⋃ z = ⋃ J \leftrightarrow (⋃ z \subseteq ⋃ J \land ⋃ J \subseteq ⋃ z)$
143	142	baib	$⊢ ⋃ z \subseteq ⋃ J \to (⋃ z = ⋃ J \leftrightarrow ⋃ J \subseteq ⋃ z)$
144	141 143	syl	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to (⋃ z = ⋃ J \leftrightarrow ⋃ J \subseteq ⋃ z)$
145		eqcom	$⊢ ⋃ z = ⋃ J \leftrightarrow ⋃ J = ⋃ z$
146		ssdif0	$⊢ ⋃ J \subseteq ⋃ z \leftrightarrow ⋃ J ∖ ⋃ z = \emptyset$
147		eqcom	$⊢ ⋃ J ∖ ⋃ z = \emptyset \leftrightarrow \emptyset = ⋃ J ∖ ⋃ z$
148	146 147	bitri	$⊢ ⋃ J \subseteq ⋃ z \leftrightarrow \emptyset = ⋃ J ∖ ⋃ z$
149	144 145 148	3bitr3g	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to (⋃ J = ⋃ z \leftrightarrow \emptyset = ⋃ J ∖ ⋃ z)$
150		df-ima	$⊢ (r \in y ⟼ ⋃ J ∖ r) [z] = ran ({(r \in y ⟼ ⋃ J ∖ r) ↾}_{z})$
151	138	resmptd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to {(r \in y ⟼ ⋃ J ∖ r) ↾}_{z} = (r \in z ⟼ ⋃ J ∖ r)$
152	151	rneqd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ran ({(r \in y ⟼ ⋃ J ∖ r) ↾}_{z}) = ran (r \in z ⟼ ⋃ J ∖ r)$
153	150 152	eqtrid	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to (r \in y ⟼ ⋃ J ∖ r) [z] = ran (r \in z ⟼ ⋃ J ∖ r)$
154	153	inteqd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] = ⋂ ran (r \in z ⟼ ⋃ J ∖ r)$
155	56	ralrimivw	$⊢ J \in Top \to \forall r \in z ⋃ J ∖ r \in V$
156	155	ad3antrrr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to \forall r \in z ⋃ J ∖ r \in V$
157		dfiin3g	$⊢ \forall r \in z ⋃ J ∖ r \in V \to ⋂_{r \in z} (⋃ J ∖ r) = ⋂ ran (r \in z ⟼ ⋃ J ∖ r)$
158	156 157	syl	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ⋂_{r \in z} (⋃ J ∖ r) = ⋂ ran (r \in z ⟼ ⋃ J ∖ r)$
159		eldifsni	$⊢ z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \to z \neq \emptyset$
160	159	adantl	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to z \neq \emptyset$
161		iindif2	$⊢ z \neq \emptyset \to ⋂_{r \in z} (⋃ J ∖ r) = ⋃ J ∖ ⋃_{r \in z} r$
162	160 161	syl	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ⋂_{r \in z} (⋃ J ∖ r) = ⋃ J ∖ ⋃_{r \in z} r$
163	154 158 162	3eqtr2d	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] = ⋃ J ∖ ⋃_{r \in z} r$
164		uniiun	$⊢ ⋃ z = ⋃_{r \in z} r$
165	164	difeq2i	$⊢ ⋃ J ∖ ⋃ z = ⋃ J ∖ ⋃_{r \in z} r$
166	163 165	eqtr4di	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] = ⋃ J ∖ ⋃ z$
167	166	eqeq2d	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to (\emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \leftrightarrow \emptyset = ⋃ J ∖ ⋃ z)$
168	149 167	bitr4d	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to (⋃ J = ⋃ z \leftrightarrow \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z])$
169	168	rexbidva	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z \leftrightarrow \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z])$
170	133 169	bitrd	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z \leftrightarrow \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z])$
171		imaeq2	$⊢ z = \emptyset \to (r \in y ⟼ ⋃ J ∖ r) [z] = (r \in y ⟼ ⋃ J ∖ r) [\emptyset]$
172		ima0	$⊢ (r \in y ⟼ ⋃ J ∖ r) [\emptyset] = \emptyset$
173	171 172	eqtrdi	$⊢ z = \emptyset \to (r \in y ⟼ ⋃ J ∖ r) [z] = \emptyset$
174	173	inteqd	$⊢ z = \emptyset \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] = ⋂ \emptyset$
175		int0	$⊢ ⋂ \emptyset = V$
176	174 175	eqtrdi	$⊢ z = \emptyset \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] = V$
177	176	neeq1d	$⊢ z = \emptyset \to (⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \neq \emptyset \leftrightarrow V \neq \emptyset)$
178	14 177	mpbiri	$⊢ z = \emptyset \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \neq \emptyset$
179	178	necomd	$⊢ z = \emptyset \to \emptyset \neq ⋂ (r \in y ⟼ ⋃ J ∖ r) [z]$
180	179	necon2i	$⊢ \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \to z \neq \emptyset$
181		eldifsn	$⊢ z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (z \in (𝒫 y \cap Fin) \land z \neq \emptyset)$
182	181	rbaibr	$⊢ z \neq \emptyset \to (z \in (𝒫 y \cap Fin) \leftrightarrow z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}))$
183	180 182	syl	$⊢ \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \to (z \in (𝒫 y \cap Fin) \leftrightarrow z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}))$
184	183	pm5.32ri	$⊢ (z \in (𝒫 y \cap Fin) \land \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z]) \leftrightarrow (z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \land \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z])$
185	184	rexbii2	$⊢ \exists z \in (𝒫 y \cap Fin) \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \leftrightarrow \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z]$
186	170 185	bitr4di	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z \leftrightarrow \exists z \in (𝒫 y \cap Fin) \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z])$
187	76 92 186	3bitr4rd	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (\exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z \leftrightarrow \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]))$
188	38 187	imbi12d	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to ((⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z) \leftrightarrow (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y])))$
189	23 188	pm2.61dane	$⊢ (J \in Top \land y \subseteq J) \to ((⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z) \leftrightarrow (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y])))$
190	57	adantr	$⊢ (J \in Top \land y \subseteq J) \to \forall r \in y ⋃ J ∖ r \in V$
191		dfiin3g	$⊢ \forall r \in y ⋃ J ∖ r \in V \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂ ran (r \in y ⟼ ⋃ J ∖ r)$
192	190 191	syl	$⊢ (J \in Top \land y \subseteq J) \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂ ran (r \in y ⟼ ⋃ J ∖ r)$
193	44	inteqd	$⊢ (J \in Top \land y \subseteq J) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] = ⋂ ran (r \in y ⟼ ⋃ J ∖ r)$
194	192 193	eqtr4d	$⊢ (J \in Top \land y \subseteq J) \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂ (r \in J ⟼ ⋃ J ∖ r) [y]$
195	194	eqeq1d	$⊢ (J \in Top \land y \subseteq J) \to (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \leftrightarrow ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] = \emptyset)$
196		nne	$⊢ \neg ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset \leftrightarrow ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] = \emptyset$
197	195 196	bitr4di	$⊢ (J \in Top \land y \subseteq J) \to (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \leftrightarrow \neg ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset)$
198	197	imbi1d	$⊢ (J \in Top \land y \subseteq J) \to ((⋂_{r \in y} (⋃ J ∖ r) = \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y])) \leftrightarrow (\neg ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y])))$
199	189 198	bitrd	$⊢ (J \in Top \land y \subseteq J) \to ((⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z) \leftrightarrow (\neg ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y])))$
200		con1b	$⊢ (\neg ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset \to \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y])) \leftrightarrow (\neg \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset)$
201	199 200	bitrdi	$⊢ (J \in Top \land y \subseteq J) \to ((⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z) \leftrightarrow (\neg \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset))$
202	1 201	sylan2	$⊢ (J \in Top \land y \in 𝒫 J) \to ((⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z) \leftrightarrow (\neg \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset))$
203	202	ralbidva	$⊢ J \in Top \to (\forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z) \leftrightarrow \forall y \in 𝒫 J (\neg \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset))$
204	54	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z))$
205	204	baib	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z))$
206	89	adantr	$⊢ (J \in Top \land y \in 𝒫 J) \to (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J)$
207		simpl	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to J \in Top$
208		funmpt	$⊢ Fun (r \in J ⟼ ⋃ J ∖ r)$
209	208	a1i	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to Fun (r \in J ⟼ ⋃ J ∖ r)$
210		elpwi	$⊢ x \in 𝒫 Clsd (J) \to x \subseteq Clsd (J)$
211		foima	$⊢ (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J) \to (r \in J ⟼ ⋃ J ∖ r) [J] = Clsd (J)$
212	83 211	syl	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) [J] = Clsd (J)$
213	212	sseq2d	$⊢ J \in Top \to (x \subseteq (r \in J ⟼ ⋃ J ∖ r) [J] \leftrightarrow x \subseteq Clsd (J))$
214	210 213	imbitrrid	$⊢ J \in Top \to (x \in 𝒫 Clsd (J) \to x \subseteq (r \in J ⟼ ⋃ J ∖ r) [J])$
215	214	imp	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to x \subseteq (r \in J ⟼ ⋃ J ∖ r) [J]$
216		ssimaexg	$⊢ (J \in Top \land Fun (r \in J ⟼ ⋃ J ∖ r) \land x \subseteq (r \in J ⟼ ⋃ J ∖ r) [J]) \to \exists y (y \subseteq J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
217	207 209 215 216	syl3anc	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to \exists y (y \subseteq J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
218		df-rex	$⊢ \exists y \in 𝒫 J x = (r \in J ⟼ ⋃ J ∖ r) [y] \leftrightarrow \exists y (y \in 𝒫 J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
219		velpw	$⊢ y \in 𝒫 J \leftrightarrow y \subseteq J$
220	219	anbi1i	$⊢ (y \in 𝒫 J \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \leftrightarrow (y \subseteq J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
221	220	exbii	$⊢ \exists y (y \in 𝒫 J \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \leftrightarrow \exists y (y \subseteq J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
222	218 221	bitri	$⊢ \exists y \in 𝒫 J x = (r \in J ⟼ ⋃ J ∖ r) [y] \leftrightarrow \exists y (y \subseteq J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
223	217 222	sylibr	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to \exists y \in 𝒫 J x = (r \in J ⟼ ⋃ J ∖ r) [y]$
224		simpr	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to x = (r \in J ⟼ ⋃ J ∖ r) [y]$
225	224	fveq2d	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to fi (x) = fi ((r \in J ⟼ ⋃ J ∖ r) [y])$
226	225	eleq2d	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to (\emptyset \in fi (x) \leftrightarrow \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]))$
227	226	notbid	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to (\neg \emptyset \in fi (x) \leftrightarrow \neg \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]))$
228	224	inteqd	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ x = ⋂ (r \in J ⟼ ⋃ J ∖ r) [y]$
229	228	neeq1d	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to (⋂ x \neq \emptyset \leftrightarrow ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset)$
230	227 229	imbi12d	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to ((\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset) \leftrightarrow (\neg \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset))$
231	206 223 230	ralxfrd	$⊢ J \in Top \to (\forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset) \leftrightarrow \forall y \in 𝒫 J (\neg \emptyset \in fi ((r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset))$
232	203 205 231	3bitr4d	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall x \in 𝒫 Clsd (J) (\neg \emptyset \in fi (x) \to ⋂ x \neq \emptyset))$

Metamath Proof Explorer

Theorem cmpfi

Proof