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		0fin	$⊢ \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	syl5eq	$⊢ (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		simpr	$⊢ (((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 (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin)$
63		elfpw	$⊢ w \in (𝒫 (r \in J ⟼ ⋃ J ∖ r) [y] \cap Fin) \leftrightarrow (w \subseteq (r \in J ⟼ ⋃ J ∖ r) [y] \land w \in Fin)$
64	62 63	sylib	$⊢ (((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)$
65	64	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]$
66	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)$
67	65 66	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)$
68	64	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$
69		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$
70	61 67 68 69	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$
71		eqcom	$⊢ (r \in y ⟼ ⋃ J ∖ r) [z] = w \leftrightarrow w = (r \in y ⟼ ⋃ J ∖ r) [z]$
72	71	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]$
73	70 72	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]$
74		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]$
75	74	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]$
76	75	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])$
77	53 73 76	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])$
78		0ex	$⊢ \emptyset \in V$
79		imassrn	$⊢ (r \in J ⟼ ⋃ J ∖ r) [y] \subseteq ran (r \in J ⟼ ⋃ J ∖ r)$
80		eqid	$⊢ (r \in J ⟼ ⋃ J ∖ r) = (r \in J ⟼ ⋃ J ∖ r)$
81	54 80	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))$
82	81	simpld	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) : J \underset{1-1 onto}{⟶} Clsd (J)$
83		f1ofo	$⊢ (r \in J ⟼ ⋃ J ∖ r) : J \underset{1-1 onto}{⟶} Clsd (J) \to (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J)$
84	82 83	syl	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J)$
85		forn	$⊢ (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J) \to ran (r \in J ⟼ ⋃ J ∖ r) = Clsd (J)$
86	84 85	syl	$⊢ J \in Top \to ran (r \in J ⟼ ⋃ J ∖ r) = Clsd (J)$
87	79 86	sseqtrid	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) [y] \subseteq Clsd (J)$
88		fvex	$⊢ Clsd (J) \in V$
89	88	elpw2	$⊢ (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J) \leftrightarrow (r \in J ⟼ ⋃ J ∖ r) [y] \subseteq Clsd (J)$
90	87 89	sylibr	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J)$
91	90	ad2antrr	$⊢ ((J \in Top \land y \subseteq J) \land y \neq \emptyset) \to (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J)$
92		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)$
93	78 91 92	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)$
94		inundif	$⊢ ((𝒫 y \cap Fin) \cap \{\emptyset\}) \cup ((𝒫 y \cap Fin) ∖ \{\emptyset\}) = 𝒫 y \cap Fin$
95	94	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$
96		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)$
97	95 96	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)$
98		elinel2	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to z \in \{\emptyset\}$
99		elsni	$⊢ z \in \{\emptyset\} \to z = \emptyset$
100	98 99	syl	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to z = \emptyset$
101	100	unieqd	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to ⋃ z = ⋃ \emptyset$
102		uni0	$⊢ ⋃ \emptyset = \emptyset$
103	101 102	eqtrdi	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to ⋃ z = \emptyset$
104	103	eqeq2d	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to (⋃ J = ⋃ z \leftrightarrow ⋃ J = \emptyset)$
105	104	biimpd	$⊢ z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) \to (⋃ J = ⋃ z \to ⋃ J = \emptyset)$
106	105	rexlimiv	$⊢ \exists z \in ((𝒫 y \cap Fin) \cap \{\emptyset\}) ⋃ J = ⋃ z \to ⋃ J = \emptyset$
107		ssidd	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \subseteq y$
108		simprr	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ J = \emptyset$
109		0ss	$⊢ \emptyset \subseteq ⋃ y$
110	108 109	eqsstrdi	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ J \subseteq ⋃ y$
111	24	ad2antlr	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ y \subseteq ⋃ J$
112	110 111	eqssd	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ J = ⋃ y$
113	112 108	eqtr3d	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ y = \emptyset$
114	113 3	eqeltrdi	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to ⋃ y \in Fin$
115		pwfi	$⊢ ⋃ y \in Fin \leftrightarrow 𝒫 ⋃ y \in Fin$
116	114 115	sylib	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to 𝒫 ⋃ y \in Fin$
117		pwuni	$⊢ y \subseteq 𝒫 ⋃ y$
118		ssfi	$⊢ (𝒫 ⋃ y \in Fin \land y \subseteq 𝒫 ⋃ y) \to y \in Fin$
119	116 117 118	sylancl	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \in Fin$
120		elfpw	$⊢ y \in (𝒫 y \cap Fin) \leftrightarrow (y \subseteq y \land y \in Fin)$
121	107 119 120	sylanbrc	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \in (𝒫 y \cap Fin)$
122		simprl	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \neq \emptyset$
123		eldifsn	$⊢ y \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (y \in (𝒫 y \cap Fin) \land y \neq \emptyset)$
124	121 122 123	sylanbrc	$⊢ ((J \in Top \land y \subseteq J) \land (y \neq \emptyset \land ⋃ J = \emptyset)) \to y \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})$
125		unieq	$⊢ z = y \to ⋃ z = ⋃ y$
126	125	rspceeqv	$⊢ (y \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \land ⋃ J = ⋃ y) \to \exists z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) ⋃ J = ⋃ z$
127	124 112 126	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$
128	127	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)$
129	106 128	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)$
130		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)$
131	129 130	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)$
132		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)$
133	131 132	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)$
134	97 133	syl5bb	$⊢ ((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)$
135		eldifi	$⊢ z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \to z \in (𝒫 y \cap Fin)$
136	135	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)$
137		elfpw	$⊢ z \in (𝒫 y \cap Fin) \leftrightarrow (z \subseteq y \land z \in Fin)$
138	136 137	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)$
139	138	simpld	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to z \subseteq y$
140		simpllr	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to y \subseteq J$
141	139 140	sstrd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to z \subseteq J$
142	141	unissd	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to ⋃ z \subseteq ⋃ J$
143		eqss	$⊢ ⋃ z = ⋃ J \leftrightarrow (⋃ z \subseteq ⋃ J \land ⋃ J \subseteq ⋃ z)$
144	143	baib	$⊢ ⋃ z \subseteq ⋃ J \to (⋃ z = ⋃ J \leftrightarrow ⋃ J \subseteq ⋃ z)$
145	142 144	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)$
146		eqcom	$⊢ ⋃ z = ⋃ J \leftrightarrow ⋃ J = ⋃ z$
147		ssdif0	$⊢ ⋃ J \subseteq ⋃ z \leftrightarrow ⋃ J ∖ ⋃ z = \emptyset$
148		eqcom	$⊢ ⋃ J ∖ ⋃ z = \emptyset \leftrightarrow \emptyset = ⋃ J ∖ ⋃ z$
149	147 148	bitri	$⊢ ⋃ J \subseteq ⋃ z \leftrightarrow \emptyset = ⋃ J ∖ ⋃ z$
150	145 146 149	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)$
151		df-ima	$⊢ (r \in y ⟼ ⋃ J ∖ r) [z] = ran ({(r \in y ⟼ ⋃ J ∖ r) ↾}_{z})$
152	139	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)$
153	152	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)$
154	151 153	syl5eq	$⊢ (((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	154	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)$
156	56	ralrimivw	$⊢ J \in Top \to \forall r \in z ⋃ J ∖ r \in V$
157	156	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$
158		dfiin3g	$⊢ \forall r \in z ⋃ J ∖ r \in V \to ⋂_{r \in z} (⋃ J ∖ r) = ⋂ ran (r \in z ⟼ ⋃ J ∖ r)$
159	157 158	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)$
160		eldifsni	$⊢ z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \to z \neq \emptyset$
161	160	adantl	$⊢ (((J \in Top \land y \subseteq J) \land y \neq \emptyset) \land z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\})) \to z \neq \emptyset$
162		iindif2	$⊢ z \neq \emptyset \to ⋂_{r \in z} (⋃ J ∖ r) = ⋃ J ∖ ⋃_{r \in z} r$
163	161 162	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$
164	155 159 163	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$
165		uniiun	$⊢ ⋃ z = ⋃_{r \in z} r$
166	165	difeq2i	$⊢ ⋃ J ∖ ⋃ z = ⋃ J ∖ ⋃_{r \in z} r$
167	164 166	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$
168	167	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)$
169	150 168	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])$
170	169	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])$
171	134 170	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])$
172		imaeq2	$⊢ z = \emptyset \to (r \in y ⟼ ⋃ J ∖ r) [z] = (r \in y ⟼ ⋃ J ∖ r) [\emptyset]$
173		ima0	$⊢ (r \in y ⟼ ⋃ J ∖ r) [\emptyset] = \emptyset$
174	172 173	eqtrdi	$⊢ z = \emptyset \to (r \in y ⟼ ⋃ J ∖ r) [z] = \emptyset$
175	174	inteqd	$⊢ z = \emptyset \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] = ⋂ \emptyset$
176		int0	$⊢ ⋂ \emptyset = V$
177	175 176	eqtrdi	$⊢ z = \emptyset \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] = V$
178	177	neeq1d	$⊢ z = \emptyset \to (⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \neq \emptyset \leftrightarrow V \neq \emptyset)$
179	14 178	mpbiri	$⊢ z = \emptyset \to ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \neq \emptyset$
180	179	necomd	$⊢ z = \emptyset \to \emptyset \neq ⋂ (r \in y ⟼ ⋃ J ∖ r) [z]$
181	180	necon2i	$⊢ \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \to z \neq \emptyset$
182		eldifsn	$⊢ z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}) \leftrightarrow (z \in (𝒫 y \cap Fin) \land z \neq \emptyset)$
183	182	rbaibr	$⊢ z \neq \emptyset \to (z \in (𝒫 y \cap Fin) \leftrightarrow z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}))$
184	181 183	syl	$⊢ \emptyset = ⋂ (r \in y ⟼ ⋃ J ∖ r) [z] \to (z \in (𝒫 y \cap Fin) \leftrightarrow z \in ((𝒫 y \cap Fin) ∖ \{\emptyset\}))$
185	184	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])$
186	185	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]$
187	171 186	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])$
188	77 93 187	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]))$
189	38 188	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])))$
190	23 189	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])))$
191	57	adantr	$⊢ (J \in Top \land y \subseteq J) \to \forall r \in y ⋃ J ∖ r \in V$
192		dfiin3g	$⊢ \forall r \in y ⋃ J ∖ r \in V \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂ ran (r \in y ⟼ ⋃ J ∖ r)$
193	191 192	syl	$⊢ (J \in Top \land y \subseteq J) \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂ ran (r \in y ⟼ ⋃ J ∖ r)$
194	44	inteqd	$⊢ (J \in Top \land y \subseteq J) \to ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] = ⋂ ran (r \in y ⟼ ⋃ J ∖ r)$
195	193 194	eqtr4d	$⊢ (J \in Top \land y \subseteq J) \to ⋂_{r \in y} (⋃ J ∖ r) = ⋂ (r \in J ⟼ ⋃ J ∖ r) [y]$
196	195	eqeq1d	$⊢ (J \in Top \land y \subseteq J) \to (⋂_{r \in y} (⋃ J ∖ r) = \emptyset \leftrightarrow ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] = \emptyset)$
197		nne	$⊢ \neg ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] \neq \emptyset \leftrightarrow ⋂ (r \in J ⟼ ⋃ J ∖ r) [y] = \emptyset$
198	196 197	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)$
199	198	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])))$
200	190 199	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])))$
201		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)$
202	200 201	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))$
203	1 202	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))$
204	203	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))$
205	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))$
206	205	baib	$⊢ J \in Top \to (J \in Comp \leftrightarrow \forall y \in 𝒫 J (⋃ J = ⋃ y \to \exists z \in (𝒫 y \cap Fin) ⋃ J = ⋃ z))$
207	90	adantr	$⊢ (J \in Top \land y \in 𝒫 J) \to (r \in J ⟼ ⋃ J ∖ r) [y] \in 𝒫 Clsd (J)$
208		simpl	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to J \in Top$
209		funmpt	$⊢ Fun (r \in J ⟼ ⋃ J ∖ r)$
210	209	a1i	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to Fun (r \in J ⟼ ⋃ J ∖ r)$
211		elpwi	$⊢ x \in 𝒫 Clsd (J) \to x \subseteq Clsd (J)$
212		foima	$⊢ (r \in J ⟼ ⋃ J ∖ r) : J \underset{onto}{⟶} Clsd (J) \to (r \in J ⟼ ⋃ J ∖ r) [J] = Clsd (J)$
213	84 212	syl	$⊢ J \in Top \to (r \in J ⟼ ⋃ J ∖ r) [J] = Clsd (J)$
214	213	sseq2d	$⊢ J \in Top \to (x \subseteq (r \in J ⟼ ⋃ J ∖ r) [J] \leftrightarrow x \subseteq Clsd (J))$
215	211 214	syl5ibr	$⊢ J \in Top \to (x \in 𝒫 Clsd (J) \to x \subseteq (r \in J ⟼ ⋃ J ∖ r) [J])$
216	215	imp	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to x \subseteq (r \in J ⟼ ⋃ J ∖ r) [J]$
217		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])$
218	208 210 216 217	syl3anc	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to \exists y (y \subseteq J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
219		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])$
220		velpw	$⊢ y \in 𝒫 J \leftrightarrow y \subseteq J$
221	220	anbi1i	$⊢ (y \in 𝒫 J \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \leftrightarrow (y \subseteq J \land x = (r \in J ⟼ ⋃ J ∖ r) [y])$
222	221	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])$
223	219 222	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])$
224	218 223	sylibr	$⊢ (J \in Top \land x \in 𝒫 Clsd (J)) \to \exists y \in 𝒫 J x = (r \in J ⟼ ⋃ J ∖ r) [y]$
225		simpr	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to x = (r \in J ⟼ ⋃ J ∖ r) [y]$
226	225	fveq2d	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to fi (x) = fi ((r \in J ⟼ ⋃ J ∖ r) [y])$
227	226	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]))$
228	227	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]))$
229	225	inteqd	$⊢ (J \in Top \land x = (r \in J ⟼ ⋃ J ∖ r) [y]) \to ⋂ x = ⋂ (r \in J ⟼ ⋃ J ∖ r) [y]$
230	229	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)$
231	228 230	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))$
232	207 224 231	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))$
233	204 206 232	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