# Metamath Proof Explorer

## Theorem 1stcelcls

Description: A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of Kreyszig p. 30. This proof uses countable choice ax-cc . A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis 1stcelcls.1 ${⊢}{X}=\bigcup {J}$
Assertion 1stcelcls

### Proof

Step Hyp Ref Expression
1 1stcelcls.1 ${⊢}{X}=\bigcup {J}$
2 simpll ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {J}\in {1}^{st}𝜔$
3 1stctop ${⊢}{J}\in {1}^{st}𝜔\to {J}\in \mathrm{Top}$
4 1 clsss3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}$
5 3 4 sylan ${⊢}\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}$
6 5 sselda ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {P}\in {X}$
7 1 1stcfb ${⊢}\left({J}\in {1}^{st}𝜔\wedge {P}\in {X}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)$
8 2 6 7 syl2anc ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)$
9 simpr2 ${⊢}\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)$
10 simpl ${⊢}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\to {P}\in {g}\left({k}\right)$
11 10 ralimi ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}\in {g}\left({k}\right)$
12 9 11 syl ${⊢}\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}\in {g}\left({k}\right)$
13 fveq2 ${⊢}{k}={n}\to {g}\left({k}\right)={g}\left({n}\right)$
14 13 eleq2d ${⊢}{k}={n}\to \left({P}\in {g}\left({k}\right)↔{P}\in {g}\left({n}\right)\right)$
15 14 rspccva ${⊢}\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{P}\in {g}\left({k}\right)\wedge {n}\in ℕ\right)\to {P}\in {g}\left({n}\right)$
16 12 15 sylan ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to {P}\in {g}\left({n}\right)$
17 eleq2 ${⊢}{y}={g}\left({n}\right)\to \left({P}\in {y}↔{P}\in {g}\left({n}\right)\right)$
18 ineq1 ${⊢}{y}={g}\left({n}\right)\to {y}\cap {S}={g}\left({n}\right)\cap {S}$
19 18 neeq1d ${⊢}{y}={g}\left({n}\right)\to \left({y}\cap {S}\ne \varnothing ↔{g}\left({n}\right)\cap {S}\ne \varnothing \right)$
20 17 19 imbi12d ${⊢}{y}={g}\left({n}\right)\to \left(\left({P}\in {y}\to {y}\cap {S}\ne \varnothing \right)↔\left({P}\in {g}\left({n}\right)\to {g}\left({n}\right)\cap {S}\ne \varnothing \right)\right)$
21 1 elcls2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\left({P}\in {X}\wedge \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {y}\to {y}\cap {S}\ne \varnothing \right)\right)\right)$
22 3 21 sylan ${⊢}\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\left({P}\in {X}\wedge \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {y}\to {y}\cap {S}\ne \varnothing \right)\right)\right)$
23 22 simplbda ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {y}\to {y}\cap {S}\ne \varnothing \right)$
24 23 ad2antrr ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {y}\to {y}\cap {S}\ne \varnothing \right)$
25 simpr1 ${⊢}\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\to {g}:ℕ⟶{J}$
26 25 ffvelrnda ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to {g}\left({n}\right)\in {J}$
27 20 24 26 rspcdva ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to \left({P}\in {g}\left({n}\right)\to {g}\left({n}\right)\cap {S}\ne \varnothing \right)$
28 16 27 mpd ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to {g}\left({n}\right)\cap {S}\ne \varnothing$
29 elin ${⊢}{x}\in \left({g}\left({n}\right)\cap {S}\right)↔\left({x}\in {g}\left({n}\right)\wedge {x}\in {S}\right)$
30 29 biancomi ${⊢}{x}\in \left({g}\left({n}\right)\cap {S}\right)↔\left({x}\in {S}\wedge {x}\in {g}\left({n}\right)\right)$
31 30 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left({g}\left({n}\right)\cap {S}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}\wedge {x}\in {g}\left({n}\right)\right)$
32 n0 ${⊢}{g}\left({n}\right)\cap {S}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left({g}\left({n}\right)\cap {S}\right)$
33 df-rex ${⊢}\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}\wedge {x}\in {g}\left({n}\right)\right)$
34 31 32 33 3bitr4i ${⊢}{g}\left({n}\right)\cap {S}\ne \varnothing ↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)$
35 28 34 sylib ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)$
36 3 ad2antrr ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {J}\in \mathrm{Top}$
37 1 topopn ${⊢}{J}\in \mathrm{Top}\to {X}\in {J}$
38 36 37 syl ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {X}\in {J}$
39 simplr ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {S}\subseteq {X}$
40 38 39 ssexd ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {S}\in \mathrm{V}$
41 fvi ${⊢}{S}\in \mathrm{V}\to \mathrm{I}\left({S}\right)={S}$
42 40 41 syl ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \mathrm{I}\left({S}\right)={S}$
43 42 ad2antrr ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to \mathrm{I}\left({S}\right)={S}$
44 43 rexeqdv ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to \left(\exists {x}\in \mathrm{I}\left({S}\right)\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)\right)$
45 35 44 mpbird ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge {n}\in ℕ\right)\to \exists {x}\in \mathrm{I}\left({S}\right)\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)$
46 45 ralrimiva ${⊢}\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{I}\left({S}\right)\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)$
47 fvex ${⊢}\mathrm{I}\left({S}\right)\in \mathrm{V}$
48 nnenom ${⊢}ℕ\approx \mathrm{\omega }$
49 eleq1 ${⊢}{x}={f}\left({n}\right)\to \left({x}\in {g}\left({n}\right)↔{f}\left({n}\right)\in {g}\left({n}\right)\right)$
50 47 48 49 axcc4 ${⊢}\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {x}\in \mathrm{I}\left({S}\right)\phantom{\rule{.4em}{0ex}}{x}\in {g}\left({n}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶\mathrm{I}\left({S}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)$
51 46 50 syl ${⊢}\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ⟶\mathrm{I}\left({S}\right)\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)$
52 42 feq3d ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left({f}:ℕ⟶\mathrm{I}\left({S}\right)↔{f}:ℕ⟶{S}\right)$
53 52 biimpd ${⊢}\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left({f}:ℕ⟶\mathrm{I}\left({S}\right)\to {f}:ℕ⟶{S}\right)$
54 53 adantr ${⊢}\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\to \left({f}:ℕ⟶\mathrm{I}\left({S}\right)\to {f}:ℕ⟶{S}\right)$
55 6 ad2antrr ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to {P}\in {X}$
56 simplr3 ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)$
57 eleq2 ${⊢}{x}={y}\to \left({P}\in {x}↔{P}\in {y}\right)$
58 fveq2 ${⊢}{k}={j}\to {g}\left({k}\right)={g}\left({j}\right)$
59 58 sseq1d ${⊢}{k}={j}\to \left({g}\left({k}\right)\subseteq {x}↔{g}\left({j}\right)\subseteq {x}\right)$
60 59 cbvrexvw ${⊢}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}↔\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {x}$
61 sseq2 ${⊢}{x}={y}\to \left({g}\left({j}\right)\subseteq {x}↔{g}\left({j}\right)\subseteq {y}\right)$
62 61 rexbidv ${⊢}{x}={y}\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {x}↔\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {y}\right)$
63 60 62 syl5bb ${⊢}{x}={y}\to \left(\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}↔\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {y}\right)$
64 57 63 imbi12d ${⊢}{x}={y}\to \left(\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)↔\left({P}\in {y}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {y}\right)\right)$
65 64 rspccva ${⊢}\left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\wedge {y}\in {J}\right)\to \left({P}\in {y}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {y}\right)$
66 56 65 sylan ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\wedge {y}\in {J}\right)\to \left({P}\in {y}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {y}\right)$
67 simpr ${⊢}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\to {g}\left({k}+1\right)\subseteq {g}\left({k}\right)$
68 67 ralimi ${⊢}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)$
69 9 68 syl ${⊢}\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)$
70 69 adantr ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\to \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)$
71 simprrr ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\to {j}\in ℕ$
72 fveq2 ${⊢}{n}={j}\to {g}\left({n}\right)={g}\left({j}\right)$
73 72 sseq1d ${⊢}{n}={j}\to \left({g}\left({n}\right)\subseteq {g}\left({j}\right)↔{g}\left({j}\right)\subseteq {g}\left({j}\right)\right)$
74 73 imbi2d ${⊢}{n}={j}\to \left(\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({n}\right)\subseteq {g}\left({j}\right)\right)↔\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({j}\right)\subseteq {g}\left({j}\right)\right)\right)$
75 fveq2 ${⊢}{n}={m}\to {g}\left({n}\right)={g}\left({m}\right)$
76 75 sseq1d ${⊢}{n}={m}\to \left({g}\left({n}\right)\subseteq {g}\left({j}\right)↔{g}\left({m}\right)\subseteq {g}\left({j}\right)\right)$
77 76 imbi2d ${⊢}{n}={m}\to \left(\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({n}\right)\subseteq {g}\left({j}\right)\right)↔\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({m}\right)\subseteq {g}\left({j}\right)\right)\right)$
78 fveq2 ${⊢}{n}={m}+1\to {g}\left({n}\right)={g}\left({m}+1\right)$
79 78 sseq1d ${⊢}{n}={m}+1\to \left({g}\left({n}\right)\subseteq {g}\left({j}\right)↔{g}\left({m}+1\right)\subseteq {g}\left({j}\right)\right)$
80 79 imbi2d ${⊢}{n}={m}+1\to \left(\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({n}\right)\subseteq {g}\left({j}\right)\right)↔\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({m}+1\right)\subseteq {g}\left({j}\right)\right)\right)$
81 ssid ${⊢}{g}\left({j}\right)\subseteq {g}\left({j}\right)$
82 81 2a1i ${⊢}{j}\in ℤ\to \left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({j}\right)\subseteq {g}\left({j}\right)\right)$
83 eluznn ${⊢}\left({j}\in ℕ\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\in ℕ$
84 fvoveq1 ${⊢}{k}={m}\to {g}\left({k}+1\right)={g}\left({m}+1\right)$
85 fveq2 ${⊢}{k}={m}\to {g}\left({k}\right)={g}\left({m}\right)$
86 84 85 sseq12d ${⊢}{k}={m}\to \left({g}\left({k}+1\right)\subseteq {g}\left({k}\right)↔{g}\left({m}+1\right)\subseteq {g}\left({m}\right)\right)$
87 86 rspccva ${⊢}\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {m}\in ℕ\right)\to {g}\left({m}+1\right)\subseteq {g}\left({m}\right)$
88 83 87 sylan2 ${⊢}\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge \left({j}\in ℕ\wedge {m}\in {ℤ}_{\ge {j}}\right)\right)\to {g}\left({m}+1\right)\subseteq {g}\left({m}\right)$
89 88 anassrs ${⊢}\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {g}\left({m}+1\right)\subseteq {g}\left({m}\right)$
90 sstr2 ${⊢}{g}\left({m}+1\right)\subseteq {g}\left({m}\right)\to \left({g}\left({m}\right)\subseteq {g}\left({j}\right)\to {g}\left({m}+1\right)\subseteq {g}\left({j}\right)\right)$
91 89 90 syl ${⊢}\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \left({g}\left({m}\right)\subseteq {g}\left({j}\right)\to {g}\left({m}+1\right)\subseteq {g}\left({j}\right)\right)$
92 91 expcom ${⊢}{m}\in {ℤ}_{\ge {j}}\to \left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to \left({g}\left({m}\right)\subseteq {g}\left({j}\right)\to {g}\left({m}+1\right)\subseteq {g}\left({j}\right)\right)\right)$
93 92 a2d ${⊢}{m}\in {ℤ}_{\ge {j}}\to \left(\left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({m}\right)\subseteq {g}\left({j}\right)\right)\to \left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({m}+1\right)\subseteq {g}\left({j}\right)\right)\right)$
94 74 77 80 77 82 93 uzind4 ${⊢}{m}\in {ℤ}_{\ge {j}}\to \left(\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to {g}\left({m}\right)\subseteq {g}\left({j}\right)\right)$
95 94 com12 ${⊢}\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to \left({m}\in {ℤ}_{\ge {j}}\to {g}\left({m}\right)\subseteq {g}\left({j}\right)\right)$
96 95 ralrimiv ${⊢}\left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}+1\right)\subseteq {g}\left({k}\right)\wedge {j}\in ℕ\right)\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{g}\left({m}\right)\subseteq {g}\left({j}\right)$
97 70 71 96 syl2anc ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{g}\left({m}\right)\subseteq {g}\left({j}\right)$
98 fveq2 ${⊢}{n}={m}\to {f}\left({n}\right)={f}\left({m}\right)$
99 98 75 eleq12d ${⊢}{n}={m}\to \left({f}\left({n}\right)\in {g}\left({n}\right)↔{f}\left({m}\right)\in {g}\left({m}\right)\right)$
100 simplr ${⊢}\left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)$
101 100 ad2antlr ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)$
102 71 83 sylan ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {m}\in ℕ$
103 99 101 102 rspcdva ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\wedge {m}\in {ℤ}_{\ge {j}}\right)\to {f}\left({m}\right)\in {g}\left({m}\right)$
104 103 ralrimiva ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {g}\left({m}\right)$
105 r19.26 ${⊢}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({g}\left({m}\right)\subseteq {g}\left({j}\right)\wedge {f}\left({m}\right)\in {g}\left({m}\right)\right)↔\left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{g}\left({m}\right)\subseteq {g}\left({j}\right)\wedge \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {g}\left({m}\right)\right)$
106 97 104 105 sylanbrc ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({g}\left({m}\right)\subseteq {g}\left({j}\right)\wedge {f}\left({m}\right)\in {g}\left({m}\right)\right)$
107 ssel2 ${⊢}\left({g}\left({m}\right)\subseteq {g}\left({j}\right)\wedge {f}\left({m}\right)\in {g}\left({m}\right)\right)\to {f}\left({m}\right)\in {g}\left({j}\right)$
108 107 ralimi ${⊢}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({g}\left({m}\right)\subseteq {g}\left({j}\right)\wedge {f}\left({m}\right)\in {g}\left({m}\right)\right)\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {g}\left({j}\right)$
109 106 108 syl ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {g}\left({j}\right)$
110 ssel ${⊢}{g}\left({j}\right)\subseteq {y}\to \left({f}\left({m}\right)\in {g}\left({j}\right)\to {f}\left({m}\right)\in {y}\right)$
111 110 ralimdv ${⊢}{g}\left({j}\right)\subseteq {y}\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {g}\left({j}\right)\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {y}\right)$
112 109 111 syl5com ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left(\left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\right)\to \left({g}\left({j}\right)\subseteq {y}\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {y}\right)$
113 112 anassrs ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\wedge \left({y}\in {J}\wedge {j}\in ℕ\right)\right)\to \left({g}\left({j}\right)\subseteq {y}\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {y}\right)$
114 113 anassrs ${⊢}\left(\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\wedge {y}\in {J}\right)\wedge {j}\in ℕ\right)\to \left({g}\left({j}\right)\subseteq {y}\to \forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {y}\right)$
115 114 reximdva ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\wedge {y}\in {J}\right)\to \left(\exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({j}\right)\subseteq {y}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {y}\right)$
116 66 115 syld ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\wedge {y}\in {J}\right)\to \left({P}\in {y}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {y}\right)$
117 116 ralrimiva ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to \forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {y}\to \exists {j}\in ℕ\phantom{\rule{.4em}{0ex}}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{f}\left({m}\right)\in {y}\right)$
118 36 ad2antrr ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to {J}\in \mathrm{Top}$
119 1 toptopon ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left({X}\right)$
120 118 119 sylib ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to {J}\in \mathrm{TopOn}\left({X}\right)$
121 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
122 1zzd ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to 1\in ℤ$
123 simprl ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to {f}:ℕ⟶{S}$
124 39 ad2antrr ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to {S}\subseteq {X}$
125 123 124 fssd ${⊢}\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\to {f}:ℕ⟶{X}$
126 eqidd ${⊢}\left(\left(\left(\left(\left({J}\in {1}^{st}𝜔\wedge {S}\subseteq {X}\right)\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}:ℕ⟶{J}\wedge \forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\left({k}\right)\wedge {g}\left({k}+1\right)\subseteq {g}\left({k}\right)\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to \exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{g}\left({k}\right)\subseteq {x}\right)\right)\right)\wedge \left({f}:ℕ⟶{S}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{f}\left({n}\right)\in {g}\left({n}\right)\right)\right)\wedge {m}\in ℕ\right)\to {f}\left({m}\right)={f}\left({m}\right)$
127 120 121 122 125 126 lmbrf
128 55 117 127 mpbir2and
129 128 expr
130 129 imdistanda
131 54 130 syland
132 131 eximdv
133 51 132 mpd
134 8 133 exlimddv
135 134 ex