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) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

	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		infinf	$⊢ b \in V \to (\neg b \in Fin \leftrightarrow ω ≼ b)$
10	9	elv	$⊢ \neg b \in Fin \leftrightarrow ω ≼ b$
11		vex	$⊢ b \in V$
12	11	infcntss	$⊢ ω ≼ b \to \exists a (a \subseteq b \land a \approx ω)$
13	10 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		vex	$⊢ a \in V$
31		simp1	$⊢ (J \in Top \land a \subseteq X \land limPt (J) (a) = \emptyset) \to J \in Top$
32	31	elexd	$⊢ (J \in Top \land a \subseteq X \land limPt (J) (a) = \emptyset) \to J \in V$
33	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\})$
34		simpr	$⊢ (p \in n \land n \cap a = \{p\}) \to n \cap a = \{p\}$
35	34	reximi	$⊢ \exists n \in J (p \in n \land n \cap a = \{p\}) \to \exists n \in J n \cap a = \{p\}$
36	35	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\}$
37	33 36	syl	$⊢ (J \in Top \land a \subseteq X \land limPt (J) (a) = \emptyset) \to \forall p \in a \exists n \in J n \cap a = \{p\}$
38		ineq1	$⊢ n = f (p) \to n \cap a = f (p) \cap a$
39	38	eqeq1d	$⊢ n = f (p) \to (n \cap a = \{p\} \leftrightarrow f (p) \cap a = \{p\})$
40	39	ac6	$⊢ (a \in V \land J \in V \land \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\})$
41	30 32 37 40	mp3an2i	$⊢ (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\})$
42		fvineqsnf1	$⊢ (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to f : a \underset{1-1}{⟶} J$
43		simpr	$⊢ (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to \forall p \in a f (p) \cap a = \{p\}$
44	42 43	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\})$
45	44	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\})$
46	41 45	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\})$
47	29 46	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\})$
48	5 47	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\})$
49	48	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\})$
50		simpr	$⊢ ((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \to f : a \underset{1-1}{⟶} J$
51		vsnid	$⊢ p \in \{p\}$
52		eleq2	$⊢ f (p) \cap a = \{p\} \to (p \in (f (p) \cap a) \leftrightarrow p \in \{p\})$
53	51 52	mpbiri	$⊢ f (p) \cap a = \{p\} \to p \in (f (p) \cap a)$
54	53	elin1d	$⊢ f (p) \cap a = \{p\} \to p \in f (p)$
55	54	ralimi	$⊢ \forall p \in a f (p) \cap a = \{p\} \to \forall p \in a p \in f (p)$
56		ralssiun	$⊢ \forall p \in a p \in f (p) \to a \subseteq ⋃_{p \in a} f (p)$
57	55 56	syl	$⊢ \forall p \in a f (p) \cap a = \{p\} \to a \subseteq ⋃_{p \in a} f (p)$
58	57	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)$
59		f1fn	$⊢ f : a \underset{1-1}{⟶} J \to f Fn a$
60		fniunfv	$⊢ f Fn a \to ⋃_{p \in a} f (p) = ⋃ ran f$
61	59 60	syl	$⊢ f : a \underset{1-1}{⟶} J \to ⋃_{p \in a} f (p) = ⋃ ran f$
62	61	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$
63	58 62	sseqtrd	$⊢ (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to a \subseteq ⋃ ran f$
64	1	cldopn	$⊢ a \in Clsd (J) \to X ∖ a \in J$
65	64	ad2antll	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to X ∖ a \in J$
66	65	anim1ci	$⊢ ((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)$
67	29	ad2antll	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to a \subseteq X$
68	67	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))$
69		unisng	$⊢ X ∖ a \in J \to ⋃ \{X ∖ a\} = X ∖ a$
70	69	eqcomd	$⊢ X ∖ a \in J \to X ∖ a = ⋃ \{X ∖ a\}$
71		eqimss	$⊢ X ∖ a = ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ \{X ∖ a\}$
72		ssun4	$⊢ X ∖ a \subseteq ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ ran f \cup ⋃ \{X ∖ a\}$
73		uniun	$⊢ ⋃ (ran f \cup \{X ∖ a\}) = ⋃ ran f \cup ⋃ \{X ∖ a\}$
74	72 73	sseqtrrdi	$⊢ X ∖ a \subseteq ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
75	70 71 74	3syl	$⊢ X ∖ a \in J \to X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
76		ssun3	$⊢ a \subseteq ⋃ ran f \to a \subseteq ⋃ ran f \cup ⋃ \{X ∖ a\}$
77	76 73	sseqtrrdi	$⊢ a \subseteq ⋃ ran f \to a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
78		uncom	$⊢ a \cup (X ∖ a) = (X ∖ a) \cup a$
79		undif1	$⊢ (X ∖ a) \cup a = X \cup a$
80	78 79	eqtri	$⊢ a \cup (X ∖ a) = X \cup a$
81		ssequn2	$⊢ a \subseteq X \leftrightarrow X \cup a = X$
82	81	biimpi	$⊢ a \subseteq X \to X \cup a = X$
83	80 82	eqtrid	$⊢ a \subseteq X \to a \cup (X ∖ a) = X$
84	83	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$
85		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\})$
86		unidm	$⊢ ⋃ (ran f \cup \{X ∖ a\}) \cup ⋃ (ran f \cup \{X ∖ a\}) = ⋃ (ran f \cup \{X ∖ a\})$
87	85 86	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\})$
88	87	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\})$
89	84 88	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\})$
90	77 89	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\})$
91	75 90	sylanr2	$⊢ (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \in J)) \to X \subseteq ⋃ (ran f \cup \{X ∖ a\})$
92	91	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\})$
93		f1f	$⊢ f : a \underset{1-1}{⟶} J \to f : a ⟶ J$
94	93	frnd	$⊢ f : a \underset{1-1}{⟶} J \to ran f \subseteq J$
95	1	topopn	$⊢ J \in Top \to X \in J$
96	1	difopn	$⊢ (X \in J \land a \in Clsd (J)) \to X ∖ a \in J$
97	95 96	sylan	$⊢ (J \in Top \land a \in Clsd (J)) \to X ∖ a \in J$
98	97	snssd	$⊢ (J \in Top \land a \in Clsd (J)) \to \{X ∖ a\} \subseteq J$
99		unss12	$⊢ (ran f \subseteq J \land \{X ∖ a\} \subseteq J) \to ran f \cup \{X ∖ a\} \subseteq J \cup J$
100		unidm	$⊢ J \cup J = J$
101	99 100	sseqtrdi	$⊢ (ran f \subseteq J \land \{X ∖ a\} \subseteq J) \to ran f \cup \{X ∖ a\} \subseteq J$
102	94 98 101	syl2an	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to ran f \cup \{X ∖ a\} \subseteq J$
103		uniss	$⊢ ran f \cup \{X ∖ a\} \subseteq J \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq ⋃ J$
104	103 1	sseqtrrdi	$⊢ ran f \cup \{X ∖ a\} \subseteq J \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq X$
105	102 104	syl	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq X$
106	105	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$
107	92 106	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\})$
108	68 107	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\})$
109	66 108	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\})$
110	63 109	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\})$
111	110	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\})$
112	111	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\}))$
113	50 112	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\}))$
114	113	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\})$
115	114	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\})$
116	5 115	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\})$
117		vex	$⊢ f \in V$
118		f1f1orn	$⊢ f : a \underset{1-1}{⟶} J \to f : a \underset{1-1 onto}{⟶} ran f$
119		f1oen3g	$⊢ (f \in V \land f : a \underset{1-1 onto}{⟶} ran f) \to a \approx ran f$
120	117 118 119	sylancr	$⊢ f : a \underset{1-1}{⟶} J \to a \approx ran f$
121		enen1	$⊢ a \approx ran f \to (a \approx ω \leftrightarrow ran f \approx ω)$
122		endom	$⊢ ran f \approx ω \to ran f ≼ ω$
123		snfi	$⊢ \{X ∖ a\} \in Fin$
124		fict	$⊢ \{X ∖ a\} \in Fin \to \{X ∖ a\} ≼ ω$
125	123 124	ax-mp	$⊢ \{X ∖ a\} ≼ ω$
126		unctb	$⊢ (ran f ≼ ω \land \{X ∖ a\} ≼ ω) \to (ran f \cup \{X ∖ a\}) ≼ ω$
127	122 125 126	sylancl	$⊢ ran f \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω$
128	121 127	biimtrdi	$⊢ a \approx ran f \to (a \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω)$
129	120 128	syl	$⊢ f : a \underset{1-1}{⟶} J \to (a \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω)$
130	129	impcom	$⊢ (a \approx ω \land f : a \underset{1-1}{⟶} J) \to (ran f \cup \{X ∖ a\}) ≼ ω$
131	130	adantll	$⊢ ((a \in Clsd (J) \land a \approx ω) \land f : a \underset{1-1}{⟶} J) \to (ran f \cup \{X ∖ a\}) ≼ ω$
132	131	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\}) ≼ ω$
133	102	ancoms	$⊢ ((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \to ran f \cup \{X ∖ a\} \subseteq J$
134	133	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$
135	134	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$
136	5 135	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$
137		elpw2g	$⊢ J \in C \to (ran f \cup \{X ∖ a\} \in 𝒫 J \leftrightarrow ran f \cup \{X ∖ a\} \subseteq J)$
138	137	biimprd	$⊢ J \in C \to (ran f \cup \{X ∖ a\} \subseteq J \to ran f \cup \{X ∖ a\} \in 𝒫 J)$
139	138	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)$
140	136 139	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$
141	4	simprbi	$⊢ J \in C \to \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists z \in (𝒫 y \cap Fin) X = ⋃ z)$
142		unieq	$⊢ s = z \to ⋃ s = ⋃ z$
143	142	eqeq2d	$⊢ s = z \to (X = ⋃ s \leftrightarrow X = ⋃ z)$
144	143	cbvrexvw	$⊢ \exists s \in (𝒫 y \cap Fin) X = ⋃ s \leftrightarrow \exists z \in (𝒫 y \cap Fin) X = ⋃ z$
145	144	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)$
146	145	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)$
147	141 146	sylibr	$⊢ J \in C \to \forall y \in 𝒫 J ((X = ⋃ y \land y ≼ ω) \to \exists s \in (𝒫 y \cap Fin) X = ⋃ s)$
148		unieq	$⊢ y = ran f \cup \{X ∖ a\} \to ⋃ y = ⋃ (ran f \cup \{X ∖ a\})$
149	148	eqeq2d	$⊢ y = ran f \cup \{X ∖ a\} \to (X = ⋃ y \leftrightarrow X = ⋃ (ran f \cup \{X ∖ a\}))$
150		breq1	$⊢ y = ran f \cup \{X ∖ a\} \to (y ≼ ω \leftrightarrow (ran f \cup \{X ∖ a\}) ≼ ω)$
151	149 150	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\}) ≼ ω))$
152		pweq	$⊢ y = ran f \cup \{X ∖ a\} \to 𝒫 y = 𝒫 (ran f \cup \{X ∖ a\})$
153	152	ineq1d	$⊢ y = ran f \cup \{X ∖ a\} \to 𝒫 y \cap Fin = 𝒫 (ran f \cup \{X ∖ a\}) \cap Fin$
154	153	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)$
155	151 154	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))$
156	155	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))$
157	147 156	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))$
158	157	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))$
159	140 158	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)$
160	116 132 159	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$
161		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)$
162		elinel1	$⊢ s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s \in 𝒫 (ran f \cup \{X ∖ a\})$
163		velpw	$⊢ s \in 𝒫 (ran f \cup \{X ∖ a\}) \leftrightarrow s \subseteq ran f \cup \{X ∖ a\}$
164		ssdif	$⊢ s \subseteq ran f \cup \{X ∖ a\} \to s ∖ \{X ∖ a\} \subseteq (ran f \cup \{X ∖ a\}) ∖ \{X ∖ a\}$
165		difun2	$⊢ (ran f \cup \{X ∖ a\}) ∖ \{X ∖ a\} = ran f ∖ \{X ∖ a\}$
166	164 165	sseqtrdi	$⊢ s \subseteq ran f \cup \{X ∖ a\} \to s ∖ \{X ∖ a\} \subseteq ran f ∖ \{X ∖ a\}$
167	166	difss2d	$⊢ s \subseteq ran f \cup \{X ∖ a\} \to s ∖ \{X ∖ a\} \subseteq ran f$
168	163 167	sylbi	$⊢ s \in 𝒫 (ran f \cup \{X ∖ a\}) \to s ∖ \{X ∖ a\} \subseteq ran f$
169	162 168	syl	$⊢ s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s ∖ \{X ∖ a\} \subseteq ran f$
170	169	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)$
171		sseq2	$⊢ X = ⋃ s \to (a \subseteq X \leftrightarrow a \subseteq ⋃ s)$
172	95	elexd	$⊢ J \in Top \to X \in V$
173		difexg	$⊢ X \in V \to X ∖ a \in V$
174		unisng	$⊢ X ∖ a \in V \to ⋃ \{X ∖ a\} = X ∖ a$
175	172 173 174	3syl	$⊢ J \in Top \to ⋃ \{X ∖ a\} = X ∖ a$
176	175	ineq2d	$⊢ J \in Top \to a \cap ⋃ \{X ∖ a\} = a \cap (X ∖ a)$
177		disjdif	$⊢ a \cap (X ∖ a) = \emptyset$
178	176 177	eqtrdi	$⊢ J \in Top \to a \cap ⋃ \{X ∖ a\} = \emptyset$
179		inunissunidif	$⊢ a \cap ⋃ \{X ∖ a\} = \emptyset \to (a \subseteq ⋃ s \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
180	178 179	syl	$⊢ J \in Top \to (a \subseteq ⋃ s \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
181	171 180	sylan9bbr	$⊢ (J \in Top \land X = ⋃ s) \to (a \subseteq X \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
182	181	biimpd	$⊢ (J \in Top \land X = ⋃ s) \to (a \subseteq X \to a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
183	182	impancom	$⊢ (J \in Top \land a \subseteq X) \to (X = ⋃ s \to a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
184	170 183	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\})))$
185	5 29 184	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\})))$
186	185	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\})))$
187	186	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\}))))$
188	120	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$
189		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$
190	59 189	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$
191		vex	$⊢ s \in V$
192		difss	$⊢ s ∖ \{X ∖ a\} \subseteq s$
193		ssdomg	$⊢ s \in V \to (s ∖ \{X ∖ a\} \subseteq s \to (s ∖ \{X ∖ a\}) ≼ s)$
194	191 192 193	mp2	$⊢ (s ∖ \{X ∖ a\}) ≼ s$
195	190 194	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$
196		endomtr	$⊢ (a \approx ran f \land ran f ≼ s) \to a ≼ s$
197	188 195 196	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$
198	187 197	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)$
199	198	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)$
200		elinel2	$⊢ s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s \in Fin$
201	200	adantr	$⊢ (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to s \in Fin$
202	199 201	jca2	$⊢ ((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))$
203	202	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))$
204	161 203	biimtrid	$⊢ ((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))$
205	160 204	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)$
206	205	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))$
207	206	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))$
208	207	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))$
209	208	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))$
210	49 209	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)$
211	18 27 28 210	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)$
212	211	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)$
213		isfinite	$⊢ s \in Fin \leftrightarrow s ≺ ω$
214		domsdomtr	$⊢ (a ≼ s \land s ≺ ω) \to a ≺ ω$
215	213 214	sylan2b	$⊢ (a ≼ s \land s \in Fin) \to a ≺ ω$
216	215	exlimiv	$⊢ \exists s (a ≼ s \land s \in Fin) \to a ≺ ω$
217		sdomnen	$⊢ a ≺ ω \to \neg a \approx ω$
218	212 216 217	3syl	$⊢ ((J \in C \land a \approx ω) \land (a \subseteq X \land limPt (J) (a) = \emptyset)) \to \neg a \approx ω$
219	17 218	pm2.65da	$⊢ (J \in C \land a \approx ω) \to \neg (a \subseteq X \land limPt (J) (a) = \emptyset)$
220		imnan	$⊢ (a \subseteq X \to \neg limPt (J) (a) = \emptyset) \leftrightarrow \neg (a \subseteq X \land limPt (J) (a) = \emptyset)$
221	219 220	sylibr	$⊢ (J \in C \land a \approx ω) \to (a \subseteq X \to \neg limPt (J) (a) = \emptyset)$
222	221	imp	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \neg limPt (J) (a) = \emptyset$
223		neq0	$⊢ \neg limPt (J) (a) = \emptyset \leftrightarrow \exists s s \in limPt (J) (a)$
224	222 223	sylib	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \exists s s \in limPt (J) (a)$
225	1	lpss	$⊢ (J \in Top \land a \subseteq X) \to limPt (J) (a) \subseteq X$
226	5 225	sylan	$⊢ (J \in C \land a \subseteq X) \to limPt (J) (a) \subseteq X$
227	226	adantlr	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to limPt (J) (a) \subseteq X$
228	227	sseld	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to (s \in limPt (J) (a) \to s \in X)$
229	228	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)))$
230	229	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)))$
231		df-rex	$⊢ \exists s \in X s \in limPt (J) (a) \leftrightarrow \exists s (s \in X \land s \in limPt (J) (a))$
232	230 231	imbitrrdi	$⊢ ((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))$
233	224 232	mpd	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \exists s \in X s \in limPt (J) (a)$
234	16 233	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)$
235	1	lpss3	$⊢ (J \in Top \land b \subseteq X \land a \subseteq b) \to limPt (J) (a) \subseteq limPt (J) (b)$
236	235	3expb	$⊢ (J \in Top \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
237	5 236	sylan	$⊢ (J \in C \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
238	237	adantlr	$⊢ ((J \in C \land a \approx ω) \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
239	238	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))$
240	239	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))$
241	234 240	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)$
242	241	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)$
243	242	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))$
244	243	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))$
245	244	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))$
246	14 245	mpd	$⊢ (J \in C \land (b \subseteq X \land \neg b \in Fin)) \to \exists s \in X s \in limPt (J) (b)$
247	8 246	sylan2b	$⊢ (J \in C \land (b \in 𝒫 X \land \neg b \in Fin)) \to \exists s \in X s \in limPt (J) (b)$
248	6 247	sylan2b	$⊢ (J \in C \land b \in (𝒫 X ∖ Fin)) \to \exists s \in X s \in limPt (J) (b)$
249	248	ralrimiva	$⊢ J \in C \to \forall b \in (𝒫 X ∖ Fin) \exists s \in X s \in limPt (J) (b)$
250		simpr	$⊢ (y = b \land z = s) \to z = s$
251		fveq2	$⊢ y = b \to limPt (J) (y) = limPt (J) (b)$
252	251	adantr	$⊢ (y = b \land z = s) \to limPt (J) (y) = limPt (J) (b)$
253	250 252	eleq12d	$⊢ (y = b \land z = s) \to (z \in limPt (J) (y) \leftrightarrow s \in limPt (J) (b))$
254	253	cbvrexdva	$⊢ y = b \to (\exists z \in X z \in limPt (J) (y) \leftrightarrow \exists s \in X s \in limPt (J) (b))$
255	254	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)$
256	249 255	sylibr	$⊢ J \in C \to \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y)$
257	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))$
258	5 256 257	sylanbrc	$⊢ J \in C \to J \in W$

Metamath Proof Explorer

Theorem pibt2

Proof