Theorem pibt2 38096

Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 38093 and pibp21 38094 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 38093	. . 3 ⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
4	3	simplbi 502	. 2 ⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ Top)
5		eldif 3916	. . . . 5 ⊢ (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6		velpw 4569	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝑋 ↔ 𝑏 ⊆ 𝑋)
7	6	anbi1i 636	. . . . . 6 ⊢ ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin))
8		vex 3461	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
9		infinf 10562	. . . . . . . . . 10 ⊢ (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
10	8, 9	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
11	8	infcntss 9285	. . . . . . . . 9 ⊢ (ω ≼ 𝑏 → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
12	10, 11	sylbi 220	. . . . . . . 8 ⊢ (¬ 𝑏 ∈ Fin → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
13	12	ad2antll 742	. . . . . . 7 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
14		sstr 3946	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) → 𝑎 ⊆ 𝑋)
15	14	ancoms 464	. . . . . . . . . . . . 13 ⊢ ((𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → 𝑎 ⊆ 𝑋)
16		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17		simpll 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω))
18		0ss 4357	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∅ ⊆ 𝑎
19		sseq1 3963	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
20	18, 19	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
21	20	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
22	1	cldlp 23337	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
23	22	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
24	21, 23	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
25	4, 24	sylanl1 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
26	25	adantllr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
28	1	cldss 23216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Clsd‘𝐽) → 𝑎 ⊆ 𝑋)
29	1	nlpineqsn 38087	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}))
30		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → (𝑛 ∩ 𝑎) = {𝑝})
31	30	reximi 3105	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝})
32	31	ralimi 3104	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝})
33		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
34		ineq1 4166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = (𝑓‘𝑝) → (𝑛 ∩ 𝑎) = ((𝑓‘𝑝) ∩ 𝑎))
35	34	eqeq1d 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑓‘𝑝) → ((𝑛 ∩ 𝑎) = {𝑝} ↔ ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
36	33, 35	ac6s 10479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
37		fvineqsnf1 38089	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎–1-1→𝐽)
38		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})
39	37, 38	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
40	39	eximi 1868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
41	29, 32, 36, 40	4syl 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
42	28, 41	syl3an2 1182	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
43	4, 42	syl3an1 1181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
44	43	3adant1r 1196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
45		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → 𝑓:𝑎–1-1→𝐽)
46		vsnid 4631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑝 ∈ {𝑝}
47		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
48	46, 47	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎))
49	48	elin1d 4157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓‘𝑝))
50	49	ralimi 3104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝))
51		ralssiun 38086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
52	50, 51	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
53	52	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
54		f1fn 6779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓 Fn 𝑎)
55		fniunfv 7247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓 Fn 𝑎 → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
56	54, 55	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓:𝑎–1-1→𝐽 → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
57	56	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
58	53, 57	sseqtrd 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ ran 𝑓)
59	1	cldopn 23218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑎) ∈ 𝐽)
60	59	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋 ∖ 𝑎) ∈ 𝐽)
61	60	anim1i 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → ((𝑋 ∖ 𝑎) ∈ 𝐽 ∧ 𝑎 ⊆ ∪ ran 𝑓))
62	61	ancomd 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))
63	28	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎 ⊆ 𝑋)
64	63	anim1i 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)))
65		unisng 4892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
66	65	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)})
67		eqimss 3996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)})
68		ssun4 4134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)}))
69		uniun 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) = (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)})
70	68, 69	sseqtrrdi 3979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
71	66, 67, 70	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
72		ssun3 4133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)}))
73	72, 69	sseqtrrdi 3979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
74		uncom 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = ((𝑋 ∖ 𝑎) ∪ 𝑎)
75		undif1 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑋 ∖ 𝑎) ∪ 𝑎) = (𝑋 ∪ 𝑎)
76	74, 75	eqtri 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = (𝑋 ∪ 𝑎)
77		ssequn2 4142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑎 ⊆ 𝑋 ↔ (𝑋 ∪ 𝑎) = 𝑋)
78	77	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑎 ⊆ 𝑋 → (𝑋 ∪ 𝑎) = 𝑋)
79	76, 78	eqtrid 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 ⊆ 𝑋 → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋)
80	79	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋)
81		unss12 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
82		unidm 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})
83	81, 82	sseqtrdi 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
84	83	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
85	80, 84	eqsstrrd 3973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
86	73, 85	sylanr1 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
87	71, 86	sylanr2 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
88	87	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
89		f1f 6778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎⟶𝐽)
90		frn 6717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑓:𝑎⟶𝐽 → ran 𝑓 ⊆ 𝐽)
91	89, 90	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓:𝑎–1-1→𝐽 → ran 𝑓 ⊆ 𝐽)
92	1	topopn 23093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
93	1	difopn 23221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑋 ∈ 𝐽 ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽)
94	92, 93	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽)
95	94	snssd 4754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋 ∖ 𝑎)} ⊆ 𝐽)
96		unss12 4141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((ran 𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ (𝐽 ∪ 𝐽))
97		unidm 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐽 ∪ 𝐽) = 𝐽
98	96, 97	sseqtrdi 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
99	91, 95, 98	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
100		uniss 4882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ ∪ 𝐽)
101	100, 1	sseqtrrdi 3979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
102	99, 101	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
103	102	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
104	88, 103	eqssd 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
105	64, 104	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
106	62, 105	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
107	58, 106	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
108	107	ancom1s 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
109	108	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
110	45, 109	mpand 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
111	110	impr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
112	111	adantlrr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
113	4, 112	sylanl1 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
114		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑓 ∈ V
115		f1f1orn 6836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎–1-1-onto→ran 𝑓)
116		f1oen3g 8965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 ∈ V ∧ 𝑓:𝑎–1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
117	114, 115, 116	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑎 ≈ ran 𝑓)
118		enen1 9108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
119		endom 8978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
120		snfi 9043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {(𝑋 ∖ 𝑎)} ∈ Fin
121		isfinite 9624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ({(𝑋 ∖ 𝑎)} ∈ Fin ↔ {(𝑋 ∖ 𝑎)} ≺ ω)
122	120, 121	mpbi 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {(𝑋 ∖ 𝑎)} ≺ ω
123		sdomdom 8979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({(𝑋 ∖ 𝑎)} ≺ ω → {(𝑋 ∖ 𝑎)} ≼ ω)
124	122, 123	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {(𝑋 ∖ 𝑎)} ≼ ω
125		unctb 10199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((ran 𝑓 ≼ ω ∧ {(𝑋 ∖ 𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
126	119, 124, 125	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
127	118, 126	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
128	117, 127	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑎–1-1→𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
129	128	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑎 ≈ ω ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
130	129	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
131	130	ad2ant2lr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
132	99	ancoms 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
133	132	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
134	133	adantlrr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
135	4, 134	sylanl1 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
136		elpw2g 5306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽))
137	136	biimprd 251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽))
138	137	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽))
139	135, 138	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽)
140	3	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
141		unieq 4885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑠 = 𝑧 → ∪ 𝑠 = ∪ 𝑧)
142	141	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 = 𝑧 → (𝑋 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑧))
143	142	cbvrexvw 3246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
144	143	imbi2i 339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
145	144	ralbii 3113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
146	140, 145	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠))
147		unieq 4885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ∪ 𝑦 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
148	147	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
149		breq1 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
150	148, 149	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) ↔ (𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)))
151		pweq 4578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
152	151	ineq1d 4172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin))
153	152	rexeqdv 3326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))
154	150, 153	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
155	154	rspccv 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
156	146, 155	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
157	156	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
158	139, 157	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))
159	113, 131, 158	mp2and 712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)
160		df-rex 3092	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠))
161		elinel1 4154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
162		velpw 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
163		ssdif 4098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}))
164		difun2 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}) = (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)})
165	163, 164	sseqtrdi 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)}))
166	165	difss2d 4093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
167	162, 166	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
168	161, 167	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓))
170		sseq2 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑋 = ∪ 𝑠 → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ 𝑠))
171		uniexg 7744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
172	1, 171	eqeltrid 2869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐽 ∈ Top → 𝑋 ∈ V)
173		difexg 5302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑎) ∈ V)
174		unisng 4892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑋 ∖ 𝑎) ∈ V → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
175	172, 173, 174	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐽 ∈ Top → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
176	175	ineq2d 4173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = (𝑎 ∩ (𝑋 ∖ 𝑎)))
177		disjdif 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 ∩ (𝑋 ∖ 𝑎)) = ∅
178	176, 177	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = ∅)
179		inunissunidif 38054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = ∅ → (𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
180	178, 179	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐽 ∈ Top → (𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
181	170, 180	sylan9bbr 520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠) → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
182	181	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠) → (𝑎 ⊆ 𝑋 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
183	182	impancom 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑋 = ∪ 𝑠 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
184	169, 183	anim12d 621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
185	4, 28, 184	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
186	185	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
187	186	anim2d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))))
188	117	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≈ ran 𝑓)
189		fvineqsneq 38091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓 Fn 𝑎 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓)
190	54, 189	sylanl1 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓)
191		vex 3461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑠 ∈ V
192		difss 4090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠
193		ssdomg 8999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 ∈ V → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠))
194	191, 192, 193	mp2 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠
195	190, 194	eqbrtrrdi 5153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → ran 𝑓 ≼ 𝑠)
196		endomtr 9011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝑠) → 𝑎 ≼ 𝑠)
197	188, 195, 196	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≼ 𝑠)
198	187, 197	syl6 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → 𝑎 ≼ 𝑠))
199	198	expdimp 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑎 ≼ 𝑠))
200		elinel2 4155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ Fin)
201	200	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin)
202	201	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin))
203	199, 202	jcad 522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → (𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
204	203	eximdv 1950	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
205	160, 204	biimtrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
206	159, 205	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
207	206	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
208	207	exlimdv 1966	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
209	208	anass1rs 668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
210	209	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
211	44, 210	mpd 16	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
212	17, 26, 27, 211	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
213	212	anasss 472	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
214		isfinite 9624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
215		domsdomtr 9103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ≺ ω) → 𝑎 ≺ ω)
216	214, 215	sylan2b 606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω)
217	216	exlimiv 1963	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω)
218		sdomnen 8980	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
219	213, 217, 218	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
220	16, 219	pm2.65da 829	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
221		imnan 405	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222	220, 221	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → (𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
223	222	imp 412	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
224		neq0 4306	. . . . . . . . . . . . . . 15 ⊢ (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
225	223, 224	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
226	1	lpss 23329	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
227	4, 226	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
228	227	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229	228	sseld 3937	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ 𝑋))
230	229	ancrd 561	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
231	230	eximdv 1950	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232		df-rex 3092	. . . . . . . . . . . . . . 15 ⊢ (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
233	231, 232	imbitrrdi 255	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234	225, 233	mpd 16	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
235	15, 234	sylan2 605	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
236	1	lpss3 23331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
237	236	3expb 1138	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
238	4, 237	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
239	238	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240	239	sseld 3937	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
241	240	reximdv 3182	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242	235, 241	mpd 16	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
243	242	an42s 674	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244	243	ex 418	. . . . . . . . 9 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → ((𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
245	244	exlimdv 1966	. . . . . . . 8 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246	245	adantrr 730	. . . . . . 7 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
247	13, 246	mpd 16	. . . . . 6 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
248	7, 247	sylan2b 606	. . . . 5 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
249	5, 248	sylan2b 606	. . . 4 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
250	249	ralrimiva 3159	. . 3 ⊢ (𝐽 ∈ 𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251		simpr 490	. . . . . 6 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → 𝑧 = 𝑠)
252		fveq2 6885	. . . . . . 7 ⊢ (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
253	252	adantr 486	. . . . . 6 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254	251, 253	eleq12d 2859	. . . . 5 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
255	254	cbvrexdva 3248	. . . 4 ⊢ (𝑦 = 𝑏 → (∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256	255	cbvralvw 3245	. . 3 ⊢ (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
257	250, 256	sylibr 237	. 2 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
258		pibt2.21	. . 3 ⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∖ Fin)∃𝑧 ∈ ∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
259	1, 258	pibp21 38094	. 2 ⊢ (𝐽 ∈ 𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
260	4, 257, 259	sylanbrc 595	1 ⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091  {crab 3418  Vcvv 3457   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  {csn 4591  ∪ cuni 4874  ∪ ciun 4958   class class class wbr 5111  ran crn 5664   Fn wfn 6535  ⟶wf 6536  –1-1→wf1 6537  –1-1-onto→wf1o 6539  ‘cfv 6540  ωcom 7864   ≈ cen 8942   ≼ cdom 8943   ≺ csdm 8944  Fincfn 8945  Topctop 23080  Clsdccld 23203  limPtclp 23321

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-reg 9557  ax-inf2 9613  ax-ac2 10458

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-2o 8456  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-oi 9475  df-r1 9739  df-rank 9740  df-scott 9861  df-dju 9899  df-card 9937  df-ac 10112  df-top 23081  df-cld 23206  df-ntr 23207  df-cls 23208  df-nei 23285  df-lp 23323

This theorem is used by: (None)