Theorem 1stcfb 22296

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 22295	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
3		simplr 769	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐴 ∈ 𝑋)
4		eleq2 2819	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
5		sseq2 3913	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑋 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑋))
6	5	anbi2d 632	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
7	6	rexbidv 3206	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
8	4, 7	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))))
9		simprrr 782	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
10		1stctop 22294	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
11	10	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐽 ∈ Top)
12	1	topopn 21757	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
13	11, 12	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑋 ∈ 𝐽)
14	8, 9, 13	rspcdva 3529	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
15	3, 14	mpd 15	. . . . . . . 8 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))
16		simpl 486	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → 𝐴 ∈ 𝑤)
17	16	reximi 3156	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
18	15, 17	syl 17	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
19		eleq2w 2814	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑎))
20	19	cbvrexvw 3349	. . . . . . 7 ⊢ (∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤 ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
21	18, 20	sylib 221	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
22		rabn0 4286	. . . . . 6 ⊢ ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
23	21, 22	sylibr 237	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
24		vex 3402	. . . . . . 7 ⊢ 𝑥 ∈ V
25	24	rabex 5210	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∈ V
26	25	0sdom 8755	. . . . 5 ⊢ (∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ↔ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
27	23, 26	sylibr 237	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
28		ssrab2 3979	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥
29		ssdomg 8652	. . . . . 6 ⊢ (𝑥 ∈ V → ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥 → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥))
30	24, 28, 29	mp2 9	. . . . 5 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥
31		simprrl 781	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ω)
32		nnenom 13518	. . . . . . 7 ⊢ ℕ ≈ ω
33	32	ensymi 8656	. . . . . 6 ⊢ ω ≈ ℕ
34		domentr 8665	. . . . . 6 ⊢ ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
35	31, 33, 34	sylancl 589	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ℕ)
36		domtr 8659	. . . . 5 ⊢ (({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥 ∧ 𝑥 ≼ ℕ) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
37	30, 35, 36	sylancr 590	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
38		fodomr 8775	. . . 4 ⊢ ((∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∧ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
39	27, 37, 38	syl2anc 587	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
40	10	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → 𝐽 ∈ Top)
41		imassrn 5925	. . . . . . . . . 10 ⊢ (𝑔 “ (1...𝑛)) ⊆ ran 𝑔
42		forn 6614	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
43	42	ad2antll 729	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
44		simprll 779	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ∈ 𝒫 𝐽)
45	44	elpwid 4510	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ⊆ 𝐽)
46	28, 45	sstrid 3898	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝐽)
47	43, 46	eqsstrd 3925	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 ⊆ 𝐽)
48	47	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ran 𝑔 ⊆ 𝐽)
49	41, 48	sstrid 3898	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ⊆ 𝐽)
50		fz1ssnn 13108	. . . . . . . . . . . . . 14 ⊢ (1...𝑛) ⊆ ℕ
51		fof 6611	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
52	51	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
53	52	fdmd 6534	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → dom 𝑔 = ℕ)
54	50, 53	sseqtrrid 3940	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (1...𝑛) ⊆ dom 𝑔)
55	54	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ dom 𝑔)
56		sseqin2 4116	. . . . . . . . . . . 12 ⊢ ((1...𝑛) ⊆ dom 𝑔 ↔ (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
57	55, 56	sylib 221	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
58		elfz1end 13107	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
59		ne0i 4235	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑛) → (1...𝑛) ≠ ∅)
60	59	adantl 485	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ (1...𝑛)) → (1...𝑛) ≠ ∅)
61	58, 60	sylan2b 597	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ≠ ∅)
62	57, 61	eqnetrd 2999	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
63		imadisj 5933	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑛)) = ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) = ∅)
64	63	necon3bii 2984	. . . . . . . . . 10 ⊢ ((𝑔 “ (1...𝑛)) ≠ ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
65	62, 64	sylibr 237	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ≠ ∅)
66		fzfid 13511	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
67	52	ffund 6527	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → Fun 𝑔)
68		fores 6621	. . . . . . . . . . 11 ⊢ ((Fun 𝑔 ∧ (1...𝑛) ⊆ dom 𝑔) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
69	67, 55, 68	syl2an2r 685	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
70		fofi 8940	. . . . . . . . . 10 ⊢ (((1...𝑛) ∈ Fin ∧ (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛))) → (𝑔 “ (1...𝑛)) ∈ Fin)
71	66, 69, 70	syl2anc 587	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ Fin)
72		fiinopn 21752	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽))
73	72	imp 410	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin)) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
74	40, 49, 65, 71, 73	syl13anc 1374	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
75	74	fmpttd 6910	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽)
76		imassrn 5925	. . . . . . . . . . . . 13 ⊢ (𝑔 “ (1...𝑘)) ⊆ ran 𝑔
77	43	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
78	76, 77	sseqtrid 3939	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
79		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
80	79	rgenw 3063	. . . . . . . . . . . . 13 ⊢ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
81		eleq2w 2814	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑛 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑛))
82	81	ralrab 3596	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 ↔ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛))
83	80, 82	mpbir 234	. . . . . . . . . . . 12 ⊢ ∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛
84		ssralv 3953	. . . . . . . . . . . 12 ⊢ ((𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
85	78, 83, 84	mpisyl 21	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛)
86		elintg 4853	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
87	86	ad3antlr 731	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
88	85, 87	mpbird 260	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ∩ (𝑔 “ (1...𝑘)))
89		eqid 2736	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))
90		oveq2 7199	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
91	90	imaeq2d 5914	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
92	91	inteqd 4850	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...𝑘)))
93		simpr 488	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
94	74	ralrimiva 3095	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
95	92	eleq1d 2815	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽))
96	95	rspccva 3526	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
97	94, 96	sylan 583	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
98	89, 92, 93, 97	fvmptd3 6819	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) = ∩ (𝑔 “ (1...𝑘)))
99	88, 98	eleqtrrd 2834	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
100		fzssp1 13120	. . . . . . . . . . . 12 ⊢ (1...𝑘) ⊆ (1...(𝑘 + 1))
101		imass2 5950	. . . . . . . . . . . 12 ⊢ ((1...𝑘) ⊆ (1...(𝑘 + 1)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
102	100, 101	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
103		intss 4866	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
104	102, 103	syl 17	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
105		oveq2 7199	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
106	105	imaeq2d 5914	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
107	106	inteqd 4850	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
108		peano2nn 11807	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
109	108	adantl 485	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
110	107	eleq1d 2815	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽))
111	110	rspccva 3526	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ (𝑘 + 1) ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
112	94, 108, 111	syl2an 599	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
113	89, 107, 109, 112	fvmptd3 6819	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
114	104, 113, 98	3sstr4d 3934	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
115	99, 114	jca 515	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
116	115	ralrimiva 3095	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
117		simprlr 780	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
118		eleq2w 2814	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦))
119		sseq2 3913	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑦))
120	119	anbi2d 632	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
121	120	rexbidv 3206	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
122	118, 121	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))))
123	122	rspccva 3526	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
124	117, 123	sylan 583	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
125		eleq2w 2814	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
126	125	rexrab 3598	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))
127	43	rexeqdv 3316	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦))
128		fofn 6613	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔 Fn ℕ)
129	128	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔 Fn ℕ)
130		sseq1 3912	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑔‘𝑘) → (𝑤 ⊆ 𝑦 ↔ (𝑔‘𝑘) ⊆ 𝑦))
131	130	rexrn 6884	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn ℕ → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
132	129, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
133	127, 132	bitr3d 284	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
134	133	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
135		elfz1end 13107	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (1...𝑘))
136		fz1ssnn 13108	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑘) ⊆ ℕ
137	53	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → dom 𝑔 = ℕ)
138	136, 137	sseqtrrid 3940	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (1...𝑘) ⊆ dom 𝑔)
139		funfvima2 7025	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑔 ∧ (1...𝑘) ⊆ dom 𝑔) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
140	67, 138, 139	syl2an2r 685	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
141	140	imp 410	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ (1...𝑘)) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
142	135, 141	sylan2b 597	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
143		intss1 4860	. . . . . . . . . . . . . 14 ⊢ ((𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)) → ∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘))
144		sstr2 3894	. . . . . . . . . . . . . 14 ⊢ (∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
145	142, 143, 144	3syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
146	145	reximdva 3183	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
147	134, 146	sylbid 243	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
148	126, 147	syl5bir 246	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
149	124, 148	syld 47	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
150	98	sseq1d 3918	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
151	150	rexbidva 3205	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
152	151	adantr 484	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
153	149, 152	sylibrd 262	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
154	153	ralrimiva 3095	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
155		nnex 11801	. . . . . . . . 9 ⊢ ℕ ∈ V
156	155	mptex 7017	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) ∈ V
157		feq1 6504	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓:ℕ⟶𝐽 ↔ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽))
158		fveq1 6694	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘𝑘) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
159	158	eleq2d 2816	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝐴 ∈ (𝑓‘𝑘) ↔ 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
160		fveq1 6694	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)))
161	160, 158	sseq12d 3920	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
162	159, 161	anbi12d 634	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
163	162	ralbidv 3108	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
164	158	sseq1d 3918	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘𝑘) ⊆ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
165	164	rexbidv 3206	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
166	165	imbi2d 344	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
167	166	ralbidv 3108	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
168	157, 163, 167	3anbi123d 1438	. . . . . . . 8 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))))
169	156, 168	spcev 3511	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
170	75, 116, 154, 169	syl3anc 1373	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
171	170	expr 460	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
172	171	adantrrl 724	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
173	172	exlimdv 1941	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
174	39, 173	mpd 15	. 2 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
175	2, 174	rexlimddv 3200	1 ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543  ∃wex 1787   ∈ wcel 2112   ≠ wne 2932  ∀wral 3051  ∃wrex 3052  {crab 3055  Vcvv 3398   ∩ cin 3852   ⊆ wss 3853  ∅c0 4223  𝒫 cpw 4499  ∪ cuni 4805  ∩ cint 4845   class class class wbr 5039   ↦ cmpt 5120  dom cdm 5536  ran crn 5537   ↾ cres 5538   “ cima 5539  Fun wfun 6352   Fn wfn 6353  ⟶wf 6354  –onto→wfo 6356  ‘cfv 6358  (class class class)co 7191  ωcom 7622   ≈ cen 8601   ≼ cdom 8602   ≺ csdm 8603  Fincfn 8604  1c1 10695   + caddc 10697  ℕcn 11795  ...cfz 13060  Topctop 21744  1^stωc1stc 22288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-inf2 9234  ax-cnex 10750  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770  ax-pre-mulgt0 10771

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-int 4846  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-1st 7739  df-2nd 7740  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-1o 8180  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-fin 8608  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-sub 11029  df-neg 11030  df-nn 11796  df-n0 12056  df-z 12142  df-uz 12404  df-fz 13061  df-top 21745  df-1stc 22290

This theorem is referenced by:  1stcelcls  22312