pibt2 - Mathbox for ML

	Mathbox for ML		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pibt2		Structured version Visualization version GIF version

Theorem pibt2 37461

Description: Theorem T000002 of pi-base, a countably compact topology is also weakly countably compact. See pibp19 37458 and pibp21 37459 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 37458	. . 3 ⊢ (𝐽 ∈ 𝐶 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
4	3	simplbi 497	. 2 ⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ Top)
5		eldif 3907	. . . . 5 ⊢ (𝑏 ∈ (𝒫 𝑋 ∖ Fin) ↔ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin))
6		velpw 4552	. . . . . . 7 ⊢ (𝑏 ∈ 𝒫 𝑋 ↔ 𝑏 ⊆ 𝑋)
7	6	anbi1i 624	. . . . . 6 ⊢ ((𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin) ↔ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin))
8		vex 3440	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
9		infinf 10457	. . . . . . . . . 10 ⊢ (𝑏 ∈ V → (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏))
10	8, 9	ax-mp 5	. . . . . . . . 9 ⊢ (¬ 𝑏 ∈ Fin ↔ ω ≼ 𝑏)
11	8	infcntss 9207	. . . . . . . . 9 ⊢ (ω ≼ 𝑏 → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
12	10, 11	sylbi 217	. . . . . . . 8 ⊢ (¬ 𝑏 ∈ Fin → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
13	12	ad2antll 729	. . . . . . 7 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω))
14		sstr 3938	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) → 𝑎 ⊆ 𝑋)
15	14	ancoms 458	. . . . . . . . . . . . 13 ⊢ ((𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → 𝑎 ⊆ 𝑋)
16		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → 𝑎 ≈ ω)
17		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω))
18		0ss 4347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∅ ⊆ 𝑎
19		sseq1 3955	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((limPt‘𝐽)‘𝑎) = ∅ → (((limPt‘𝐽)‘𝑎) ⊆ 𝑎 ↔ ∅ ⊆ 𝑎))
20	18, 19	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((limPt‘𝐽)‘𝑎) = ∅ → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
21	20	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑎)
22	1	cldlp 23065	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
23	22	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (𝑎 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑎) ⊆ 𝑎))
24	21, 23	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
25	4, 24	sylanl1 680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
26	25	adantllr 719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → 𝑎 ∈ (Clsd‘𝐽))
27		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ((limPt‘𝐽)‘𝑎) = ∅)
28	1	cldss 22944	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 ∈ (Clsd‘𝐽) → 𝑎 ⊆ 𝑋)
29	1	nlpineqsn 37452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}))
30		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → (𝑛 ∩ 𝑎) = {𝑝})
31	30	reximi 3070	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝})
32	31	ralimi 3069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑝 ∈ 𝑛 ∧ (𝑛 ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝})
33		vex 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
34		ineq1 4160	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = (𝑓‘𝑝) → (𝑛 ∩ 𝑎) = ((𝑓‘𝑝) ∩ 𝑎))
35	34	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑓‘𝑝) → ((𝑛 ∩ 𝑎) = {𝑝} ↔ ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
36	33, 35	ac6s 10375	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑝 ∈ 𝑎 ∃𝑛 ∈ 𝐽 (𝑛 ∩ 𝑎) = {𝑝} → ∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
37		fvineqsnf1 37454	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑓:𝑎–1-1→𝐽)
38		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})
39	37, 38	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
40	39	eximi 1836	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑓(𝑓:𝑎⟶𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
41	29, 32, 36, 40	4syl 19	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
42	28, 41	syl3an2 1164	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
43	4, 42	syl3an1 1163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
44	43	3adant1r 1178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}))
45		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → 𝑓:𝑎–1-1→𝐽)
46		vsnid 4613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ 𝑝 ∈ {𝑝}
47		eleq2 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → (𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎) ↔ 𝑝 ∈ {𝑝}))
48	46, 47	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ ((𝑓‘𝑝) ∩ 𝑎))
49	48	elin1d 4151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑝 ∈ (𝑓‘𝑝))
50	49	ralimi 3069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → ∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝))
51		ralssiun 37451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (∀𝑝 ∈ 𝑎 𝑝 ∈ (𝑓‘𝑝) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
52	50, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
53	52	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝))
54		f1fn 6720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓 Fn 𝑎)
55		fniunfv 7181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑓 Fn 𝑎 → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑓:𝑎–1-1→𝐽 → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
57	56	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∪ 𝑝 ∈ 𝑎 (𝑓‘𝑝) = ∪ ran 𝑓)
58	53, 57	sseqtrd 3966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑎 ⊆ ∪ ran 𝑓)
59	1	cldopn 22946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑎) ∈ 𝐽)
60	59	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (𝑋 ∖ 𝑎) ∈ 𝐽)
61	60	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → ((𝑋 ∖ 𝑎) ∈ 𝐽 ∧ 𝑎 ⊆ ∪ ran 𝑓))
62	61	ancomd 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))
63	28	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → 𝑎 ⊆ 𝑋)
64	63	anim1i 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)))
65		unisng 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
66	65	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)})
67		eqimss 3988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) = ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)})
68		ssun4 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)}))
69		uniun 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) = (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)})
70	68, 69	sseqtrrdi 3971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑋 ∖ 𝑎) ⊆ ∪ {(𝑋 ∖ 𝑎)} → (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
71	66, 67, 70	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑋 ∖ 𝑎) ∈ 𝐽 → (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
72		ssun3 4127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ (∪ ran 𝑓 ∪ ∪ {(𝑋 ∖ 𝑎)}))
73	72, 69	sseqtrrdi 3971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 ⊆ ∪ ran 𝑓 → 𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
74		uncom 4105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = ((𝑋 ∖ 𝑎) ∪ 𝑎)
75		undif1 4423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑋 ∖ 𝑎) ∪ 𝑎) = (𝑋 ∪ 𝑎)
76	74, 75	eqtri 2754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑎 ∪ (𝑋 ∖ 𝑎)) = (𝑋 ∪ 𝑎)
77		ssequn2 4136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑎 ⊆ 𝑋 ↔ (𝑋 ∪ 𝑎) = 𝑋)
78	77	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑎 ⊆ 𝑋 → (𝑋 ∪ 𝑎) = 𝑋)
79	76, 78	eqtrid 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑎 ⊆ 𝑋 → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) = 𝑋)
81		unss12 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
82		unidm 4104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∪ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})
83	81, 82	sseqtrdi 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
84	83	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → (𝑎 ∪ (𝑋 ∖ 𝑎)) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
85	80, 84	eqsstrrd 3965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
86	73, 85	sylanr1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
87	71, 86	sylanr2 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
88	87	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 ⊆ ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
89		f1f 6719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎⟶𝐽)
90		frn 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑓:𝑎⟶𝐽 → ran 𝑓 ⊆ 𝐽)
91	89, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓:𝑎–1-1→𝐽 → ran 𝑓 ⊆ 𝐽)
92	1	topopn 22821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
93	1	difopn 22949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑋 ∈ 𝐽 ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽)
94	92, 93	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → (𝑋 ∖ 𝑎) ∈ 𝐽)
95	94	snssd 4758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) → {(𝑋 ∖ 𝑎)} ⊆ 𝐽)
96		unss12 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((ran 𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ (𝐽 ∪ 𝐽))
97		unidm 4104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐽 ∪ 𝐽) = 𝐽
98	96, 97	sseqtrdi 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ⊆ 𝐽 ∧ {(𝑋 ∖ 𝑎)} ⊆ 𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
99	91, 95, 98	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
100		uniss 4864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ ∪ 𝐽)
101	100, 1	sseqtrrdi 3971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
102	99, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
103	102	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝑋)
104	88, 103	eqssd 3947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ 𝑋 ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽))) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
105	64, 104	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑎 ⊆ ∪ ran 𝑓 ∧ (𝑋 ∖ 𝑎) ∈ 𝐽)) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
106	62, 105	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ 𝑎 ⊆ ∪ ran 𝑓) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
107	58, 106	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ (𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽))) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
108	107	ancom1s 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
109	108	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
110	45, 109	mpand 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝} → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
111	110	impr 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
112	111	adantlrr 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
113	4, 112	sylanl1 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
114		vex 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑓 ∈ V
115		f1f1orn 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑓:𝑎–1-1-onto→ran 𝑓)
116		f1oen3g 8889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 ∈ V ∧ 𝑓:𝑎–1-1-onto→ran 𝑓) → 𝑎 ≈ ran 𝑓)
117	114, 115, 116	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓:𝑎–1-1→𝐽 → 𝑎 ≈ ran 𝑓)
118		enen1 9030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω ↔ ran 𝑓 ≈ ω))
119		endom 8901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ran 𝑓 ≈ ω → ran 𝑓 ≼ ω)
120		snfi 8965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ {(𝑋 ∖ 𝑎)} ∈ Fin
121		isfinite 9542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ({(𝑋 ∖ 𝑎)} ∈ Fin ↔ {(𝑋 ∖ 𝑎)} ≺ ω)
122	120, 121	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ {(𝑋 ∖ 𝑎)} ≺ ω
123		sdomdom 8902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({(𝑋 ∖ 𝑎)} ≺ ω → {(𝑋 ∖ 𝑎)} ≼ ω)
124	122, 123	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {(𝑋 ∖ 𝑎)} ≼ ω
125		unctb 10095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((ran 𝑓 ≼ ω ∧ {(𝑋 ∖ 𝑎)} ≼ ω) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
126	119, 124, 125	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ran 𝑓 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
127	118, 126	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 ≈ ran 𝑓 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
128	117, 127	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓:𝑎–1-1→𝐽 → (𝑎 ≈ ω → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
129	128	impcom 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑎 ≈ ω ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
130	129	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
131	130	ad2ant2lr 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)
132	99	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ 𝑓:𝑎–1-1→𝐽) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
133	132	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐽 ∈ Top ∧ 𝑎 ∈ (Clsd‘𝐽)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
134	133	adantlrr 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐽 ∈ Top ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
135	4, 134	sylanl1 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽)
136		elpw2g 5269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽))
137	136	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽))
138	137	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ⊆ 𝐽 → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽))
139	135, 138	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽)
140	3	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
141		unieq 4867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑠 = 𝑧 → ∪ 𝑠 = ∪ 𝑧)
142	141	eqeq2d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 = 𝑧 → (𝑋 = ∪ 𝑠 ↔ 𝑋 = ∪ 𝑧))
143	142	cbvrexvw 3211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
144	143	imbi2i 336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
145	144	ralbii 3078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
146	140, 145	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠))
147		unieq 4867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ∪ 𝑦 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
148	147	eqeq2d 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)})))
149		breq1 5092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑦 ≼ ω ↔ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω))
150	148, 149	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → ((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) ↔ (𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω)))
151		pweq 4561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → 𝒫 𝑦 = 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
152	151	ineq1d 4166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝒫 𝑦 ∩ Fin) = (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin))
153	152	rexeqdv 3293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))
154	150, 153	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) ↔ ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
155	154	rspccv 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀𝑦 ∈ 𝒫 𝐽((𝑋 = ∪ 𝑦 ∧ 𝑦 ≼ ω) → ∃𝑠 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑠) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
156	146, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ 𝐶 → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
157	156	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∈ 𝒫 𝐽 → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)))
158	139, 157	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑋 = ∪ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∧ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ≼ ω) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠))
159	113, 131, 158	mp2and 699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠)
160		df-rex 3057	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 ↔ ∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠))
161		elinel1 4148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
162		velpw 4552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ↔ 𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}))
163		ssdif 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}))
164		difun2 4428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∖ {(𝑋 ∖ 𝑎)}) = (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)})
165	163, 164	sseqtrdi 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ (ran 𝑓 ∖ {(𝑋 ∖ 𝑎)}))
166	165	difss2d 4086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑠 ⊆ (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
167	162, 166	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑠 ∈ 𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
168	161, 167	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓)
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓))
170		sseq2 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑋 = ∪ 𝑠 → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ 𝑠))
171		uniexg 7673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V)
172	1, 171	eqeltrid 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝐽 ∈ Top → 𝑋 ∈ V)
173		difexg 5265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑋 ∈ V → (𝑋 ∖ 𝑎) ∈ V)
174		unisng 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑋 ∖ 𝑎) ∈ V → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
175	172, 173, 174	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝐽 ∈ Top → ∪ {(𝑋 ∖ 𝑎)} = (𝑋 ∖ 𝑎))
176	175	ineq2d 4167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = (𝑎 ∩ (𝑋 ∖ 𝑎)))
177		disjdif 4419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑎 ∩ (𝑋 ∖ 𝑎)) = ∅
178	176, 177	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐽 ∈ Top → (𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = ∅)
179		inunissunidif 37419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑎 ∩ ∪ {(𝑋 ∖ 𝑎)}) = ∅ → (𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
180	178, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝐽 ∈ Top → (𝑎 ⊆ ∪ 𝑠 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
181	170, 180	sylan9bbr 510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠) → (𝑎 ⊆ 𝑋 ↔ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
182	181	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑠) → (𝑎 ⊆ 𝑋 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
183	182	impancom 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → (𝑋 = ∪ 𝑠 → 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))
184	169, 183	anim12d 609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
185	4, 28, 184	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ∈ (Clsd‘𝐽)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
186	185	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))))
187	186	anim2d 612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)})))))
188	117	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≈ ran 𝑓)
189		fvineqsneq 37456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑓 Fn 𝑎 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓)
190	54, 189	sylanl1 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) = ran 𝑓)
191		vex 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑠 ∈ V
192		difss 4083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠
193		ssdomg 8922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑠 ∈ V → ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ 𝑠 → (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠))
194	191, 192, 193	mp2 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑠 ∖ {(𝑋 ∖ 𝑎)}) ≼ 𝑠
195	190, 194	eqbrtrrdi 5129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → ran 𝑓 ≼ 𝑠)
196		endomtr 8934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑎 ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝑠) → 𝑎 ≼ 𝑠)
197	188, 195, 196	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ ((𝑠 ∖ {(𝑋 ∖ 𝑎)}) ⊆ ran 𝑓 ∧ 𝑎 ⊆ ∪ (𝑠 ∖ {(𝑋 ∖ 𝑎)}))) → 𝑎 ≼ 𝑠)
198	187, 197	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) ∧ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠)) → 𝑎 ≼ 𝑠))
199	198	expdimp 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑎 ≼ 𝑠))
200		elinel2 4149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) → 𝑠 ∈ Fin)
201	200	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin)
202	201	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → 𝑠 ∈ Fin))
203	199, 202	jcad 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ((𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → (𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
204	203	eximdv 1918	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠(𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin) ∧ 𝑋 = ∪ 𝑠) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
205	160, 204	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → (∃𝑠 ∈ (𝒫 (ran 𝑓 ∪ {(𝑋 ∖ 𝑎)}) ∩ Fin)𝑋 = ∪ 𝑠 → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
206	159, 205	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) ∧ (𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝})) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
207	206	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → ((𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
208	207	exlimdv 1934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑎 ∈ (Clsd‘𝐽) ∧ 𝑎 ≈ ω)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
209	208	anass1rs 655	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽)) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
210	209	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → (∃𝑓(𝑓:𝑎–1-1→𝐽 ∧ ∀𝑝 ∈ 𝑎 ((𝑓‘𝑝) ∩ 𝑎) = {𝑝}) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin)))
211	44, 210	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ∈ (Clsd‘𝐽) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
212	17, 26, 27, 211	syl3anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) ∧ ((limPt‘𝐽)‘𝑎) = ∅) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
213	212	anasss 466	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin))
214		isfinite 9542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ Fin ↔ 𝑠 ≺ ω)
215		domsdomtr 9025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ≺ ω) → 𝑎 ≺ ω)
216	214, 215	sylan2b 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω)
217	216	exlimiv 1931	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑠(𝑎 ≼ 𝑠 ∧ 𝑠 ∈ Fin) → 𝑎 ≺ ω)
218		sdomnen 8903	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ≺ ω → ¬ 𝑎 ≈ ω)
219	213, 217, 218	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅)) → ¬ 𝑎 ≈ ω)
220	16, 219	pm2.65da 816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
221		imnan 399	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅) ↔ ¬ (𝑎 ⊆ 𝑋 ∧ ((limPt‘𝐽)‘𝑎) = ∅))
222	220, 221	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) → (𝑎 ⊆ 𝑋 → ¬ ((limPt‘𝐽)‘𝑎) = ∅))
223	222	imp 406	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ¬ ((limPt‘𝐽)‘𝑎) = ∅)
224		neq0 4299	. . . . . . . . . . . . . . 15 ⊢ (¬ ((limPt‘𝐽)‘𝑎) = ∅ ↔ ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
225	223, 224	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
226	1	lpss 23057	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Top ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
227	4, 226	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
228	227	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑎) ⊆ 𝑋)
229	228	sseld 3928	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ 𝑋))
230	229	ancrd 551	. . . . . . . . . . . . . . . 16 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → (𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
231	230	eximdv 1918	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎))))
232		df-rex 3057	. . . . . . . . . . . . . . 15 ⊢ (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) ↔ ∃𝑠(𝑠 ∈ 𝑋 ∧ 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
233	231, 232	imbitrrdi 252	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎)))
234	225, 233	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ 𝑎 ⊆ 𝑋) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
235	15, 234	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎))
236	1	lpss3 23059	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
237	236	3expb 1120	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
238	4, 237	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
239	238	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ((limPt‘𝐽)‘𝑎) ⊆ ((limPt‘𝐽)‘𝑏))
240	239	sseld 3928	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (𝑠 ∈ ((limPt‘𝐽)‘𝑎) → 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
241	240	reximdv 3147	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → (∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑎) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
242	235, 241	mpd 15	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑎 ≈ ω) ∧ (𝑏 ⊆ 𝑋 ∧ 𝑎 ⊆ 𝑏)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
243	242	an42s 661	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
244	243	ex 412	. . . . . . . . 9 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → ((𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
245	244	exlimdv 1934	. . . . . . . 8 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ⊆ 𝑋) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
246	245	adantrr 717	. . . . . . 7 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → (∃𝑎(𝑎 ⊆ 𝑏 ∧ 𝑎 ≈ ω) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
247	13, 246	mpd 15	. . . . . 6 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ⊆ 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
248	7, 247	sylan2b 594	. . . . 5 ⊢ ((𝐽 ∈ 𝐶 ∧ (𝑏 ∈ 𝒫 𝑋 ∧ ¬ 𝑏 ∈ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
249	5, 248	sylan2b 594	. . . 4 ⊢ ((𝐽 ∈ 𝐶 ∧ 𝑏 ∈ (𝒫 𝑋 ∖ Fin)) → ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
250	249	ralrimiva 3124	. . 3 ⊢ (𝐽 ∈ 𝐶 → ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
251		simpr 484	. . . . . 6 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → 𝑧 = 𝑠)
252		fveq2 6822	. . . . . . 7 ⊢ (𝑦 = 𝑏 → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
253	252	adantr 480	. . . . . 6 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → ((limPt‘𝐽)‘𝑦) = ((limPt‘𝐽)‘𝑏))
254	251, 253	eleq12d 2825	. . . . 5 ⊢ ((𝑦 = 𝑏 ∧ 𝑧 = 𝑠) → (𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
255	254	cbvrexdva 3213	. . . 4 ⊢ (𝑦 = 𝑏 → (∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏)))
256	255	cbvralvw 3210	. . 3 ⊢ (∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦) ↔ ∀𝑏 ∈ (𝒫 𝑋 ∖ Fin)∃𝑠 ∈ 𝑋 𝑠 ∈ ((limPt‘𝐽)‘𝑏))
257	250, 256	sylibr 234	. 2 ⊢ (𝐽 ∈ 𝐶 → ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦))
258		pibt2.21	. . 3 ⊢ 𝑊 = {𝑥 ∈ Top ∣ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∖ Fin)∃𝑧 ∈ ∪ 𝑥𝑧 ∈ ((limPt‘𝑥)‘𝑦)}
259	1, 258	pibp21 37459	. 2 ⊢ (𝐽 ∈ 𝑊 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ (𝒫 𝑋 ∖ Fin)∃𝑧 ∈ 𝑋 𝑧 ∈ ((limPt‘𝐽)‘𝑦)))
260	4, 257, 259	sylanbrc 583	1 ⊢ (𝐽 ∈ 𝐶 → 𝐽 ∈ 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 {crab 3395 Vcvv 3436 ∖ cdif 3894 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 𝒫 cpw 4547 {csn 4573 ∪ cuni 4856 ∪ ciun 4939 class class class wbr 5089 ran crn 5615 Fn wfn 6476 ⟶wf 6477 –1-1→wf1 6478 –1-1-onto→wf1o 6480 ‘cfv 6481 ωcom 7796 ≈ cen 8866 ≼ cdom 8867 ≺ csdm 8868 Fincfn 8869 Topctop 22808 Clsdccld 22931 limPtclp 23049

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-reg 9478 ax-inf2 9531 ax-ac2 10354

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-iin 4942 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-oi 9396 df-r1 9657 df-rank 9658 df-dju 9794 df-card 9832 df-ac 10007 df-top 22809 df-cld 22934 df-ntr 22935 df-cls 22936 df-nei 23013 df-lp 23051

This theorem is referenced by: (None)

W3C validator