pibt2

Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 and pibp21 for the definitions of the relevant properties. This proof uses the axiom of choice. (Contributed by ML, 30-Mar-2021)

	Ref	Expression
Hypotheses	pibt2.x	$⊢ X = ⋃ J$
	pibt2.19	$⊢ C = \{x \in Top \| \forall y \in 𝒫 x ((⋃ x = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) ⋃ x = ⋃ z)\}$
	pibt2.21	$⊢ W = \{x \in Top \| \forall y \in (𝒫 ⋃ x ∖ Fin) \exists z \in ⋃ x z \in limPt (x) (y)\}$
Assertion	pibt2	$⊢ J \in C \to J \in W$

Proof

Step	Hyp	Ref	Expression
1		pibt2.x	$⊢ X = ⋃ J$
2		pibt2.19	$⊢ C = \{x \in Top \| \forall y \in 𝒫 x ((⋃ x = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) ⋃ x = ⋃ z)\}$
3		pibt2.21	$⊢ W = \{x \in Top \| \forall y \in (𝒫 ⋃ x ∖ Fin) \exists z \in ⋃ x z \in limPt (x) (y)\}$
4	1 2	pibp19	$⊢ J \in C \leftrightarrow (J \in Top \land \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z))$
5	4	simplbi	$⊢ J \in C \to J \in Top$
6		eldif	$⊢ b \in (𝒫 X ∖ Fin) \leftrightarrow (b \in 𝒫 X \land \neg b \in Fin)$
7		velpw	$⊢ b \in 𝒫 X \leftrightarrow b \subseteq X$
8	7	anbi1i	$⊢ (b \in 𝒫 X \land \neg b \in Fin) \leftrightarrow (b \subseteq X \land \neg b \in Fin)$
9		vex	$⊢ b \in V$
10		infinf	$⊢ b \in V \to (\neg b \in Fin \leftrightarrow ω ≼ b)$
11	9 10	ax-mp	$⊢ \neg b \in Fin \leftrightarrow ω ≼ b$
12	9	infcntss	$⊢ ω ≼ b \to \exists a (a \subseteq b \land a \approx ω)$
13	11 12	sylbi	$⊢ \neg b \in Fin \to \exists a (a \subseteq b \land a \approx ω)$
14	13	ad2antll	$⊢ (J \in C \land (b \subseteq X \land \neg b \in Fin)) \to \exists a (a \subseteq b \land a \approx ω)$
15		sstr	$⊢ (a \subseteq b \land b \subseteq X) \to a \subseteq X$
16	15	ancoms	$⊢ (b \subseteq X \land a \subseteq b) \to a \subseteq X$
17		simplr	$⊢ ((J \in C \land a \approx ω) \land (a \subseteq X \land limPt (J) (a) = \emptyset)) \to a \approx ω$
18		simpll	$⊢ (((J \in C \land a \approx ω) \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to (J \in C \land a \approx ω)$
19		0ss	$⊢ \emptyset \subseteq a$
20		sseq1	$⊢ limPt (J) (a) = \emptyset \to (limPt (J) (a) \subseteq a \leftrightarrow \emptyset \subseteq a)$
21	19 20	mpbiri	$⊢ limPt (J) (a) = \emptyset \to limPt (J) (a) \subseteq a$
22	21	adantl	$⊢ ((J \in Top \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to limPt (J) (a) \subseteq a$
23	1	cldlp	$⊢ (J \in Top \land a \subseteq X) \to (a \in Clsd (J) \leftrightarrow limPt (J) (a) \subseteq a)$
24	23	adantr	$⊢ ((J \in Top \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to (a \in Clsd (J) \leftrightarrow limPt (J) (a) \subseteq a)$
25	22 24	mpbird	$⊢ ((J \in Top \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to a \in Clsd (J)$
26	5 25	sylanl1	$⊢ ((J \in C \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to a \in Clsd (J)$
27	26	adantllr	$⊢ (((J \in C \land a \approx ω) \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to a \in Clsd (J)$
28		simpr	$⊢ (((J \in C \land a \approx ω) \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to limPt (J) (a) = \emptyset$
29	1	cldss	$⊢ a \in Clsd (J) \to a \subseteq X$
30	1	nlpineqsn	$⊢ (J \in Top \land a \subseteq X \land limPt (J) (a) = \emptyset) \to \forall p \in a \exists n \in J (p \in n \land n \cap a = \{p\})$
31		simpr	$⊢ (p \in n \land n \cap a = \{p\}) \to n \cap a = \{p\}$
32	31	reximi	$⊢ \exists n \in J (p \in n \land n \cap a = \{p\}) \to \exists n \in J n \cap a = \{p\}$
33	32	ralimi	$⊢ \forall p \in a \exists n \in J (p \in n \land n \cap a = \{p\}) \to \forall p \in a \exists n \in J n \cap a = \{p\}$
34		vex	$⊢ a \in V$
35		ineq1	$⊢ n = f (p) \to n \cap a = f (p) \cap a$
36	35	eqeq1d	$⊢ n = f (p) \to (n \cap a = \{p\} \leftrightarrow f (p) \cap a = \{p\})$
37	34 36	ac6s	$⊢ \forall p \in a \exists n \in J n \cap a = \{p\} \to \exists f (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\})$
38	30 33 37	3syl	$⊢ (J \in Top \land a \subseteq X \land limPt (J) (a) = \emptyset) \to \exists f (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\})$
39		fvineqsnf1	$⊢ (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to f : a \underset{1-1}{⟶} J$
40		simpr	$⊢ (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to \forall p \in a f (p) \cap a = \{p\}$
41	39 40	jca	$⊢ (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})$
42	41	eximi	$⊢ \exists f (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to \exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})$
43	38 42	syl	$⊢ (J \in Top \land a \subseteq X \land limPt (J) (a) = \emptyset) \to \exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})$
44	29 43	syl3an2	$⊢ (J \in Top \land a \in Clsd (J) \land limPt (J) (a) = \emptyset) \to \exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})$
45	5 44	syl3an1	$⊢ (J \in C \land a \in Clsd (J) \land limPt (J) (a) = \emptyset) \to \exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})$
46	45	3adant1r	$⊢ ((J \in C \land a \approx ω) \land a \in Clsd (J) \land limPt (J) (a) = \emptyset) \to \exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})$
47		simpr	$⊢ ((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \to f : a \underset{1-1}{⟶} J$
48		vsnid	$⊢ p \in \{p\}$
49		eleq2	$⊢ f (p) \cap a = \{p\} \to (p \in (f (p) \cap a) \leftrightarrow p \in \{p\})$
50	48 49	mpbiri	$⊢ f (p) \cap a = \{p\} \to p \in (f (p) \cap a)$
51	50	elin1d	$⊢ f (p) \cap a = \{p\} \to p \in f (p)$
52	51	ralimi	$⊢ \forall p \in a f (p) \cap a = \{p\} \to \forall p \in a p \in f (p)$
53		ralssiun	$⊢ \forall p \in a p \in f (p) \to a \subseteq ⋃_{p \in a} f (p)$
54	52 53	syl	$⊢ \forall p \in a f (p) \cap a = \{p\} \to a \subseteq ⋃_{p \in a} f (p)$
55	54	adantl	$⊢ (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to a \subseteq ⋃_{p \in a} f (p)$
56		f1fn	$⊢ f : a \underset{1-1}{⟶} J \to f Fn a$
57		fniunfv	$⊢ f Fn a \to ⋃_{p \in a} f (p) = ⋃ ran f$
58	56 57	syl	$⊢ f : a \underset{1-1}{⟶} J \to ⋃_{p \in a} f (p) = ⋃ ran f$
59	58	adantr	$⊢ (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to ⋃_{p \in a} f (p) = ⋃ ran f$
60	55 59	sseqtrd	$⊢ (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to a \subseteq ⋃ ran f$
61	1	cldopn	$⊢ a \in Clsd (J) \to X ∖ a \in J$
62	61	ad2antll	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to X ∖ a \in J$
63	62	anim1i	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land a \subseteq ⋃ ran f) \to (X ∖ a \in J \land a \subseteq ⋃ ran f)$
64	63	ancomd	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land a \subseteq ⋃ ran f) \to (a \subseteq ⋃ ran f \land X ∖ a \in J)$
65	29	ad2antll	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to a \subseteq X$
66	65	anim1i	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land (a \subseteq ⋃ ran f \land X ∖ a \in J)) \to (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \in J))$
67		unisng	$⊢ X ∖ a \in J \to ⋃ \{X ∖ a\} = X ∖ a$
68	67	eqcomd	$⊢ X ∖ a \in J \to X ∖ a = ⋃ \{X ∖ a\}$
69		eqimss	$⊢ X ∖ a = ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ \{X ∖ a\}$
70		ssun4	$⊢ X ∖ a \subseteq ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ ran f \cup ⋃ \{X ∖ a\}$
71		uniun	$⊢ ⋃ (ran f \cup \{X ∖ a\}) = ⋃ ran f \cup ⋃ \{X ∖ a\}$
72	70 71	sseqtrrdi	$⊢ X ∖ a \subseteq ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
73	68 69 72	3syl	$⊢ X ∖ a \in J \to X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
74		ssun3	$⊢ a \subseteq ⋃ ran f \to a \subseteq ⋃ ran f \cup ⋃ \{X ∖ a\}$
75	74 71	sseqtrrdi	$⊢ a \subseteq ⋃ ran f \to a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
76		uncom	$⊢ a \cup (X ∖ a) = (X ∖ a) \cup a$
77		undif1	$⊢ (X ∖ a) \cup a = X \cup a$
78	76 77	eqtri	$⊢ a \cup (X ∖ a) = X \cup a$
79		ssequn2	$⊢ a \subseteq X \leftrightarrow X \cup a = X$
80	79	biimpi	$⊢ a \subseteq X \to X \cup a = X$
81	78 80	syl5eq	$⊢ a \subseteq X \to a \cup (X ∖ a) = X$
82	81	adantr	$⊢ (a \subseteq X \land (a \subseteq ⋃ (ran f \cup \{X ∖ a\}) \land X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\}))) \to a \cup (X ∖ a) = X$
83		unss12	$⊢ (a \subseteq ⋃ (ran f \cup \{X ∖ a\}) \land X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})) \to a \cup (X ∖ a) \subseteq ⋃ (ran f \cup \{X ∖ a\}) \cup ⋃ (ran f \cup \{X ∖ a\})$
84		unidm	$⊢ ⋃ (ran f \cup \{X ∖ a\}) \cup ⋃ (ran f \cup \{X ∖ a\}) = ⋃ (ran f \cup \{X ∖ a\})$
85	83 84	sseqtrdi	$⊢ (a \subseteq ⋃ (ran f \cup \{X ∖ a\}) \land X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})) \to a \cup (X ∖ a) \subseteq ⋃ (ran f \cup \{X ∖ a\})$
86	85	adantl	$⊢ (a \subseteq X \land (a \subseteq ⋃ (ran f \cup \{X ∖ a\}) \land X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\}))) \to a \cup (X ∖ a) \subseteq ⋃ (ran f \cup \{X ∖ a\})$
87	82 86	eqsstrrd	$⊢ (a \subseteq X \land (a \subseteq ⋃ (ran f \cup \{X ∖ a\}) \land X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\}))) \to X \subseteq ⋃ (ran f \cup \{X ∖ a\})$
88	75 87	sylanr1	$⊢ (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\}))) \to X \subseteq ⋃ (ran f \cup \{X ∖ a\})$
89	73 88	sylanr2	$⊢ (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \in J)) \to X \subseteq ⋃ (ran f \cup \{X ∖ a\})$
90	89	adantl	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \in J))) \to X \subseteq ⋃ (ran f \cup \{X ∖ a\})$
91		f1f	$⊢ f : a \underset{1-1}{⟶} J \to f : a ⟶ J$
92		frn	$⊢ f : a ⟶ J \to ran f \subseteq J$
93	91 92	syl	$⊢ f : a \underset{1-1}{⟶} J \to ran f \subseteq J$
94	1	topopn	$⊢ J \in Top \to X \in J$
95	1	difopn	$⊢ (X \in J \land a \in Clsd (J)) \to X ∖ a \in J$
96	94 95	sylan	$⊢ (J \in Top \land a \in Clsd (J)) \to X ∖ a \in J$
97	96	snssd	$⊢ (J \in Top \land a \in Clsd (J)) \to \{X ∖ a\} \subseteq J$
98		unss12	$⊢ (ran f \subseteq J \land \{X ∖ a\} \subseteq J) \to ran f \cup \{X ∖ a\} \subseteq J \cup J$
99		unidm	$⊢ J \cup J = J$
100	98 99	sseqtrdi	$⊢ (ran f \subseteq J \land \{X ∖ a\} \subseteq J) \to ran f \cup \{X ∖ a\} \subseteq J$
101	93 97 100	syl2an	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to ran f \cup \{X ∖ a\} \subseteq J$
102		uniss	$⊢ ran f \cup \{X ∖ a\} \subseteq J \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq ⋃ J$
103	102 1	sseqtrrdi	$⊢ ran f \cup \{X ∖ a\} \subseteq J \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq X$
104	101 103	syl	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq X$
105	104	adantr	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \in J))) \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq X$
106	90 105	eqssd	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \in J))) \to X = ⋃ (ran f \cup \{X ∖ a\})$
107	66 106	syldan	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land (a \subseteq ⋃ ran f \land X ∖ a \in J)) \to X = ⋃ (ran f \cup \{X ∖ a\})$
108	64 107	syldan	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land a \subseteq ⋃ ran f) \to X = ⋃ (ran f \cup \{X ∖ a\})$
109	60 108	sylan2	$⊢ ((f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to X = ⋃ (ran f \cup \{X ∖ a\})$
110	109	ancom1s	$⊢ (((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to X = ⋃ (ran f \cup \{X ∖ a\})$
111	110	ex	$⊢ ((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \to ((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to X = ⋃ (ran f \cup \{X ∖ a\}))$
112	47 111	mpand	$⊢ ((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \to (\forall p \in a f (p) \cap a = \{p\} \to X = ⋃ (ran f \cup \{X ∖ a\}))$
113	112	impr	$⊢ ((J \in Top \land a \in Clsd (J)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to X = ⋃ (ran f \cup \{X ∖ a\})$
114	113	adantlrr	$⊢ ((J \in Top \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to X = ⋃ (ran f \cup \{X ∖ a\})$
115	5 114	sylanl1	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to X = ⋃ (ran f \cup \{X ∖ a\})$
116		vex	$⊢ f \in V$
117		f1f1orn	$⊢ f : a \underset{1-1}{⟶} J \to f : a \underset{1-1 onto}{⟶} ran f$
118		f1oen3g	$⊢ (f \in V \land f : a \underset{1-1 onto}{⟶} ran f) \to a \approx ran f$
119	116 117 118	sylancr	$⊢ f : a \underset{1-1}{⟶} J \to a \approx ran f$
120		enen1	$⊢ a \approx ran f \to (a \approx ω \leftrightarrow ran f \approx ω)$
121		endom	$⊢ ran f \approx ω \to ran f ≼ ω$
122		snfi	$⊢ \{X ∖ a\} \in Fin$
123		isfinite	$⊢ \{X ∖ a\} \in Fin \leftrightarrow \{X ∖ a\} ≺ ω$
124	122 123	mpbi	$⊢ \{X ∖ a\} ≺ ω$
125		sdomdom	$⊢ \{X ∖ a\} ≺ ω \to \{X ∖ a\} ≼ ω$
126	124 125	ax-mp	$⊢ \{X ∖ a\} ≼ ω$
127		unctb	$⊢ (ran f ≼ ω \land \{X ∖ a\} ≼ ω) \to (ran f \cup \{X ∖ a\}) ≼ ω$
128	121 126 127	sylancl	$⊢ ran f \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω$
129	120 128	syl6bi	$⊢ a \approx ran f \to (a \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω)$
130	119 129	syl	$⊢ f : a \underset{1-1}{⟶} J \to (a \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω)$
131	130	impcom	$⊢ (a \approx ω \land f : a \underset{1-1}{⟶} J) \to (ran f \cup \{X ∖ a\}) ≼ ω$
132	131	adantll	$⊢ ((a \in Clsd (J) \land a \approx ω) \land f : a \underset{1-1}{⟶} J) \to (ran f \cup \{X ∖ a\}) ≼ ω$
133	132	ad2ant2lr	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to (ran f \cup \{X ∖ a\}) ≼ ω$
134	101	ancoms	$⊢ ((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \to ran f \cup \{X ∖ a\} \subseteq J$
135	134	adantrr	$⊢ ((J \in Top \land a \in Clsd (J)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ran f \cup \{X ∖ a\} \subseteq J$
136	135	adantlrr	$⊢ ((J \in Top \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ran f \cup \{X ∖ a\} \subseteq J$
137	5 136	sylanl1	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ran f \cup \{X ∖ a\} \subseteq J$
138		elpw2g	$⊢ J \in C \to (ran f \cup \{X ∖ a\} \in 𝒫 J \leftrightarrow ran f \cup \{X ∖ a\} \subseteq J)$
139	138	biimprd	$⊢ J \in C \to (ran f \cup \{X ∖ a\} \subseteq J \to ran f \cup \{X ∖ a\} \in 𝒫 J)$
140	139	ad2antrr	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to (ran f \cup \{X ∖ a\} \subseteq J \to ran f \cup \{X ∖ a\} \in 𝒫 J)$
141	137 140	mpd	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ran f \cup \{X ∖ a\} \in 𝒫 J$
142	4	simprbi	$⊢ J \in C \to \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
143		unieq	$⊢ s = z \to ⋃ s = ⋃ z$
144	143	eqeq2d	$⊢ s = z \to (X = ⋃ s \leftrightarrow X = ⋃ z)$
145	144	cbvrexvw	$⊢ \exists s \in (𝒫 y \cap Fin) X = ⋃ s \leftrightarrow \exists z \in (𝒫 y \cap Fin) X = ⋃ z$
146	145	imbi2i	$⊢ ((X = ⋃ y \land y ≼ ω) \to \exists s \in (𝒫 y \cap Fin) X = ⋃ s) \leftrightarrow ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
147	146	ralbii	$⊢ \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists s \in (𝒫 y \cap Fin) X = ⋃ s) \leftrightarrow \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
148	142 147	sylibr	$⊢ J \in C \to \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists s \in (𝒫 y \cap Fin) X = ⋃ s)$
149		unieq	$⊢ y = ran f \cup \{X ∖ a\} \to ⋃ y = ⋃ (ran f \cup \{X ∖ a\})$
150	149	eqeq2d	$⊢ y = ran f \cup \{X ∖ a\} \to (X = ⋃ y \leftrightarrow X = ⋃ (ran f \cup \{X ∖ a\}))$
151		breq1	$⊢ y = ran f \cup \{X ∖ a\} \to (y ≼ ω \leftrightarrow (ran f \cup \{X ∖ a\}) ≼ ω)$
152	150 151	anbi12d	$⊢ y = ran f \cup \{X ∖ a\} \to ((X = ⋃ y \land y ≼ ω) \leftrightarrow (X = ⋃ (ran f \cup \{X ∖ a\}) \land (ran f \cup \{X ∖ a\}) ≼ ω))$
153		pweq	$⊢ y = ran f \cup \{X ∖ a\} \to 𝒫 y = 𝒫 (ran f \cup \{X ∖ a\})$
154	153	ineq1d	$⊢ y = ran f \cup \{X ∖ a\} \to 𝒫 y \cap Fin = 𝒫 (ran f \cup \{X ∖ a\}) \cap Fin$
155	154	rexeqdv	$⊢ y = ran f \cup \{X ∖ a\} \to (\exists s \in (𝒫 y \cap Fin) X = ⋃ s \leftrightarrow \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s)$
156	152 155	imbi12d	$⊢ y = ran f \cup \{X ∖ a\} \to (((X = ⋃ y \land y ≼ ω) \to \exists s \in (𝒫 y \cap Fin) X = ⋃ s) \leftrightarrow ((X = ⋃ (ran f \cup \{X ∖ a\}) \land (ran f \cup \{X ∖ a\}) ≼ ω) \to \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s))$
157	156	rspccv	$⊢ \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists s \in (𝒫 y \cap Fin) X = ⋃ s) \to (ran f \cup \{X ∖ a\} \in 𝒫 J \to ((X = ⋃ (ran f \cup \{X ∖ a\}) \land (ran f \cup \{X ∖ a\}) ≼ ω) \to \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s))$
158	148 157	syl	$⊢ J \in C \to (ran f \cup \{X ∖ a\} \in 𝒫 J \to ((X = ⋃ (ran f \cup \{X ∖ a\}) \land (ran f \cup \{X ∖ a\}) ≼ ω) \to \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s))$
159	158	ad2antrr	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to (ran f \cup \{X ∖ a\} \in 𝒫 J \to ((X = ⋃ (ran f \cup \{X ∖ a\}) \land (ran f \cup \{X ∖ a\}) ≼ ω) \to \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s))$
160	141 159	mpd	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ((X = ⋃ (ran f \cup \{X ∖ a\}) \land (ran f \cup \{X ∖ a\}) ≼ ω) \to \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s)$
161	115 133 160	mp2and	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s$
162		df-rex	$⊢ \exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s \leftrightarrow \exists s (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s)$
163		elinel1	$⊢ s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s \in 𝒫 (ran f \cup \{X ∖ a\})$
164		velpw	$⊢ s \in 𝒫 (ran f \cup \{X ∖ a\}) \leftrightarrow s \subseteq ran f \cup \{X ∖ a\}$
165		ssdif	$⊢ s \subseteq ran f \cup \{X ∖ a\} \to s ∖ \{X ∖ a\} \subseteq (ran f \cup \{X ∖ a\}) ∖ \{X ∖ a\}$
166		difun2	$⊢ (ran f \cup \{X ∖ a\}) ∖ \{X ∖ a\} = ran f ∖ \{X ∖ a\}$
167	165 166	sseqtrdi	$⊢ s \subseteq ran f \cup \{X ∖ a\} \to s ∖ \{X ∖ a\} \subseteq ran f ∖ \{X ∖ a\}$
168	167	difss2d	$⊢ s \subseteq ran f \cup \{X ∖ a\} \to s ∖ \{X ∖ a\} \subseteq ran f$
169	164 168	sylbi	$⊢ s \in 𝒫 (ran f \cup \{X ∖ a\}) \to s ∖ \{X ∖ a\} \subseteq ran f$
170	163 169	syl	$⊢ s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s ∖ \{X ∖ a\} \subseteq ran f$
171	170	a1i	$⊢ (J \in Top \land a \subseteq X) \to (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s ∖ \{X ∖ a\} \subseteq ran f)$
172		sseq2	$⊢ X = ⋃ s \to (a \subseteq X \leftrightarrow a \subseteq ⋃ s)$
173		uniexg	$⊢ J \in Top \to ⋃ J \in V$
174	1 173	eqeltrid	$⊢ J \in Top \to X \in V$
175		difexg	$⊢ X \in V \to X ∖ a \in V$
176		unisng	$⊢ X ∖ a \in V \to ⋃ \{X ∖ a\} = X ∖ a$
177	174 175 176	3syl	$⊢ J \in Top \to ⋃ \{X ∖ a\} = X ∖ a$
178	177	ineq2d	$⊢ J \in Top \to a \cap ⋃ \{X ∖ a\} = a \cap (X ∖ a)$
179		disjdif	$⊢ a \cap (X ∖ a) = \emptyset$
180	178 179	eqtrdi	$⊢ J \in Top \to a \cap ⋃ \{X ∖ a\} = \emptyset$
181		inunissunidif	$⊢ a \cap ⋃ \{X ∖ a\} = \emptyset \to (a \subseteq ⋃ s \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
182	180 181	syl	$⊢ J \in Top \to (a \subseteq ⋃ s \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
183	172 182	sylan9bbr	$⊢ (J \in Top \land X = ⋃ s) \to (a \subseteq X \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
184	183	biimpd	$⊢ (J \in Top \land X = ⋃ s) \to (a \subseteq X \to a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
185	184	impancom	$⊢ (J \in Top \land a \subseteq X) \to (X = ⋃ s \to a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
186	171 185	anim12d	$⊢ (J \in Top \land a \subseteq X) \to ((s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\})))$
187	5 29 186	syl2an	$⊢ (J \in C \land a \in Clsd (J)) \to ((s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\})))$
188	187	adantrr	$⊢ (J \in C \land (a \in Clsd (J) \land a \approx ω)) \to ((s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\})))$
189	188	anim2d	$⊢ (J \in C \land (a \in Clsd (J) \land a \approx ω)) \to (((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \land (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s)) \to ((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \land (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\}))))$
190	119	ad2antrr	$⊢ ((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \land (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\}))) \to a \approx ran f$
191		fvineqsneq	$⊢ ((f Fn a \land \forall p \in a f (p) \cap a = \{p\}) \land (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\}))) \to s ∖ \{X ∖ a\} = ran f$
192	56 191	sylanl1	$⊢ ((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \land (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\}))) \to s ∖ \{X ∖ a\} = ran f$
193		vex	$⊢ s \in V$
194		difss	$⊢ s ∖ \{X ∖ a\} \subseteq s$
195		ssdomg	$⊢ s \in V \to (s ∖ \{X ∖ a\} \subseteq s \to (s ∖ \{X ∖ a\}) ≼ s)$
196	193 194 195	mp2	$⊢ (s ∖ \{X ∖ a\}) ≼ s$
197	192 196	eqbrtrrdi	$⊢ ((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \land (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\}))) \to ran f ≼ s$
198		endomtr	$⊢ (a \approx ran f \land ran f ≼ s) \to a ≼ s$
199	190 197 198	syl2anc	$⊢ ((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \land (s ∖ \{X ∖ a\} \subseteq ran f \land a \subseteq ⋃ (s ∖ \{X ∖ a\}))) \to a ≼ s$
200	189 199	syl6	$⊢ (J \in C \land (a \in Clsd (J) \land a \approx ω)) \to (((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \land (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s)) \to a ≼ s)$
201	200	expdimp	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ((s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to a ≼ s)$
202		elinel2	$⊢ s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s \in Fin$
203	202	adantr	$⊢ (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to s \in Fin$
204	203	a1i	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ((s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to s \in Fin)$
205	201 204	jcad	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to ((s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to (a ≼ s \land s \in Fin))$
206	205	eximdv	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to (\exists s (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to \exists s (a ≼ s \land s \in Fin))$
207	162 206	syl5bi	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to (\exists s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) X = ⋃ s \to \exists s (a ≼ s \land s \in Fin))$
208	161 207	mpd	$⊢ ((J \in C \land (a \in Clsd (J) \land a \approx ω)) \land (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\})) \to \exists s (a ≼ s \land s \in Fin)$
209	208	ex	$⊢ (J \in C \land (a \in Clsd (J) \land a \approx ω)) \to ((f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to \exists s (a ≼ s \land s \in Fin))$
210	209	exlimdv	$⊢ (J \in C \land (a \in Clsd (J) \land a \approx ω)) \to (\exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to \exists s (a ≼ s \land s \in Fin))$
211	210	anass1rs	$⊢ ((J \in C \land a \approx ω) \land a \in Clsd (J)) \to (\exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to \exists s (a ≼ s \land s \in Fin))$
212	211	3adant3	$⊢ ((J \in C \land a \approx ω) \land a \in Clsd (J) \land limPt (J) (a) = \emptyset) \to (\exists f (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to \exists s (a ≼ s \land s \in Fin))$
213	46 212	mpd	$⊢ ((J \in C \land a \approx ω) \land a \in Clsd (J) \land limPt (J) (a) = \emptyset) \to \exists s (a ≼ s \land s \in Fin)$
214	18 27 28 213	syl3anc	$⊢ (((J \in C \land a \approx ω) \land a \subseteq X) \land limPt (J) (a) = \emptyset) \to \exists s (a ≼ s \land s \in Fin)$
215	214	anasss	$⊢ ((J \in C \land a \approx ω) \land (a \subseteq X \land limPt (J) (a) = \emptyset)) \to \exists s (a ≼ s \land s \in Fin)$
216		isfinite	$⊢ s \in Fin \leftrightarrow s ≺ ω$
217		domsdomtr	$⊢ (a ≼ s \land s ≺ ω) \to a ≺ ω$
218	216 217	sylan2b	$⊢ (a ≼ s \land s \in Fin) \to a ≺ ω$
219	218	exlimiv	$⊢ \exists s (a ≼ s \land s \in Fin) \to a ≺ ω$
220		sdomnen	$⊢ a ≺ ω \to \neg a \approx ω$
221	215 219 220	3syl	$⊢ ((J \in C \land a \approx ω) \land (a \subseteq X \land limPt (J) (a) = \emptyset)) \to \neg a \approx ω$
222	17 221	pm2.65da	$⊢ (J \in C \land a \approx ω) \to \neg (a \subseteq X \land limPt (J) (a) = \emptyset)$
223		imnan	$⊢ (a \subseteq X \to \neg limPt (J) (a) = \emptyset) \leftrightarrow \neg (a \subseteq X \land limPt (J) (a) = \emptyset)$
224	222 223	sylibr	$⊢ (J \in C \land a \approx ω) \to (a \subseteq X \to \neg limPt (J) (a) = \emptyset)$
225	224	imp	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \neg limPt (J) (a) = \emptyset$
226		neq0	$⊢ \neg limPt (J) (a) = \emptyset \leftrightarrow \exists s s \in limPt (J) (a)$
227	225 226	sylib	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \exists s s \in limPt (J) (a)$
228	1	lpss	$⊢ (J \in Top \land a \subseteq X) \to limPt (J) (a) \subseteq X$
229	5 228	sylan	$⊢ (J \in C \land a \subseteq X) \to limPt (J) (a) \subseteq X$
230	229	adantlr	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to limPt (J) (a) \subseteq X$
231	230	sseld	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to (s \in limPt (J) (a) \to s \in X)$
232	231	ancrd	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to (s \in limPt (J) (a) \to (s \in X \land s \in limPt (J) (a)))$
233	232	eximdv	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to (\exists s s \in limPt (J) (a) \to \exists s (s \in X \land s \in limPt (J) (a)))$
234		df-rex	$⊢ \exists s \in X s \in limPt (J) (a) \leftrightarrow \exists s (s \in X \land s \in limPt (J) (a))$
235	233 234	syl6ibr	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to (\exists s s \in limPt (J) (a) \to \exists s \in X s \in limPt (J) (a))$
236	227 235	mpd	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \exists s \in X s \in limPt (J) (a)$
237	16 236	sylan2	$⊢ ((J \in C \land a \approx ω) \land (b \subseteq X \land a \subseteq b)) \to \exists s \in X s \in limPt (J) (a)$
238	1	lpss3	$⊢ (J \in Top \land b \subseteq X \land a \subseteq b) \to limPt (J) (a) \subseteq limPt (J) (b)$
239	238	3expb	$⊢ (J \in Top \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
240	5 239	sylan	$⊢ (J \in C \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
241	240	adantlr	$⊢ ((J \in C \land a \approx ω) \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
242	241	sseld	$⊢ ((J \in C \land a \approx ω) \land (b \subseteq X \land a \subseteq b)) \to (s \in limPt (J) (a) \to s \in limPt (J) (b))$
243	242	reximdv	$⊢ ((J \in C \land a \approx ω) \land (b \subseteq X \land a \subseteq b)) \to (\exists s \in X s \in limPt (J) (a) \to \exists s \in X s \in limPt (J) (b))$
244	237 243	mpd	$⊢ ((J \in C \land a \approx ω) \land (b \subseteq X \land a \subseteq b)) \to \exists s \in X s \in limPt (J) (b)$
245	244	an42s	$⊢ ((J \in C \land b \subseteq X) \land (a \subseteq b \land a \approx ω)) \to \exists s \in X s \in limPt (J) (b)$
246	245	ex	$⊢ (J \in C \land b \subseteq X) \to ((a \subseteq b \land a \approx ω) \to \exists s \in X s \in limPt (J) (b))$
247	246	exlimdv	$⊢ (J \in C \land b \subseteq X) \to (\exists a (a \subseteq b \land a \approx ω) \to \exists s \in X s \in limPt (J) (b))$
248	247	adantrr	$⊢ (J \in C \land (b \subseteq X \land \neg b \in Fin)) \to (\exists a (a \subseteq b \land a \approx ω) \to \exists s \in X s \in limPt (J) (b))$
249	14 248	mpd	$⊢ (J \in C \land (b \subseteq X \land \neg b \in Fin)) \to \exists s \in X s \in limPt (J) (b)$
250	8 249	sylan2b	$⊢ (J \in C \land (b \in 𝒫 X \land \neg b \in Fin)) \to \exists s \in X s \in limPt (J) (b)$
251	6 250	sylan2b	$⊢ (J \in C \land b \in (𝒫 X ∖ Fin)) \to \exists s \in X s \in limPt (J) (b)$
252	251	ralrimiva	$⊢ J \in C \to \forall b \in (𝒫 X ∖ Fin) \exists s \in X s \in limPt (J) (b)$
253		simpr	$⊢ (y = b \land z = s) \to z = s$
254		fveq2	$⊢ y = b \to limPt (J) (y) = limPt (J) (b)$
255	254	adantr	$⊢ (y = b \land z = s) \to limPt (J) (y) = limPt (J) (b)$
256	253 255	eleq12d	$⊢ (y = b \land z = s) \to (z \in limPt (J) (y) \leftrightarrow s \in limPt (J) (b))$
257	256	cbvrexdva	$⊢ y = b \to (\exists z \in X z \in limPt (J) (y) \leftrightarrow \exists s \in X s \in limPt (J) (b))$
258	257	cbvralvw	$⊢ \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y) \leftrightarrow \forall b \in (𝒫 X ∖ Fin) \exists s \in X s \in limPt (J) (b)$
259	252 258	sylibr	$⊢ J \in C \to \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y)$
260	1 3	pibp21	$⊢ J \in W \leftrightarrow (J \in Top \land \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y))$
261	5 259 260	sylanbrc	$⊢ J \in C \to J \in W$

Metamath Proof Explorer

Theorem pibt2

Proof