This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1stcrest

Description: A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 1stcrest ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ 1stω )

Proof

Step Hyp Ref Expression
1 1stctop ⊢ ( 𝐽 ∈ 1stω → 𝐽 ∈ Top )
2 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
3 1 2 sylan ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )
4 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
5 4 restuni2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
6 1 5 sylan ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ∪ 𝐽 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
7 6 eleq2d ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ↔ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ) )
8 7 biimpar ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) )
9 simpl ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → 𝐽 ∈ 1stω )
10 elinel2 ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) → 𝑥 ∈ ∪ 𝐽 )
11 4 1stcclb ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝑥 ∈ ∪ 𝐽 ) → ∃ 𝑡 ∈ 𝒫 𝐽 ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) )
12 9 10 11 syl2an ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) → ∃ 𝑡 ∈ 𝒫 𝐽 ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) )
13 simplll ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝐽 ∈ 1stω )
14 elpwi ⊢ ( 𝑡 ∈ 𝒫 𝐽 → 𝑡 ⊆ 𝐽 )
15 14 ad2antrl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝑡 ⊆ 𝐽 )
16 ssrest ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝑡 ⊆ 𝐽 ) → ( 𝑡 ↾t 𝐴 ) ⊆ ( 𝐽 ↾t 𝐴 ) )
17 13 15 16 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) ⊆ ( 𝐽 ↾t 𝐴 ) )
18 ovex ⊢ ( 𝐽 ↾t 𝐴 ) ∈ V
19 18 elpw2 ⊢ ( ( 𝑡 ↾t 𝐴 ) ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ↔ ( 𝑡 ↾t 𝐴 ) ⊆ ( 𝐽 ↾t 𝐴 ) )
20 17 19 sylibr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) )
21 vex ⊢ 𝑡 ∈ V
22 simpllr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝐴 ∈ 𝑉 )
23 restval ⊢ ( ( 𝑡 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑡 ↾t 𝐴 ) = ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) )
24 21 22 23 sylancr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) = ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) )
25 simprrl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝑡 ≼ ω )
26 1stcrestlem ⊢ ( 𝑡 ≼ ω → ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) ≼ ω )
27 25 26 syl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ran ( 𝑣 ∈ 𝑡 ↦ ( 𝑣 ∩ 𝐴 ) ) ≼ ω )
28 24 27 eqbrtrd ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑡 ↾t 𝐴 ) ≼ ω )
29 1 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → 𝐽 ∈ Top )
30 elrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) )
31 29 22 30 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) )
32 r19.29 ⊢ ( ( ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐽 ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ 𝑧 = ( 𝑎 ∩ 𝐴 ) ) )
33 simprr ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
34 33 a1d ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ 𝐴 ) )
35 34 ancld ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴 ) ) )
36 elin ⊢ ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
37 35 36 imbitrrdi ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ) )
38 ssrin ⊢ ( 𝑦 ⊆ 𝑎 → ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) )
39 37 38 anim12d1 ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
40 39 reximdv ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
41 vex ⊢ 𝑦 ∈ V
42 41 inex1 ⊢ ( 𝑦 ∩ 𝐴 ) ∈ V
43 42 a1i ⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) ∧ 𝑦 ∈ 𝑡 ) → ( 𝑦 ∩ 𝐴 ) ∈ V )
44 simp-4r ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐴 ∈ 𝑉 )
45 elrest ⊢ ( ( 𝑡 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑡 𝑤 = ( 𝑦 ∩ 𝐴 ) ) )
46 21 44 45 sylancr ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑡 𝑤 = ( 𝑦 ∩ 𝐴 ) ) )
47 eleq2 ⊢ ( 𝑤 = ( 𝑦 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ) )
48 sseq1 ⊢ ( 𝑤 = ( 𝑦 ∩ 𝐴 ) → ( 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ↔ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) )
49 47 48 anbi12d ⊢ ( 𝑤 = ( 𝑦 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
50 49 adantl ⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) ∧ 𝑤 = ( 𝑦 ∩ 𝐴 ) ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ↔ ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
51 43 46 50 rexxfr2d ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ↔ ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( 𝑦 ∩ 𝐴 ) ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
52 40 51 sylibrd ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ ( 𝑎 ∈ 𝐽 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
53 52 expr ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) )
54 53 com23 ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) → ( 𝑥 ∈ 𝐴 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) )
55 54 imim2d ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) → ( 𝑥 ∈ 𝑎 → ( 𝑥 ∈ 𝐴 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) ) )
56 55 imp4b ⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) → ( ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
57 eleq2 ⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( 𝑎 ∩ 𝐴 ) ) )
58 elin ⊢ ( 𝑥 ∈ ( 𝑎 ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) )
59 57 58 bitrdi ⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 ↔ ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) ) )
60 sseq2 ⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) )
61 60 anbi2d ⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
62 61 rexbidv ⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) )
63 59 62 imbi12d ⊢ ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝑎 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑎 ∩ 𝐴 ) ) ) ) )
64 56 63 syl5ibrcom ⊢ ( ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) ∧ ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) → ( 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
65 64 expimpd ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) ∧ 𝑎 ∈ 𝐽 ) → ( ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
66 65 rexlimdva ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) → ( ∃ 𝑎 ∈ 𝐽 ( ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
67 32 66 syl5 ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) → ( ( ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ∧ ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
68 67 expd ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ 𝑡 ∈ 𝒫 𝐽 ) → ( ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) → ( ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
69 68 impr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) → ( ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
70 69 adantrrl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( ∃ 𝑎 ∈ 𝐽 𝑧 = ( 𝑎 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
71 31 70 sylbid ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ( 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) → ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
72 71 ralrimiv ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
73 breq1 ⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( 𝑦 ≼ ω ↔ ( 𝑡 ↾t 𝐴 ) ≼ ω ) )
74 rexeq ⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
75 74 imbi2d ⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
76 75 ralbidv ⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
77 73 76 anbi12d ⊢ ( 𝑦 = ( 𝑡 ↾t 𝐴 ) → ( ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ↔ ( ( 𝑡 ↾t 𝐴 ) ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
78 77 rspcev ⊢ ( ( ( 𝑡 ↾t 𝐴 ) ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ∧ ( ( 𝑡 ↾t 𝐴 ) ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ ( 𝑡 ↾t 𝐴 ) ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
79 20 28 72 78 syl12anc ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) ∧ ( 𝑡 ∈ 𝒫 𝐽 ∧ ( 𝑡 ≼ ω ∧ ∀ 𝑎 ∈ 𝐽 ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑡 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑎 ) ) ) ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
80 12 79 rexlimddv ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝐴 ∩ ∪ 𝐽 ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
81 8 80 syldan ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ) → ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
82 81 ralrimiva ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
83 eqid ⊢ ∪ ( 𝐽 ↾t 𝐴 ) = ∪ ( 𝐽 ↾t 𝐴 )
84 83 is1stc2 ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ 1stω ↔ ( ( 𝐽 ↾t 𝐴 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( 𝐽 ↾t 𝐴 ) ∃ 𝑦 ∈ 𝒫 ( 𝐽 ↾t 𝐴 ) ( 𝑦 ≼ ω ∧ ∀ 𝑧 ∈ ( 𝐽 ↾t 𝐴 ) ( 𝑥 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑦 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) )
85 3 82 84 sylanbrc ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ 1stω )