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	⊢ ( ( 𝐽 ∈ 1^stω ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ℕ ( 𝐴 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( 𝑓 ‘ ( 𝑘 + 1 ) ) ⊆ ( 𝑓 ‘ 𝑘 ) ) ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ⊆ 𝑦 ) ) )

Proof

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

Metamath Proof Explorer

Theorem 1stcfb

Proof