Theorem pibt2 36298

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

Hypotheses

Ref	Expression
pibt2.x	⊢ 𝑋 = ∪ 𝐽
pibt2.19	⊢ 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥((∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
pibt2.21	⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∖ Fin)∃𝑧 ∈ ∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}

Assertion

Ref	Expression
pibt2	⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊)

Distinct variable groups:   𝑦,𝐽,𝑥,𝑧   𝑦,𝑋,𝑥,𝑧

Allowed substitution hints:   𝐶(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)

Proof of Theorem pibt2

Dummy variables 𝑎 𝑏 𝑠 𝑓 𝑛 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		pibt2.x	. . . 4 ⊢ 𝑋 = ∪ 𝐽
2		pibt2.19	. . . 4 ⊢ 𝐶 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥((∪ 𝑥 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
3	1, 2	pibp19 36295	. . 3 ⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
4	3	simplbi 499	. 2 ⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ Top)
5		eldif 3959	. . . . 5 ⊢ (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6		velpw 4608	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝑋 ↔ 𝑏 ⊆ 𝑋)
7	6	anbi1i 625	. . . . . 6 ⊢ ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin))
8		vex 3479	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
9		infinf 10561	. . . . . . . . . 10 ⊢ (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
10	8, 9	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
11	8	infcntss 9321	. . . . . . . . 9 ⊢ (ω ≼ 𝑏 → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
12	10, 11	sylbi 216	. . . . . . . 8 ⊢ (¬ 𝑏 ∈ Fin → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
13	12	ad2antll 728	. . . . . . 7 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
14		sstr 3991	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) → 𝑎 ⊆ 𝑋)
15	14	ancoms 460	. . . . . . . . . . . . 13 ⊢ ((𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → 𝑎 ⊆ 𝑋)
16		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω))
18		0ss 4397	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∅ ⊆ 𝑎
19		sseq1 4008	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
20	18, 19	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
21	20	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
22	1	cldlp 22654	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
23	22	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
24	21, 23	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
25	4, 24	sylanl1 679	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
26	25	adantllr 718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27		simpr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
28	1	cldss 22533	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Clsd‘𝐽) → 𝑎 ⊆ 𝑋)
29	1	nlpineqsn 36289	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}))
30		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → (𝑛 ∩ 𝑎) = {𝑝})
31	30	reximi 3085	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝})
32	31	ralimi 3084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝})
33		vex 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 𝑎 ∈ V
34		ineq1 4206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = (𝑓‘𝑝) → (𝑛 ∩ 𝑎) = ((𝑓‘𝑝) ∩ 𝑎))
35	34	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = (𝑓‘𝑝) → ((𝑛 ∩ 𝑎) = {𝑝} ↔ ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
36	33, 35	ac6s 10479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
37	29, 32, 36	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
38		fvineqsnf1 36291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎–1-1→𝐽)
39		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})
40	38, 39	jca 513	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
41	40	eximi 1838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
42	37, 41	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
43	28, 42	syl3an2 1165	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
44	4, 43	syl3an1 1164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
45	44	3adant1r 1178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
46		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → 𝑓:𝑎–1-1→𝐽)
47		vsnid 4666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑝 ∈ {𝑝}
48		eleq2 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
49	47, 48	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎))
50	49	elin1d 4199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓‘𝑝))
51	50	ralimi 3084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝))
52		ralssiun 36288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
53	51, 52	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
54	53	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
55		f1fn 6789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓 Fn 𝑎)
56		fniunfv 7246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓 Fn 𝑎 → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓:𝑎–1-1→𝐽 → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
58	57	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
59	54, 58	sseqtrd 4023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ ran 𝑓)
60	1	cldopn 22535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑎) ∈ 𝐽)
61	60	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋 ∖ 𝑎) ∈ 𝐽)
62	61	anim1i 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → ((𝑋 ∖ 𝑎) ∈ 𝐽 ∧ 𝑎 ⊆ ∪ ran 𝑓))
63	62	ancomd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))
64	28	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎 ⊆ 𝑋)
65	64	anim1i 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)))
66		unisng 4930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
67	66	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)})
68		eqimss 4041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)})
69		ssun4 4176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)}))
70		uniun 4935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) = (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)})
71	69, 70	sseqtrrdi 4034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
72	67, 68, 71	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
73		ssun3 4175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)}))
74	73, 70	sseqtrrdi 4034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
75		uncom 4154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = ((𝑋 ∖ 𝑎) ∪ 𝑎)
76		undif1 4476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑋 ∖ 𝑎) ∪ 𝑎) = (𝑋 ∪ 𝑎)
77	75, 76	eqtri 2761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = (𝑋 ∪ 𝑎)
78		ssequn2 4184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑎 ⊆ 𝑋 ↔ (𝑋 ∪ 𝑎) = 𝑋)
79	78	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑎 ⊆ 𝑋 → (𝑋 ∪ 𝑎) = 𝑋)
80	77, 79	eqtrid 2785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 ⊆ 𝑋 → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋)
81	80	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋)
82		unss12 4183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
83		unidm 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})
84	82, 83	sseqtrdi 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
85	84	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
86	81, 85	eqsstrrd 4022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
87	74, 86	sylanr1 681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
88	72, 87	sylanr2 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
89	88	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
90		f1f 6788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎⟶𝐽)
91		frn 6725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑓:𝑎⟶𝐽 → ran 𝑓 ⊆ 𝐽)
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓:𝑎–1-1→𝐽 → ran 𝑓 ⊆ 𝐽)
93	1	topopn 22408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
94	1	difopn 22538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑋 ∈ 𝐽 ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽)
95	93, 94	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽)
96	95	snssd 4813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋 ∖ 𝑎)} ⊆ 𝐽)
97		unss12 4183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((ran 𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ (𝐽 ∪ 𝐽))
98		unidm 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐽 ∪ 𝐽) = 𝐽
99	97, 98	sseqtrdi 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
100	92, 96, 99	syl2an 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
101		uniss 4917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ ∪ 𝐽)
102	101, 1	sseqtrrdi 4034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
103	100, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
104	103	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
105	89, 104	eqssd 4000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
106	65, 105	syldan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
107	63, 106	syldan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
108	59, 107	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
109	108	ancom1s 652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
110	109	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
111	46, 110	mpand 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
112	111	impr 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
113	112	adantlrr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
114	4, 113	sylanl1 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
115		vex 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑓 ∈ V
116		f1f1orn 6845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎–1-1-onto→ran 𝑓)
117		f1oen3g 8962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 ∈ V ∧ 𝑓:𝑎–1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
118	115, 116, 117	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑎 ≈ ran 𝑓)
119		enen1 9117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
120		endom 8975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
121		snfi 9044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {(𝑋 ∖ 𝑎)} ∈ Fin
122		isfinite 9647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ({(𝑋 ∖ 𝑎)} ∈ Fin ↔ {(𝑋 ∖ 𝑎)} ≺ ω)
123	121, 122	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {(𝑋 ∖ 𝑎)} ≺ ω
124		sdomdom 8976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({(𝑋 ∖ 𝑎)} ≺ ω → {(𝑋 ∖ 𝑎)} ≼ ω)
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {(𝑋 ∖ 𝑎)} ≼ ω
126		unctb 10200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((ran 𝑓 ≼ ω ∧ {(𝑋 ∖ 𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
127	120, 125, 126	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
128	119, 127	syl6bi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
129	118, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑎–1-1→𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
130	129	impcom 409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑎 ≈ ω ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
131	130	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
132	131	ad2ant2lr 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
133	100	ancoms 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
134	133	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
135	134	adantlrr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
136	4, 135	sylanl1 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
137		elpw2g 5345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽))
138	137	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽))
139	138	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽))
140	136, 139	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽)
141	3	simprbi 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
142		unieq 4920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑠 = 𝑧 → ∪ 𝑠 = ∪ 𝑧)
143	142	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 = 𝑧 → (𝑋 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑧))
144	143	cbvrexvw 3236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
145	144	imbi2i 336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
146	145	ralbii 3094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
147	141, 146	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠))
148		unieq 4920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ∪ 𝑦 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
149	148	eqeq2d 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
150		breq1 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
151	149, 150	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) ↔ (𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)))
152		pweq 4617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
153	152	ineq1d 4212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin))
154	153	rexeqdv 3327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))
155	151, 154	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
156	155	rspccv 3610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
157	147, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
158	157	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
159	140, 158	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))
160	114, 132, 159	mp2and 698	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)
161		df-rex 3072	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠))
162		elinel1 4196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
163		velpw 4608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
164		ssdif 4140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}))
165		difun2 4481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}) = (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)})
166	164, 165	sseqtrdi 4033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)}))
167	166	difss2d 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
168	163, 167	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
169	162, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓))
171		sseq2 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑋 = ∪ 𝑠 → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ 𝑠))
172		uniexg 7730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
173	1, 172	eqeltrid 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐽 ∈ Top → 𝑋 ∈ V)
174		difexg 5328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑎) ∈ V)
175		unisng 4930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑋 ∖ 𝑎) ∈ V → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
176	173, 174, 175	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐽 ∈ Top → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
177	176	ineq2d 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = (𝑎 ∩ (𝑋 ∖ 𝑎)))
178		disjdif 4472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 ∩ (𝑋 ∖ 𝑎)) = ∅
179	177, 178	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = ∅)
180		inunissunidif 36256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = ∅ → (𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
181	179, 180	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐽 ∈ Top → (𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
182	171, 181	sylan9bbr 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠) → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
183	182	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠) → (𝑎 ⊆ 𝑋 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
184	183	impancom 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑋 = ∪ 𝑠 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
185	170, 184	anim12d 610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
186	4, 28, 185	syl2an 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
187	186	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
188	187	anim2d 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))))
189	118	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≈ ran 𝑓)
190		fvineqsneq 36293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓 Fn 𝑎 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓)
191	55, 190	sylanl1 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓)
192		vex 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑠 ∈ V
193		difss 4132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠
194		ssdomg 8996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 ∈ V → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠))
195	192, 193, 194	mp2 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠
196	191, 195	eqbrtrrdi 5189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → ran 𝑓 ≼ 𝑠)
197		endomtr 9008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝑠) → 𝑎 ≼ 𝑠)
198	189, 196, 197	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≼ 𝑠)
199	188, 198	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → 𝑎 ≼ 𝑠))
200	199	expdimp 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑎 ≼ 𝑠))
201		elinel2 4197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ Fin)
202	201	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin)
203	202	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin))
204	200, 203	jcad 514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → (𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
205	204	eximdv 1921	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
206	161, 205	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
207	160, 206	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
208	207	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
209	208	exlimdv 1937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
210	209	anass1rs 654	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
211	210	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
212	45, 211	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
213	17, 26, 27, 212	syl3anc 1372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
214	213	anasss 468	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
215		isfinite 9647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
216		domsdomtr 9112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ≺ ω) → 𝑎 ≺ ω)
217	215, 216	sylan2b 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω)
218	217	exlimiv 1934	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω)
219		sdomnen 8977	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
220	214, 218, 219	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
221	16, 220	pm2.65da 816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222		imnan 401	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
223	221, 222	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → (𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
224	223	imp 408	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
225		neq0 4346	. . . . . . . . . . . . . . 15 ⊢ (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
226	224, 225	sylib 217	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
227	1	lpss 22646	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
228	4, 227	sylan 581	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229	228	adantlr 714	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
230	229	sseld 3982	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ 𝑋))
231	230	ancrd 553	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232	231	eximdv 1921	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
233		df-rex 3072	. . . . . . . . . . . . . . 15 ⊢ (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234	232, 233	syl6ibr 252	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
235	226, 234	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
236	15, 235	sylan2 594	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
237	1	lpss3 22648	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
238	237	3expb 1121	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
239	4, 238	sylan 581	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240	239	adantlr 714	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
241	240	sseld 3982	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242	241	reximdv 3171	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
243	236, 242	mpd 15	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244	243	an42s 660	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
245	244	ex 414	. . . . . . . . 9 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → ((𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246	245	exlimdv 1937	. . . . . . . 8 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
247	246	adantrr 716	. . . . . . 7 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
248	13, 247	mpd 15	. . . . . 6 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
249	7, 248	sylan2b 595	. . . . 5 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
250	5, 249	sylan2b 595	. . . 4 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251	250	ralrimiva 3147	. . 3 ⊢ (𝐽 ∈ 𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
252		simpr 486	. . . . . 6 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → 𝑧 = 𝑠)
253		fveq2 6892	. . . . . . 7 ⊢ (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254	253	adantr 482	. . . . . 6 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
255	252, 254	eleq12d 2828	. . . . 5 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256	255	cbvrexdva 3238	. . . 4 ⊢ (𝑦 = 𝑏 → (∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
257	256	cbvralvw 3235	. . 3 ⊢ (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
258	251, 257	sylibr 233	. 2 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
259		pibt2.21	. . 3 ⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∖ Fin)∃𝑧 ∈ ∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
260	1, 259	pibp21 36296	. 2 ⊢ (𝐽 ∈ 𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
261	4, 258, 260	sylanbrc 584	1 ⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071  {crab 3433  Vcvv 3475   ∖ cdif 3946   ∪ cun 3947   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323  𝒫 cpw 4603  {csn 4629  ∪ cuni 4909  ∪ ciun 4998   class class class wbr 5149  ran crn 5678   Fn wfn 6539  ⟶wf 6540  –1-1→wf1 6541  –1-1-onto→wf1o 6543  ‘cfv 6544  ωcom 7855   ≈ cen 8936   ≼ cdom 8937   ≺ csdm 8938  Fincfn 8939  Topctop 22395  Clsdccld 22520  limPtclp 22638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-reg 9587  ax-inf2 9636  ax-ac2 10458

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-oi 9505  df-r1 9759  df-rank 9760  df-dju 9896  df-card 9934  df-ac 10111  df-top 22396  df-cld 22523  df-ntr 22524  df-cls 22525  df-nei 22602  df-lp 22640

This theorem is referenced by: (None)