Metamath Proof Explorer

Theorem lly1stc

Description: First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion lly1stc Locally 1stω = 1stω

Proof

Step Hyp Ref Expression
1 llytop ⊢ ( 𝑗 ∈ Locally 1stω → 𝑗 ∈ Top )
2 simprr ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → ( 𝑗 ↾t 𝑢 ) ∈ 1stω )
3 simprl ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → 𝑥 ∈ 𝑢 )
4 1 ad3antrrr ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → 𝑗 ∈ Top )
5 elssuni ⊢ ( 𝑢 ∈ 𝑗 → 𝑢 ⊆ ∪ 𝑗 )
6 5 ad2antlr ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → 𝑢 ⊆ ∪ 𝑗 )
7 eqid ⊢ ∪ 𝑗 = ∪ 𝑗
8 7 restuni ⊢ ( ( 𝑗 ∈ Top ∧ 𝑢 ⊆ ∪ 𝑗 ) → 𝑢 = ∪ ( 𝑗 ↾t 𝑢 ) )
9 4 6 8 syl2anc ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → 𝑢 = ∪ ( 𝑗 ↾t 𝑢 ) )
10 3 9 eleqtrd ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → 𝑥 ∈ ∪ ( 𝑗 ↾t 𝑢 ) )
11 eqid ⊢ ∪ ( 𝑗 ↾t 𝑢 ) = ∪ ( 𝑗 ↾t 𝑢 )
12 11 1stcclb ⊢ ( ( ( 𝑗 ↾t 𝑢 ) ∈ 1stω ∧ 𝑥 ∈ ∪ ( 𝑗 ↾t 𝑢 ) ) → ∃ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) )
13 2 10 12 syl2anc ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → ∃ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) )
14 elpwi ⊢ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) → 𝑡 ⊆ ( 𝑗 ↾t 𝑢 ) )
15 14 adantl ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → 𝑡 ⊆ ( 𝑗 ↾t 𝑢 ) )
16 15 sselda ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → 𝑛 ∈ ( 𝑗 ↾t 𝑢 ) )
17 4 adantr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → 𝑗 ∈ Top )
18 simpllr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → 𝑢 ∈ 𝑗 )
19 restopn2 ⊢ ( ( 𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗 ) → ( 𝑛 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑛 ∈ 𝑗 ∧ 𝑛 ⊆ 𝑢 ) ) )
20 17 18 19 syl2anc ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → ( 𝑛 ∈ ( 𝑗 ↾t 𝑢 ) ↔ ( 𝑛 ∈ 𝑗 ∧ 𝑛 ⊆ 𝑢 ) ) )
21 20 simplbda ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ ( 𝑗 ↾t 𝑢 ) ) → 𝑛 ⊆ 𝑢 )
22 16 21 syldan ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → 𝑛 ⊆ 𝑢 )
23 df-ss ⊢ ( 𝑛 ⊆ 𝑢 ↔ ( 𝑛 ∩ 𝑢 ) = 𝑛 )
24 22 23 sylib ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → ( 𝑛 ∩ 𝑢 ) = 𝑛 )
25 20 simprbda ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ ( 𝑗 ↾t 𝑢 ) ) → 𝑛 ∈ 𝑗 )
26 16 25 syldan ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → 𝑛 ∈ 𝑗 )
27 24 26 eqeltrd ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → ( 𝑛 ∩ 𝑢 ) ∈ 𝑗 )
28 ineq1 ⊢ ( 𝑎 = 𝑛 → ( 𝑎 ∩ 𝑢 ) = ( 𝑛 ∩ 𝑢 ) )
29 28 cbvmptv ⊢ ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) = ( 𝑛 ∈ 𝑡 ↦ ( 𝑛 ∩ 𝑢 ) )
30 27 29 fmptd ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) : 𝑡 ⟶ 𝑗 )
31 30 frnd ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ⊆ 𝑗 )
32 31 adantrr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ⊆ 𝑗 )
33 vex ⊢ 𝑗 ∈ V
34 33 elpw2 ⊢ ( ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ∈ 𝒫 𝑗 ↔ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ⊆ 𝑗 )
35 32 34 sylibr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ∈ 𝒫 𝑗 )
36 simprrl ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → 𝑡 ≼ ω )
37 1stcrestlem ⊢ ( 𝑡 ≼ ω → ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ≼ ω )
38 36 37 syl ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ≼ ω )
39 simprr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑥 ∈ 𝑧 )
40 3 ad2antrr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑥 ∈ 𝑢 )
41 39 40 elind ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑥 ∈ ( 𝑧 ∩ 𝑢 ) )
42 eleq2 ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( 𝑥 ∈ 𝑣 ↔ 𝑥 ∈ ( 𝑧 ∩ 𝑢 ) ) )
43 sseq2 ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( 𝑛 ⊆ 𝑣 ↔ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) )
44 43 anbi2d ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ↔ ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) ) )
45 44 rexbidv ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ↔ ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) ) )
46 42 45 imbi12d ⊢ ( 𝑣 = ( 𝑧 ∩ 𝑢 ) → ( ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ↔ ( 𝑥 ∈ ( 𝑧 ∩ 𝑢 ) → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) ) ) )
47 simprrr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) )
48 47 adantr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) )
49 4 ad2antrr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑗 ∈ Top )
50 simpllr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → 𝑢 ∈ 𝑗 )
51 50 adantr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑢 ∈ 𝑗 )
52 simprl ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → 𝑧 ∈ 𝑗 )
53 elrestr ⊢ ( ( 𝑗 ∈ Top ∧ 𝑢 ∈ 𝑗 ∧ 𝑧 ∈ 𝑗 ) → ( 𝑧 ∩ 𝑢 ) ∈ ( 𝑗 ↾t 𝑢 ) )
54 49 51 52 53 syl3anc ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → ( 𝑧 ∩ 𝑢 ) ∈ ( 𝑗 ↾t 𝑢 ) )
55 46 48 54 rspcdva ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → ( 𝑥 ∈ ( 𝑧 ∩ 𝑢 ) → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) ) )
56 41 55 mpd ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) )
57 3 ad2antrr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → 𝑥 ∈ 𝑢 )
58 elin ⊢ ( 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ↔ ( 𝑥 ∈ 𝑛 ∧ 𝑥 ∈ 𝑢 ) )
59 58 simplbi2com ⊢ ( 𝑥 ∈ 𝑢 → ( 𝑥 ∈ 𝑛 → 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ) )
60 57 59 syl ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → ( 𝑥 ∈ 𝑛 → 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ) )
61 22 biantrud ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → ( 𝑛 ⊆ 𝑧 ↔ ( 𝑛 ⊆ 𝑧 ∧ 𝑛 ⊆ 𝑢 ) ) )
62 ssin ⊢ ( ( 𝑛 ⊆ 𝑧 ∧ 𝑛 ⊆ 𝑢 ) ↔ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) )
63 61 62 bitrdi ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → ( 𝑛 ⊆ 𝑧 ↔ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) )
64 ssinss1 ⊢ ( 𝑛 ⊆ 𝑧 → ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 )
65 63 64 syl6bir ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → ( 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) → ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 ) )
66 60 65 anim12d ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) ∧ 𝑛 ∈ 𝑡 ) → ( ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) → ( 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ∧ ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 ) ) )
67 66 reximdva ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → ( ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ∧ ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 ) ) )
68 vex ⊢ 𝑛 ∈ V
69 68 inex1 ⊢ ( 𝑛 ∩ 𝑢 ) ∈ V
70 69 rgenw ⊢ ∀ 𝑛 ∈ 𝑡 ( 𝑛 ∩ 𝑢 ) ∈ V
71 eleq2 ⊢ ( 𝑤 = ( 𝑛 ∩ 𝑢 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ) )
72 sseq1 ⊢ ( 𝑤 = ( 𝑛 ∩ 𝑢 ) → ( 𝑤 ⊆ 𝑧 ↔ ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 ) )
73 71 72 anbi12d ⊢ ( 𝑤 = ( 𝑛 ∩ 𝑢 ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ∧ ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 ) ) )
74 29 73 rexrnmptw ⊢ ( ∀ 𝑛 ∈ 𝑡 ( 𝑛 ∩ 𝑢 ) ∈ V → ( ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ∧ ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 ) ) )
75 70 74 ax-mp ⊢ ( ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ ( 𝑛 ∩ 𝑢 ) ∧ ( 𝑛 ∩ 𝑢 ) ⊆ 𝑧 ) )
76 67 75 syl6ibr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ) → ( ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
77 76 adantrr ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → ( ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
78 77 adantr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → ( ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ ( 𝑧 ∩ 𝑢 ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
79 56 78 mpd ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ ( 𝑧 ∈ 𝑗 ∧ 𝑥 ∈ 𝑧 ) ) → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) )
80 79 expr ⊢ ( ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) ∧ 𝑧 ∈ 𝑗 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
81 80 ralrimiva ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
82 breq1 ⊢ ( 𝑦 = ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) → ( 𝑦 ≼ ω ↔ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ≼ ω ) )
83 rexeq ⊢ ( 𝑦 = ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) → ( ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
84 83 imbi2d ⊢ ( 𝑦 = ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) → ( ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
85 84 ralbidv ⊢ ( 𝑦 = ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) → ( ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
86 82 85 anbi12d ⊢ ( 𝑦 = ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) → ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ( ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
87 86 rspcev ⊢ ( ( ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ∈ 𝒫 𝑗 ∧ ( ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ran ( 𝑎 ∈ 𝑡 ↦ ( 𝑎 ∩ 𝑢 ) ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
88 35 38 81 87 syl12anc ⊢ ( ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) ∧ ( 𝑡 ∈ 𝒫 ( 𝑗 ↾t 𝑢 ) ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑣 ∈ ( 𝑗 ↾t 𝑢 ) ( 𝑥 ∈ 𝑣 → ∃ 𝑛 ∈ 𝑡 ( 𝑥 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑣 ) ) ) ) ) → ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
89 13 88 rexlimddv ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
90 89 3adantr1 ⊢ ( ( ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) ∧ 𝑢 ∈ 𝑗 ) ∧ ( 𝑢 ⊆ ∪ 𝑗 ∧ 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) ) → ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
91 simpl ⊢ ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) → 𝑗 ∈ Locally 1stω )
92 1 adantr ⊢ ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) → 𝑗 ∈ Top )
93 7 topopn ⊢ ( 𝑗 ∈ Top → ∪ 𝑗 ∈ 𝑗 )
94 92 93 syl ⊢ ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) → ∪ 𝑗 ∈ 𝑗 )
95 simpr ⊢ ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) → 𝑥 ∈ ∪ 𝑗 )
96 llyi ⊢ ( ( 𝑗 ∈ Locally 1stω ∧ ∪ 𝑗 ∈ 𝑗 ∧ 𝑥 ∈ ∪ 𝑗 ) → ∃ 𝑢 ∈ 𝑗 ( 𝑢 ⊆ ∪ 𝑗 ∧ 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) )
97 91 94 95 96 syl3anc ⊢ ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) → ∃ 𝑢 ∈ 𝑗 ( 𝑢 ⊆ ∪ 𝑗 ∧ 𝑥 ∈ 𝑢 ∧ ( 𝑗 ↾t 𝑢 ) ∈ 1stω ) )
98 90 97 r19.29a ⊢ ( ( 𝑗 ∈ Locally 1stω ∧ 𝑥 ∈ ∪ 𝑗 ) → ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
99 98 ralrimiva ⊢ ( 𝑗 ∈ Locally 1stω → ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
100 7 is1stc2 ⊢ ( 𝑗 ∈ 1stω ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑦 ∈ 𝒫 𝑗 ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ 𝑗 ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
101 1 99 100 sylanbrc ⊢ ( 𝑗 ∈ Locally 1stω → 𝑗 ∈ 1stω )
102 101 ssriv ⊢ Locally 1stω ⊆ 1stω
103 1stcrest ⊢ ( ( 𝑗 ∈ 1stω ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ 1stω )
104 103 adantl ⊢ ( ( ⊤ ∧ ( 𝑗 ∈ 1stω ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ 1stω )
105 1stctop ⊢ ( 𝑗 ∈ 1stω → 𝑗 ∈ Top )
106 105 ssriv ⊢ 1stω ⊆ Top
107 106 a1i ⊢ ( ⊤ → 1stω ⊆ Top )
108 104 107 restlly ⊢ ( ⊤ → 1stω ⊆ Locally 1stω )
109 108 mptru ⊢ 1stω ⊆ Locally 1stω
110 102 109 eqssi ⊢ Locally 1stω = 1stω