Theorem 1stcfb 23273

Description: For any point 𝐴 in a first-countable topology, there is a function 𝑓:ℕ⟶𝐽 enumerating neighborhoods of 𝐴 which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015.)

Hypothesis

Ref	Expression
1stcclb.1	⊢ 𝑋 = ∪ 𝐽

Assertion

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

Distinct variable groups:   𝑓,𝑘,𝑦,𝐴   𝑓,𝐽,𝑘,𝑦   𝑘,𝑋,𝑦

Allowed substitution hint:   𝑋(𝑓)

Proof of Theorem 1stcfb

Dummy variables 𝑎 𝑔 𝑛 𝑤 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1stcclb.1	. . 3 ⊢ 𝑋 = ∪ 𝐽
2	1	1stcclb 23272	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
3		simplr 766	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐴 ∈ 𝑋)
4		eleq2 2814	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
5		sseq2 4001	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑋 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑋))
6	5	anbi2d 628	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
7	6	rexbidv 3170	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
8	4, 7	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))))
9		simprrr 779	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
10		1stctop 23271	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
11	10	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐽 ∈ Top)
12	1	topopn 22732	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
13	11, 12	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑋 ∈ 𝐽)
14	8, 9, 13	rspcdva 3605	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
15	3, 14	mpd 15	. . . . . . . 8 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))
16		simpl 482	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → 𝐴 ∈ 𝑤)
17	16	reximi 3076	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
18	15, 17	syl 17	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
19		eleq2w 2809	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑎))
20	19	cbvrexvw 3227	. . . . . . 7 ⊢ (∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤 ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
21	18, 20	sylib 217	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
22		rabn0 4378	. . . . . 6 ⊢ ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
23	21, 22	sylibr 233	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
24		vex 3470	. . . . . . 7 ⊢ 𝑥 ∈ V
25	24	rabex 5323	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∈ V
26	25	0sdom 9104	. . . . 5 ⊢ (∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ↔ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
27	23, 26	sylibr 233	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
28		ssrab2 4070	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥
29		ssdomg 8993	. . . . . 6 ⊢ (𝑥 ∈ V → ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥 → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥))
30	24, 28, 29	mp2 9	. . . . 5 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥
31		simprrl 778	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ω)
32		nnenom 13943	. . . . . . 7 ⊢ ℕ ≈ ω
33	32	ensymi 8997	. . . . . 6 ⊢ ω ≈ ℕ
34		domentr 9006	. . . . . 6 ⊢ ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
35	31, 33, 34	sylancl 585	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ℕ)
36		domtr 9000	. . . . 5 ⊢ (({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥 ∧ 𝑥 ≼ ℕ) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
37	30, 35, 36	sylancr 586	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
38		fodomr 9125	. . . 4 ⊢ ((∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∧ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
39	27, 37, 38	syl2anc 583	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
40	10	ad3antrrr 727	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → 𝐽 ∈ Top)
41		imassrn 6061	. . . . . . . . . 10 ⊢ (𝑔 “ (1...𝑛)) ⊆ ran 𝑔
42		forn 6799	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
43	42	ad2antll 726	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
44		simprll 776	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ∈ 𝒫 𝐽)
45	44	elpwid 4604	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ⊆ 𝐽)
46	28, 45	sstrid 3986	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝐽)
47	43, 46	eqsstrd 4013	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 ⊆ 𝐽)
48	47	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ran 𝑔 ⊆ 𝐽)
49	41, 48	sstrid 3986	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ⊆ 𝐽)
50		fz1ssnn 13530	. . . . . . . . . . . . . 14 ⊢ (1...𝑛) ⊆ ℕ
51		fof 6796	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
52	51	ad2antll 726	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
53	52	fdmd 6719	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → dom 𝑔 = ℕ)
54	50, 53	sseqtrrid 4028	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (1...𝑛) ⊆ dom 𝑔)
55	54	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ dom 𝑔)
56		sseqin2 4208	. . . . . . . . . . . 12 ⊢ ((1...𝑛) ⊆ dom 𝑔 ↔ (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
57	55, 56	sylib 217	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
58		elfz1end 13529	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
59		ne0i 4327	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑛) → (1...𝑛) ≠ ∅)
60	59	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ (1...𝑛)) → (1...𝑛) ≠ ∅)
61	58, 60	sylan2b 593	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ≠ ∅)
62	57, 61	eqnetrd 3000	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
63		imadisj 6070	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑛)) = ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) = ∅)
64	63	necon3bii 2985	. . . . . . . . . 10 ⊢ ((𝑔 “ (1...𝑛)) ≠ ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
65	62, 64	sylibr 233	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ≠ ∅)
66		fzfid 13936	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
67	52	ffund 6712	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → Fun 𝑔)
68		fores 6806	. . . . . . . . . . 11 ⊢ ((Fun 𝑔 ∧ (1...𝑛) ⊆ dom 𝑔) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
69	67, 55, 68	syl2an2r 682	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
70		fofi 9335	. . . . . . . . . 10 ⊢ (((1...𝑛) ∈ Fin ∧ (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛))) → (𝑔 “ (1...𝑛)) ∈ Fin)
71	66, 69, 70	syl2anc 583	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ Fin)
72		fiinopn 22727	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽))
73	72	imp 406	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin)) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
74	40, 49, 65, 71, 73	syl13anc 1369	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
75	74	fmpttd 7107	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽)
76		imassrn 6061	. . . . . . . . . . . . 13 ⊢ (𝑔 “ (1...𝑘)) ⊆ ran 𝑔
77	43	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
78	76, 77	sseqtrid 4027	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
79		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
80	79	rgenw 3057	. . . . . . . . . . . . 13 ⊢ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
81		eleq2w 2809	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑛 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑛))
82	81	ralrab 3682	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 ↔ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛))
83	80, 82	mpbir 230	. . . . . . . . . . . 12 ⊢ ∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛
84		ssralv 4043	. . . . . . . . . . . 12 ⊢ ((𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
85	78, 83, 84	mpisyl 21	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛)
86		elintg 4949	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
87	86	ad3antlr 728	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
88	85, 87	mpbird 257	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ∩ (𝑔 “ (1...𝑘)))
89		eqid 2724	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))
90		oveq2 7410	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
91	90	imaeq2d 6050	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
92	91	inteqd 4946	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...𝑘)))
93		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
94	74	ralrimiva 3138	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
95	92	eleq1d 2810	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽))
96	95	rspccva 3603	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
97	94, 96	sylan 579	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
98	89, 92, 93, 97	fvmptd3 7012	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) = ∩ (𝑔 “ (1...𝑘)))
99	88, 98	eleqtrrd 2828	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
100		fzssp1 13542	. . . . . . . . . . . 12 ⊢ (1...𝑘) ⊆ (1...(𝑘 + 1))
101		imass2 6092	. . . . . . . . . . . 12 ⊢ ((1...𝑘) ⊆ (1...(𝑘 + 1)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
102	100, 101	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
103		intss 4964	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
104	102, 103	syl 17	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
105		oveq2 7410	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
106	105	imaeq2d 6050	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
107	106	inteqd 4946	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
108		peano2nn 12222	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
109	108	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
110	107	eleq1d 2810	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽))
111	110	rspccva 3603	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ (𝑘 + 1) ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
112	94, 108, 111	syl2an 595	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
113	89, 107, 109, 112	fvmptd3 7012	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
114	104, 113, 98	3sstr4d 4022	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
115	99, 114	jca 511	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
116	115	ralrimiva 3138	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
117		simprlr 777	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
118		eleq2w 2809	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦))
119		sseq2 4001	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑦))
120	119	anbi2d 628	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
121	120	rexbidv 3170	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
122	118, 121	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))))
123	122	rspccva 3603	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
124	117, 123	sylan 579	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
125		eleq2w 2809	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
126	125	rexrab 3685	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))
127	43	rexeqdv 3318	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦))
128		fofn 6798	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔 Fn ℕ)
129	128	ad2antll 726	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔 Fn ℕ)
130		sseq1 4000	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑔‘𝑘) → (𝑤 ⊆ 𝑦 ↔ (𝑔‘𝑘) ⊆ 𝑦))
131	130	rexrn 7079	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn ℕ → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
132	129, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
133	127, 132	bitr3d 281	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
134	133	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
135		elfz1end 13529	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (1...𝑘))
136		fz1ssnn 13530	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑘) ⊆ ℕ
137	53	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → dom 𝑔 = ℕ)
138	136, 137	sseqtrrid 4028	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (1...𝑘) ⊆ dom 𝑔)
139		funfvima2 7225	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑔 ∧ (1...𝑘) ⊆ dom 𝑔) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
140	67, 138, 139	syl2an2r 682	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
141	140	imp 406	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ (1...𝑘)) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
142	135, 141	sylan2b 593	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
143		intss1 4958	. . . . . . . . . . . . . 14 ⊢ ((𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)) → ∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘))
144		sstr2 3982	. . . . . . . . . . . . . 14 ⊢ (∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
145	142, 143, 144	3syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
146	145	reximdva 3160	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
147	134, 146	sylbid 239	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
148	126, 147	biimtrrid 242	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
149	124, 148	syld 47	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
150	98	sseq1d 4006	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
151	150	rexbidva 3168	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
152	151	adantr 480	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
153	149, 152	sylibrd 259	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
154	153	ralrimiva 3138	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
155		nnex 12216	. . . . . . . . 9 ⊢ ℕ ∈ V
156	155	mptex 7217	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) ∈ V
157		feq1 6689	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓:ℕ⟶𝐽 ↔ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽))
158		fveq1 6881	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘𝑘) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
159	158	eleq2d 2811	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝐴 ∈ (𝑓‘𝑘) ↔ 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
160		fveq1 6881	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)))
161	160, 158	sseq12d 4008	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
162	159, 161	anbi12d 630	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
163	162	ralbidv 3169	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
164	158	sseq1d 4006	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘𝑘) ⊆ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
165	164	rexbidv 3170	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
166	165	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
167	166	ralbidv 3169	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
168	157, 163, 167	3anbi123d 1432	. . . . . . . 8 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))))
169	156, 168	spcev 3588	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
170	75, 116, 154, 169	syl3anc 1368	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
171	170	expr 456	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
172	171	adantrrl 721	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
173	172	exlimdv 1928	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
174	39, 173	mpd 15	. 2 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
175	2, 174	rexlimddv 3153	1 ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2932  ∀wral 3053  ∃wrex 3062  {crab 3424  Vcvv 3466   ∩ cin 3940   ⊆ wss 3941  ∅c0 4315  𝒫 cpw 4595  ∪ cuni 4900  ∩ cint 4941   class class class wbr 5139   ↦ cmpt 5222  dom cdm 5667  ran crn 5668   ↾ cres 5669   “ cima 5670  Fun wfun 6528   Fn wfn 6529  ⟶wf 6530  –onto→wfo 6532  ‘cfv 6534  (class class class)co 7402  ωcom 7849   ≈ cen 8933   ≼ cdom 8934   ≺ csdm 8935  Fincfn 8936  1c1 11108   + caddc 11110  ℕcn 12210  ...cfz 13482  Topctop 22719  1^stωc1stc 23265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-nn 12211  df-n0 12471  df-z 12557  df-uz 12821  df-fz 13483  df-top 22720  df-1stc 23267

This theorem is referenced by:  1stcelcls  23289