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		fvineqsnf1	$⊢ (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to f : a \underset{1-1}{⟶} J$
39		simpr	$⊢ (f : a ⟶ J \land \forall p \in a f (p) \cap a = \{p\}) \to \forall p \in a f (p) \cap a = \{p\}$
40	38 39	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\})$
41	40	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\})$
42	30 33 37 41	4syl	$⊢ (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\})$
43	29 42	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\})$
44	5 43	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\})$
45	44	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\})$
46		simpr	$⊢ ((J \in Top \land a \in Clsd (J)) \land f : a \underset{1-1}{⟶} J) \to f : a \underset{1-1}{⟶} J$
47		vsnid	$⊢ p \in \{p\}$
48		eleq2	$⊢ f (p) \cap a = \{p\} \to (p \in (f (p) \cap a) \leftrightarrow p \in \{p\})$
49	47 48	mpbiri	$⊢ f (p) \cap a = \{p\} \to p \in (f (p) \cap a)$
50	49	elin1d	$⊢ f (p) \cap a = \{p\} \to p \in f (p)$
51	50	ralimi	$⊢ \forall p \in a f (p) \cap a = \{p\} \to \forall p \in a p \in f (p)$
52		ralssiun	$⊢ \forall p \in a p \in f (p) \to a \subseteq ⋃_{p \in a} f (p)$
53	51 52	syl	$⊢ \forall p \in a f (p) \cap a = \{p\} \to a \subseteq ⋃_{p \in a} f (p)$
54	53	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)$
55		f1fn	$⊢ f : a \underset{1-1}{⟶} J \to f Fn a$
56		fniunfv	$⊢ f Fn a \to ⋃_{p \in a} f (p) = ⋃ ran f$
57	55 56	syl	$⊢ f : a \underset{1-1}{⟶} J \to ⋃_{p \in a} f (p) = ⋃ ran f$
58	57	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$
59	54 58	sseqtrd	$⊢ (f : a \underset{1-1}{⟶} J \land \forall p \in a f (p) \cap a = \{p\}) \to a \subseteq ⋃ ran f$
60	1	cldopn	$⊢ a \in Clsd (J) \to X ∖ a \in J$
61	60	ad2antll	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to X ∖ a \in J$
62	61	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)$
63	62	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)$
64	29	ad2antll	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to a \subseteq X$
65	64	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))$
66		unisng	$⊢ X ∖ a \in J \to ⋃ \{X ∖ a\} = X ∖ a$
67	66	eqcomd	$⊢ X ∖ a \in J \to X ∖ a = ⋃ \{X ∖ a\}$
68		eqimss	$⊢ X ∖ a = ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ \{X ∖ a\}$
69		ssun4	$⊢ X ∖ a \subseteq ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ ran f \cup ⋃ \{X ∖ a\}$
70		uniun	$⊢ ⋃ (ran f \cup \{X ∖ a\}) = ⋃ ran f \cup ⋃ \{X ∖ a\}$
71	69 70	sseqtrrdi	$⊢ X ∖ a \subseteq ⋃ \{X ∖ a\} \to X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
72	67 68 71	3syl	$⊢ X ∖ a \in J \to X ∖ a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
73		ssun3	$⊢ a \subseteq ⋃ ran f \to a \subseteq ⋃ ran f \cup ⋃ \{X ∖ a\}$
74	73 70	sseqtrrdi	$⊢ a \subseteq ⋃ ran f \to a \subseteq ⋃ (ran f \cup \{X ∖ a\})$
75		uncom	$⊢ a \cup (X ∖ a) = (X ∖ a) \cup a$
76		undif1	$⊢ (X ∖ a) \cup a = X \cup a$
77	75 76	eqtri	$⊢ a \cup (X ∖ a) = X \cup a$
78		ssequn2	$⊢ a \subseteq X \leftrightarrow X \cup a = X$
79	78	biimpi	$⊢ a \subseteq X \to X \cup a = X$
80	77 79	eqtrid	$⊢ a \subseteq X \to a \cup (X ∖ a) = X$
81	80	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$
82		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\})$
83		unidm	$⊢ ⋃ (ran f \cup \{X ∖ a\}) \cup ⋃ (ran f \cup \{X ∖ a\}) = ⋃ (ran f \cup \{X ∖ a\})$
84	82 83	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\})$
85	84	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\})$
86	81 85	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\})$
87	74 86	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\})$
88	72 87	sylanr2	$⊢ (a \subseteq X \land (a \subseteq ⋃ ran f \land X ∖ a \in J)) \to X \subseteq ⋃ (ran f \cup \{X ∖ a\})$
89	88	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\})$
90		f1f	$⊢ f : a \underset{1-1}{⟶} J \to f : a ⟶ J$
91		frn	$⊢ f : a ⟶ J \to ran f \subseteq J$
92	90 91	syl	$⊢ f : a \underset{1-1}{⟶} J \to ran f \subseteq J$
93	1	topopn	$⊢ J \in Top \to X \in J$
94	1	difopn	$⊢ (X \in J \land a \in Clsd (J)) \to X ∖ a \in J$
95	93 94	sylan	$⊢ (J \in Top \land a \in Clsd (J)) \to X ∖ a \in J$
96	95	snssd	$⊢ (J \in Top \land a \in Clsd (J)) \to \{X ∖ a\} \subseteq J$
97		unss12	$⊢ (ran f \subseteq J \land \{X ∖ a\} \subseteq J) \to ran f \cup \{X ∖ a\} \subseteq J \cup J$
98		unidm	$⊢ J \cup J = J$
99	97 98	sseqtrdi	$⊢ (ran f \subseteq J \land \{X ∖ a\} \subseteq J) \to ran f \cup \{X ∖ a\} \subseteq J$
100	92 96 99	syl2an	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to ran f \cup \{X ∖ a\} \subseteq J$
101		uniss	$⊢ ran f \cup \{X ∖ a\} \subseteq J \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq ⋃ J$
102	101 1	sseqtrrdi	$⊢ ran f \cup \{X ∖ a\} \subseteq J \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq X$
103	100 102	syl	$⊢ (f : a \underset{1-1}{⟶} J \land (J \in Top \land a \in Clsd (J))) \to ⋃ (ran f \cup \{X ∖ a\}) \subseteq X$
104	103	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$
105	89 104	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\})$
106	65 105	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\})$
107	63 106	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\})$
108	59 107	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\})$
109	108	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\})$
110	109	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\}))$
111	46 110	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\}))$
112	111	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\})$
113	112	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\})$
114	5 113	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\})$
115		vex	$⊢ f \in V$
116		f1f1orn	$⊢ f : a \underset{1-1}{⟶} J \to f : a \underset{1-1 onto}{⟶} ran f$
117		f1oen3g	$⊢ (f \in V \land f : a \underset{1-1 onto}{⟶} ran f) \to a \approx ran f$
118	115 116 117	sylancr	$⊢ f : a \underset{1-1}{⟶} J \to a \approx ran f$
119		enen1	$⊢ a \approx ran f \to (a \approx ω \leftrightarrow ran f \approx ω)$
120		endom	$⊢ ran f \approx ω \to ran f ≼ ω$
121		snfi	$⊢ \{X ∖ a\} \in Fin$
122		isfinite	$⊢ \{X ∖ a\} \in Fin \leftrightarrow \{X ∖ a\} ≺ ω$
123	121 122	mpbi	$⊢ \{X ∖ a\} ≺ ω$
124		sdomdom	$⊢ \{X ∖ a\} ≺ ω \to \{X ∖ a\} ≼ ω$
125	123 124	ax-mp	$⊢ \{X ∖ a\} ≼ ω$
126		unctb	$⊢ (ran f ≼ ω \land \{X ∖ a\} ≼ ω) \to (ran f \cup \{X ∖ a\}) ≼ ω$
127	120 125 126	sylancl	$⊢ ran f \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω$
128	119 127	biimtrdi	$⊢ a \approx ran f \to (a \approx ω \to (ran f \cup \{X ∖ a\}) ≼ ω)$
129	118 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	100	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	114 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		uniexg	$⊢ J \in Top \to ⋃ J \in V$
173	1 172	eqeltrid	$⊢ J \in Top \to X \in V$
174		difexg	$⊢ X \in V \to X ∖ a \in V$
175		unisng	$⊢ X ∖ a \in V \to ⋃ \{X ∖ a\} = X ∖ a$
176	173 174 175	3syl	$⊢ J \in Top \to ⋃ \{X ∖ a\} = X ∖ a$
177	176	ineq2d	$⊢ J \in Top \to a \cap ⋃ \{X ∖ a\} = a \cap (X ∖ a)$
178		disjdif	$⊢ a \cap (X ∖ a) = \emptyset$
179	177 178	eqtrdi	$⊢ J \in Top \to a \cap ⋃ \{X ∖ a\} = \emptyset$
180		inunissunidif	$⊢ a \cap ⋃ \{X ∖ a\} = \emptyset \to (a \subseteq ⋃ s \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
181	179 180	syl	$⊢ J \in Top \to (a \subseteq ⋃ s \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
182	171 181	sylan9bbr	$⊢ (J \in Top \land X = ⋃ s) \to (a \subseteq X \leftrightarrow a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
183	182	biimpd	$⊢ (J \in Top \land X = ⋃ s) \to (a \subseteq X \to a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
184	183	impancom	$⊢ (J \in Top \land a \subseteq X) \to (X = ⋃ s \to a \subseteq ⋃ (s ∖ \{X ∖ a\}))$
185	170 184	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\})))$
186	5 29 185	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\})))$
187	186	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\})))$
188	187	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\}))))$
189	118	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$
190		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$
191	55 190	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$
192		vex	$⊢ s \in V$
193		difss	$⊢ s ∖ \{X ∖ a\} \subseteq s$
194		ssdomg	$⊢ s \in V \to (s ∖ \{X ∖ a\} \subseteq s \to (s ∖ \{X ∖ a\}) ≼ s)$
195	192 193 194	mp2	$⊢ (s ∖ \{X ∖ a\}) ≼ s$
196	191 195	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$
197		endomtr	$⊢ (a \approx ran f \land ran f ≼ s) \to a ≼ s$
198	189 196 197	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$
199	188 198	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)$
200	199	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)$
201		elinel2	$⊢ s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \to s \in Fin$
202	201	adantr	$⊢ (s \in (𝒫 (ran f \cup \{X ∖ a\}) \cap Fin) \land X = ⋃ s) \to s \in Fin$
203	202	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)$
204	200 203	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))$
205	204	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))$
206	161 205	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))$
207	160 206	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)$
208	207	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))$
209	208	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))$
210	209	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))$
211	210	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))$
212	45 211	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)$
213	18 27 28 212	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)$
214	213	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)$
215		isfinite	$⊢ s \in Fin \leftrightarrow s ≺ ω$
216		domsdomtr	$⊢ (a ≼ s \land s ≺ ω) \to a ≺ ω$
217	215 216	sylan2b	$⊢ (a ≼ s \land s \in Fin) \to a ≺ ω$
218	217	exlimiv	$⊢ \exists s (a ≼ s \land s \in Fin) \to a ≺ ω$
219		sdomnen	$⊢ a ≺ ω \to \neg a \approx ω$
220	214 218 219	3syl	$⊢ ((J \in C \land a \approx ω) \land (a \subseteq X \land limPt (J) (a) = \emptyset)) \to \neg a \approx ω$
221	17 220	pm2.65da	$⊢ (J \in C \land a \approx ω) \to \neg (a \subseteq X \land limPt (J) (a) = \emptyset)$
222		imnan	$⊢ (a \subseteq X \to \neg limPt (J) (a) = \emptyset) \leftrightarrow \neg (a \subseteq X \land limPt (J) (a) = \emptyset)$
223	221 222	sylibr	$⊢ (J \in C \land a \approx ω) \to (a \subseteq X \to \neg limPt (J) (a) = \emptyset)$
224	223	imp	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \neg limPt (J) (a) = \emptyset$
225		neq0	$⊢ \neg limPt (J) (a) = \emptyset \leftrightarrow \exists s s \in limPt (J) (a)$
226	224 225	sylib	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \exists s s \in limPt (J) (a)$
227	1	lpss	$⊢ (J \in Top \land a \subseteq X) \to limPt (J) (a) \subseteq X$
228	5 227	sylan	$⊢ (J \in C \land a \subseteq X) \to limPt (J) (a) \subseteq X$
229	228	adantlr	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to limPt (J) (a) \subseteq X$
230	229	sseld	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to (s \in limPt (J) (a) \to s \in X)$
231	230	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)))$
232	231	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)))$
233		df-rex	$⊢ \exists s \in X s \in limPt (J) (a) \leftrightarrow \exists s (s \in X \land s \in limPt (J) (a))$
234	232 233	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))$
235	226 234	mpd	$⊢ ((J \in C \land a \approx ω) \land a \subseteq X) \to \exists s \in X s \in limPt (J) (a)$
236	16 235	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)$
237	1	lpss3	$⊢ (J \in Top \land b \subseteq X \land a \subseteq b) \to limPt (J) (a) \subseteq limPt (J) (b)$
238	237	3expb	$⊢ (J \in Top \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
239	5 238	sylan	$⊢ (J \in C \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
240	239	adantlr	$⊢ ((J \in C \land a \approx ω) \land (b \subseteq X \land a \subseteq b)) \to limPt (J) (a) \subseteq limPt (J) (b)$
241	240	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))$
242	241	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))$
243	236 242	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)$
244	243	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)$
245	244	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))$
246	245	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))$
247	246	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))$
248	14 247	mpd	$⊢ (J \in C \land (b \subseteq X \land \neg b \in Fin)) \to \exists s \in X s \in limPt (J) (b)$
249	8 248	sylan2b	$⊢ (J \in C \land (b \in 𝒫 X \land \neg b \in Fin)) \to \exists s \in X s \in limPt (J) (b)$
250	6 249	sylan2b	$⊢ (J \in C \land b \in (𝒫 X ∖ Fin)) \to \exists s \in X s \in limPt (J) (b)$
251	250	ralrimiva	$⊢ J \in C \to \forall b \in (𝒫 X ∖ Fin) \exists s \in X s \in limPt (J) (b)$
252		simpr	$⊢ (y = b \land z = s) \to z = s$
253		fveq2	$⊢ y = b \to limPt (J) (y) = limPt (J) (b)$
254	253	adantr	$⊢ (y = b \land z = s) \to limPt (J) (y) = limPt (J) (b)$
255	252 254	eleq12d	$⊢ (y = b \land z = s) \to (z \in limPt (J) (y) \leftrightarrow s \in limPt (J) (b))$
256	255	cbvrexdva	$⊢ y = b \to (\exists z \in X z \in limPt (J) (y) \leftrightarrow \exists s \in X s \in limPt (J) (b))$
257	256	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)$
258	251 257	sylibr	$⊢ J \in C \to \forall y \in (𝒫 X ∖ Fin) \exists z \in X z \in limPt (J) (y)$
259	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))$
260	5 258 259	sylanbrc	$⊢ J \in C \to J \in W$

Metamath Proof Explorer

Theorem pibt2

Proof