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