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

Metamath Proof Explorer

Theorem 1stcfb

Description: For any point A in a first-countable topology, there is a function f : NN --> J enumerating neighborhoods of A which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis 1stcclb.1 ⊢ 𝑋 = ∪ 𝐽
Assertion 1stcfb ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 1stcclb.1 ⊢ 𝑋 = ∪ 𝐽
2 1 1stcclb ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝒫 𝐽 ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) )
3 simplr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → 𝐴 ∈ 𝑋 )
4 eleq2 ⊢ ( 𝑧 = 𝑋 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋 ) )
5 sseq2 ⊢ ( 𝑧 = 𝑋 → ( 𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑋 ) )
6 5 anbi2d ⊢ ( 𝑧 = 𝑋 → ( ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋 ) ) )
7 6 rexbidv ⊢ ( 𝑧 = 𝑋 → ( ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋 ) ) )
8 4 7 imbi12d ⊢ ( 𝑧 = 𝑋 → ( ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( 𝐴 ∈ 𝑋 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋 ) ) ) )
9 simprrr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
10 1stctop ⊢ ( 𝐽 ∈ 1stω → 𝐽 ∈ Top )
11 10 ad2antrr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → 𝐽 ∈ Top )
12 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
13 11 12 syl ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → 𝑋 ∈ 𝐽 )
14 8 9 13 rspcdva ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ( 𝐴 ∈ 𝑋 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋 ) ) )
15 3 14 mpd ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋 ) )
16 simpl ⊢ ( ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋 ) → 𝐴 ∈ 𝑤 )
17 16 reximi ⊢ ( ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋 ) → ∃ 𝑤 ∈ 𝑥 𝐴 ∈ 𝑤 )
18 15 17 syl ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ∃ 𝑤 ∈ 𝑥 𝐴 ∈ 𝑤 )
19 eleq2w ⊢ ( 𝑤 = 𝑎 → ( 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑎 ) )
20 19 cbvrexvw ⊢ ( ∃ 𝑤 ∈ 𝑥 𝐴 ∈ 𝑤 ↔ ∃ 𝑎 ∈ 𝑥 𝐴 ∈ 𝑎 )
21 18 20 sylib ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ∃ 𝑎 ∈ 𝑥 𝐴 ∈ 𝑎 )
22 rabn0 ⊢ ( { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≠ ∅ ↔ ∃ 𝑎 ∈ 𝑥 𝐴 ∈ 𝑎 )
23 21 22 sylibr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≠ ∅ )
24 vex ⊢ 𝑥 ∈ V
25 24 rabex ⊢ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ∈ V
26 25 0sdom ⊢ ( ∅ ≺ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ↔ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≠ ∅ )
27 23 26 sylibr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ∅ ≺ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
28 ssrab2 ⊢ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ⊆ 𝑥
29 ssdomg ⊢ ( 𝑥 ∈ V → ( { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ⊆ 𝑥 → { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≼ 𝑥 ) )
30 24 28 29 mp2 ⊢ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≼ 𝑥
31 simprrl ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → 𝑥 ≼ ω )
32 nnenom ⊢ ℕ ≈ ω
33 32 ensymi ⊢ ω ≈ ℕ
34 domentr ⊢ ( ( 𝑥 ≼ ω ∧ ω ≈ ℕ ) → 𝑥 ≼ ℕ )
35 31 33 34 sylancl ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → 𝑥 ≼ ℕ )
36 domtr ⊢ ( ( { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≼ 𝑥 ∧ 𝑥 ≼ ℕ ) → { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≼ ℕ )
37 30 35 36 sylancr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≼ ℕ )
38 fodomr ⊢ ( ( ∅ ≺ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ∧ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ≼ ℕ ) → ∃ 𝑔 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
39 27 37 38 syl2anc ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ∃ 𝑔 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
40 10 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → 𝐽 ∈ Top )
41 imassrn ⊢ ( 𝑔 “ ( 1 ... 𝑛 ) ) ⊆ ran 𝑔
42 forn ⊢ ( 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } → ran 𝑔 = { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
43 42 ad2antll ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ran 𝑔 = { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
44 simprll ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → 𝑥 ∈ 𝒫 𝐽 )
45 44 elpwid ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → 𝑥 ⊆ 𝐽 )
46 28 45 sstrid ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ⊆ 𝐽 )
47 43 46 eqsstrd ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ran 𝑔 ⊆ 𝐽 )
48 47 adantr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ran 𝑔 ⊆ 𝐽 )
49 41 48 sstrid ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 “ ( 1 ... 𝑛 ) ) ⊆ 𝐽 )
50 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
51 fof ⊢ ( 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } → 𝑔 : ℕ ⟶ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
52 51 ad2antll ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → 𝑔 : ℕ ⟶ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
53 52 fdmd ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → dom 𝑔 = ℕ )
54 50 53 sseqtrrid ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ( 1 ... 𝑛 ) ⊆ dom 𝑔 )
55 54 adantr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ dom 𝑔 )
56 sseqin2 ⊢ ( ( 1 ... 𝑛 ) ⊆ dom 𝑔 ↔ ( dom 𝑔 ∩ ( 1 ... 𝑛 ) ) = ( 1 ... 𝑛 ) )
57 55 56 sylib ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( dom 𝑔 ∩ ( 1 ... 𝑛 ) ) = ( 1 ... 𝑛 ) )
58 elfz1end ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( 1 ... 𝑛 ) )
59 ne0i ⊢ ( 𝑛 ∈ ( 1 ... 𝑛 ) → ( 1 ... 𝑛 ) ≠ ∅ )
60 59 adantl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ( 1 ... 𝑛 ) ) → ( 1 ... 𝑛 ) ≠ ∅ )
61 58 60 sylan2b ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ≠ ∅ )
62 57 61 eqnetrd ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( dom 𝑔 ∩ ( 1 ... 𝑛 ) ) ≠ ∅ )
63 imadisj ⊢ ( ( 𝑔 “ ( 1 ... 𝑛 ) ) = ∅ ↔ ( dom 𝑔 ∩ ( 1 ... 𝑛 ) ) = ∅ )
64 63 necon3bii ⊢ ( ( 𝑔 “ ( 1 ... 𝑛 ) ) ≠ ∅ ↔ ( dom 𝑔 ∩ ( 1 ... 𝑛 ) ) ≠ ∅ )
65 62 64 sylibr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 “ ( 1 ... 𝑛 ) ) ≠ ∅ )
66 fzfid ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
67 52 ffund ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → Fun 𝑔 )
68 fores ⊢ ( ( Fun 𝑔 ∧ ( 1 ... 𝑛 ) ⊆ dom 𝑔 ) → ( 𝑔 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –onto→ ( 𝑔 “ ( 1 ... 𝑛 ) ) )
69 67 55 68 syl2an2r ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –onto→ ( 𝑔 “ ( 1 ... 𝑛 ) ) )
70 fofi ⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ ( 𝑔 ↾ ( 1 ... 𝑛 ) ) : ( 1 ... 𝑛 ) –onto→ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ Fin )
71 66 69 70 syl2anc ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ Fin )
72 fiinopn ⊢ ( 𝐽 ∈ Top → ( ( ( 𝑔 “ ( 1 ... 𝑛 ) ) ⊆ 𝐽 ∧ ( 𝑔 “ ( 1 ... 𝑛 ) ) ≠ ∅ ∧ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ Fin ) → ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 ) )
73 72 imp ⊢ ( ( 𝐽 ∈ Top ∧ ( ( 𝑔 “ ( 1 ... 𝑛 ) ) ⊆ 𝐽 ∧ ( 𝑔 “ ( 1 ... 𝑛 ) ) ≠ ∅ ∧ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ Fin ) ) → ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 )
74 40 49 65 71 73 syl13anc ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑛 ∈ ℕ ) → ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 )
75 74 fmpttd ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) : ℕ ⟶ 𝐽 )
76 imassrn ⊢ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ ran 𝑔
77 43 adantr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ran 𝑔 = { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
78 76 77 sseqtrid ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } )
79 id ⊢ ( 𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛 )
80 79 rgenw ⊢ ∀ 𝑛 ∈ 𝑥 ( 𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛 )
81 eleq2w ⊢ ( 𝑎 = 𝑛 → ( 𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑛 ) )
82 81 ralrab ⊢ ( ∀ 𝑛 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝐴 ∈ 𝑛 ↔ ∀ 𝑛 ∈ 𝑥 ( 𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛 ) )
83 80 82 mpbir ⊢ ∀ 𝑛 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝐴 ∈ 𝑛
84 ssralv ⊢ ( ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } → ( ∀ 𝑛 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝐴 ∈ 𝑛 → ∀ 𝑛 ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) 𝐴 ∈ 𝑛 ) )
85 78 83 84 mpisyl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) 𝐴 ∈ 𝑛 )
86 elintg ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ↔ ∀ 𝑛 ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) 𝐴 ∈ 𝑛 ) )
87 86 ad3antlr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ∈ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ↔ ∀ 𝑛 ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) 𝐴 ∈ 𝑛 ) )
88 85 87 mpbird ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) )
89 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) )
90 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 1 ... 𝑛 ) = ( 1 ... 𝑘 ) )
91 90 imaeq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑔 “ ( 1 ... 𝑛 ) ) = ( 𝑔 “ ( 1 ... 𝑘 ) ) )
92 91 inteqd ⊢ ( 𝑛 = 𝑘 → ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) = ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) )
93 simpr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
94 74 ralrimiva ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ∀ 𝑛 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 )
95 92 eleq1d ⊢ ( 𝑛 = 𝑘 → ( ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 ↔ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ∈ 𝐽 ) )
96 95 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 ∧ 𝑘 ∈ ℕ ) → ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ∈ 𝐽 )
97 94 96 sylan ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ∈ 𝐽 )
98 89 92 93 97 fvmptd3 ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) = ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) )
99 88 98 eleqtrrd ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) )
100 fzssp1 ⊢ ( 1 ... 𝑘 ) ⊆ ( 1 ... ( 𝑘 + 1 ) )
101 imass2 ⊢ ( ( 1 ... 𝑘 ) ⊆ ( 1 ... ( 𝑘 + 1 ) ) → ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) )
102 100 101 mp1i ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) )
103 intss ⊢ ( ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) → ∩ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) ⊆ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) )
104 102 103 syl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ∩ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) ⊆ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) )
105 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 ... 𝑛 ) = ( 1 ... ( 𝑘 + 1 ) ) )
106 105 imaeq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑔 “ ( 1 ... 𝑛 ) ) = ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) )
107 106 inteqd ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) = ∩ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) )
108 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
109 108 adantl ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
110 107 eleq1d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 ↔ ∩ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) ∈ 𝐽 ) )
111 110 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ∈ 𝐽 ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ∩ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) ∈ 𝐽 )
112 94 108 111 syl2an ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ∩ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) ∈ 𝐽 )
113 89 107 109 112 fvmptd3 ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) = ∩ ( 𝑔 “ ( 1 ... ( 𝑘 + 1 ) ) ) )
114 104 113 98 3sstr4d ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) )
115 99 114 jca ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) )
116 115 ralrimiva ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) )
117 simprlr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) )
118 eleq2w ⊢ ( 𝑧 = 𝑦 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦 ) )
119 sseq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑦 ) )
120 119 anbi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ) )
121 120 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ↔ ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ) )
122 118 121 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ↔ ( 𝐴 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ) ) )
123 122 rspccva ⊢ ( ( ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ) )
124 117 123 sylan ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑦 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) ) )
125 eleq2w ⊢ ( 𝑎 = 𝑤 → ( 𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤 ) )
126 125 rexrab ⊢ ( ∃ 𝑤 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝑤 ⊆ 𝑦 ↔ ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) )
127 43 rexeqdv ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ( ∃ 𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃ 𝑤 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝑤 ⊆ 𝑦 ) )
128 fofn ⊢ ( 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } → 𝑔 Fn ℕ )
129 128 ad2antll ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → 𝑔 Fn ℕ )
130 sseq1 ⊢ ( 𝑤 = ( 𝑔 ‘ 𝑘 ) → ( 𝑤 ⊆ 𝑦 ↔ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 ) )
131 130 rexrn ⊢ ( 𝑔 Fn ℕ → ( ∃ 𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 ) )
132 129 131 syl ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ( ∃ 𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 ) )
133 127 132 bitr3d ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ( ∃ 𝑤 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝑤 ⊆ 𝑦 ↔ ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 ) )
134 133 adantr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝑤 ⊆ 𝑦 ↔ ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 ) )
135 elfz1end ⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( 1 ... 𝑘 ) )
136 fz1ssnn ⊢ ( 1 ... 𝑘 ) ⊆ ℕ
137 53 adantr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → dom 𝑔 = ℕ )
138 136 137 sseqtrrid ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 1 ... 𝑘 ) ⊆ dom 𝑔 )
139 funfvima2 ⊢ ( ( Fun 𝑔 ∧ ( 1 ... 𝑘 ) ⊆ dom 𝑔 ) → ( 𝑘 ∈ ( 1 ... 𝑘 ) → ( 𝑔 ‘ 𝑘 ) ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) ) )
140 67 138 139 syl2an2r ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑘 ∈ ( 1 ... 𝑘 ) → ( 𝑔 ‘ 𝑘 ) ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) ) )
141 140 imp ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑘 ∈ ( 1 ... 𝑘 ) ) → ( 𝑔 ‘ 𝑘 ) ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) )
142 135 141 sylan2b ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑔 ‘ 𝑘 ) ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) )
143 intss1 ⊢ ( ( 𝑔 ‘ 𝑘 ) ∈ ( 𝑔 “ ( 1 ... 𝑘 ) ) → ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) )
144 sstr2 ⊢ ( ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝑔 ‘ 𝑘 ) → ( ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 → ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
145 142 143 144 3syl ⊢ ( ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 → ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
146 145 reximdva ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑘 ∈ ℕ ( 𝑔 ‘ 𝑘 ) ⊆ 𝑦 → ∃ 𝑘 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
147 134 146 sylbid ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } 𝑤 ⊆ 𝑦 → ∃ 𝑘 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
148 126 147 biimtrrid ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦 ) → ∃ 𝑘 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
149 124 148 syld ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
150 98 sseq1d ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ↔ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
151 150 rexbidva ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ( ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ↔ ∃ 𝑘 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
152 151 adantr ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ↔ ∃ 𝑘 ∈ ℕ ∩ ( 𝑔 “ ( 1 ... 𝑘 ) ) ⊆ 𝑦 ) )
153 149 152 sylibrd ⊢ ( ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) )
154 153 ralrimiva ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) )
155 nnex ⊢ ℕ ∈ V
156 155 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ∈ V
157 feq1 ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( 𝑓 : ℕ ⟶ 𝐽 ↔ ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) : ℕ ⟶ 𝐽 ) )
158 fveq1 ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( 𝑓 ‘ 𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) )
159 158 eleq2d ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ↔ 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) )
160 fveq1 ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( 𝑓 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) )
161 160 158 sseq12d ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ↔ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) )
162 159 161 anbi12d ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ↔ ( 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
163 162 ralbidv ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) ) )
164 158 sseq1d ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ↔ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) )
165 164 rexbidv ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ↔ ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) )
166 165 imbi2d ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ↔ ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) ) )
167 166 ralbidv ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) ) )
168 157 163 167 3anbi123d ⊢ ( 𝑓 = ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) → ( ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) ↔ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) ) ) )
169 156 168 spcev ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ∧ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ ( 𝑘 + 1 ) ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ∩ ( 𝑔 “ ( 1 ... 𝑛 ) ) ) ‘ 𝑘 ) ⊆ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) )
170 75 116 154 169 syl3anc ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ∧ 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) )
171 170 expr ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) → ( 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) ) )
172 171 adantrrl ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ( 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) ) )
173 172 exlimdv ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ( ∃ 𝑔 𝑔 : ℕ –onto→ { 𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎 } → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) ) )
174 39 173 mpd ⊢ ( ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝒫 𝐽 ∧ ( 𝑥 ≼ ω ∧ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ∃ 𝑤 ∈ 𝑥 ( 𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧 ) ) ) ) ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) )
175 2 174 rexlimddv ⊢ ( ( 𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) )