Theorem 1stcfb 23654

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 23653	. 2 ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
3		simplr 781	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐴 ∈ 𝑋)
4		eleq2 2854	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
5		sseq2 3964	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑋 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑋))
6	5	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
7	6	rexbidv 3191	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
8	4, 7	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))))
9		simprrr 794	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
10		1stctop 23652	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
11	10	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐽 ∈ Top)
12	1	topopn 23115	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
13	11, 12	syl 18	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑋 ∈ 𝐽)
14	8, 9, 13	rspcdva 3584	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
15	3, 14	mpd 16	. . . . . . . 8 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))
16		simpl 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → 𝐴 ∈ 𝑤)
17	16	reximi 3105	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
18	15, 17	syl 18	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
19		eleq2w 2849	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑎))
20	19	cbvrexvw 3246	. . . . . . 7 ⊢ (∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤 ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
21	18, 20	sylib 221	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
22		rabn0 4346	. . . . . 6 ⊢ ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
23	21, 22	sylibr 237	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
24		vex 3461	. . . . . . 7 ⊢ 𝑥 ∈ V
25	24	rabex 5311	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∈ V
26	25	0sdom 9103	. . . . 5 ⊢ (∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ↔ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
27	23, 26	sylibr 237	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
28		ssrab2 4035	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥
29		ssdomg 9003	. . . . . 6 ⊢ (𝑥 ∈ V → ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥 → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥))
30	24, 28, 29	mp2 9	. . . . 5 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥
31		simprrl 793	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ω)
32		nnenom 14036	. . . . . . 7 ⊢ ℕ ≈ ω
33	32	ensymi 9007	. . . . . 6 ⊢ ω ≈ ℕ
34		domentr 9016	. . . . . 6 ⊢ ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
35	31, 33, 34	sylancl 598	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ℕ)
36		domtr 9010	. . . . 5 ⊢ (({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥 ∧ 𝑥 ≼ ℕ) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
37	30, 35, 36	sylancr 599	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
38		fodomr 9123	. . . 4 ⊢ ((∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∧ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
39	27, 37, 38	syl2anc 596	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
40	10	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → 𝐽 ∈ Top)
41		imassrn 6075	. . . . . . . . . 10 ⊢ (𝑔 “ (1...𝑛)) ⊆ ran 𝑔
42		forn 6799	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
43	42	ad2antll 742	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
44		simprll 791	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ∈ 𝒫 𝐽)
45	44	elpwid 4573	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ⊆ 𝐽)
46	28, 45	sstrid 3949	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝐽)
47	43, 46	eqsstrd 3972	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 ⊆ 𝐽)
48	47	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ran 𝑔 ⊆ 𝐽)
49	41, 48	sstrid 3949	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ⊆ 𝐽)
50		fz1ssnn 13602	. . . . . . . . . . . . . 14 ⊢ (1...𝑛) ⊆ ℕ
51		fof 6796	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
52	51	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
53	52	fdmd 6720	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → dom 𝑔 = ℕ)
54	50, 53	sseqtrrid 3981	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (1...𝑛) ⊆ dom 𝑔)
55	54	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ dom 𝑔)
56		sseqin2 4176	. . . . . . . . . . . 12 ⊢ ((1...𝑛) ⊆ dom 𝑔 ↔ (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
57	55, 56	sylib 221	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
58		elfz1end 13601	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
59		ne0i 4294	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑛) → (1...𝑛) ≠ ∅)
60	59	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ (1...𝑛)) → (1...𝑛) ≠ ∅)
61	58, 60	sylan2b 606	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ≠ ∅)
62	57, 61	eqnetrd 3027	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
63		imadisj 6084	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑛)) = ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) = ∅)
64	63	necon3bii 3012	. . . . . . . . . 10 ⊢ ((𝑔 “ (1...𝑛)) ≠ ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
65	62, 64	sylibr 237	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ≠ ∅)
66		fzfid 14029	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
67	52	ffund 6714	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → Fun 𝑔)
68		fores 6806	. . . . . . . . . . 11 ⊢ ((Fun 𝑔 ∧ (1...𝑛) ⊆ dom 𝑔) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
69	67, 55, 68	syl2an2r 698	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
70		fofi 9280	. . . . . . . . . 10 ⊢ (((1...𝑛) ∈ Fin ∧ (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛))) → (𝑔 “ (1...𝑛)) ∈ Fin)
71	66, 69, 70	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ Fin)
72		fiinopn 23110	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽))
73	72	imp 412	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin)) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
74	40, 49, 65, 71, 73	syl13anc 1399	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
75	74	fmpttd 7114	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽)
76		imassrn 6075	. . . . . . . . . . . . 13 ⊢ (𝑔 “ (1...𝑘)) ⊆ ran 𝑔
77	43	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
78	76, 77	sseqtrid 3980	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
79		id 23	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
80	79	rgenw 3085	. . . . . . . . . . . . 13 ⊢ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
81		eleq2w 2849	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑛 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑛))
82	81	ralrab 3659	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 ↔ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛))
83	80, 82	mpbir 234	. . . . . . . . . . . 12 ⊢ ∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛
84		ssralv 4007	. . . . . . . . . . . 12 ⊢ ((𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
85	78, 83, 84	mpisyl 22	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛)
86		elintg 4922	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
87	86	ad3antlr 744	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
88	85, 87	mpbird 260	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ∩ (𝑔 “ (1...𝑘)))
89		eqid 2765	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))
90		oveq2 7427	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
91	90	imaeq2d 6064	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
92	91	inteqd 4919	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...𝑘)))
93		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
94	74	ralrimiva 3159	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
95	92	eleq1d 2850	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽))
96	95	rspccva 3582	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
97	94, 96	sylan 592	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
98	89, 92, 93, 97	fvmptd3 7017	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) = ∩ (𝑔 “ (1...𝑘)))
99	88, 98	eleqtrrd 2868	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
100		fzssp1 13614	. . . . . . . . . . . 12 ⊢ (1...𝑘) ⊆ (1...(𝑘 + 1))
101		imass2 6106	. . . . . . . . . . . 12 ⊢ ((1...𝑘) ⊆ (1...(𝑘 + 1)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
102	100, 101	mp1i 14	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
103		intss 4936	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
104	102, 103	syl 18	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
105		oveq2 7427	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
106	105	imaeq2d 6064	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
107	106	inteqd 4919	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
108		peano2nn 12262	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
109	108	adantl 487	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
110	107	eleq1d 2850	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽))
111	110	rspccva 3582	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ (𝑘 + 1) ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
112	94, 108, 111	syl2an 608	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
113	89, 107, 109, 112	fvmptd3 7017	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
114	104, 113, 98	3sstr4d 3993	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
115	99, 114	jca 521	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
116	115	ralrimiva 3159	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
117		simprlr 792	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
118		eleq2w 2849	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦))
119		sseq2 3964	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑦))
120	119	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
121	120	rexbidv 3191	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
122	118, 121	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))))
123	122	rspccva 3582	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
124	117, 123	sylan 592	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
125		eleq2w 2849	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
126	125	rexrab 3661	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))
127	43	rexeqdv 3326	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦))
128		fofn 6798	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔 Fn ℕ)
129	128	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔 Fn ℕ)
130		sseq1 3963	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑔‘𝑘) → (𝑤 ⊆ 𝑦 ↔ (𝑔‘𝑘) ⊆ 𝑦))
131	130	rexrn 7086	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn ℕ → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
132	129, 131	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
133	127, 132	bitr3d 284	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
134	133	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
135		elfz1end 13601	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (1...𝑘))
136		fz1ssnn 13602	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑘) ⊆ ℕ
137	53	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → dom 𝑔 = ℕ)
138	136, 137	sseqtrrid 3981	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (1...𝑘) ⊆ dom 𝑔)
139		funfvima2 7236	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑔 ∧ (1...𝑘) ⊆ dom 𝑔) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
140	67, 138, 139	syl2an2r 698	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
141	140	imp 412	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ (1...𝑘)) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
142	135, 141	sylan2b 606	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
143		intss1 4930	. . . . . . . . . . . . . 14 ⊢ ((𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)) → ∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘))
144		sstr2 3945	. . . . . . . . . . . . . 14 ⊢ (∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
145	142, 143, 144	3syl 19	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
146	145	reximdva 3180	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
147	134, 146	sylbid 243	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
148	126, 147	biimtrrid 246	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
149	124, 148	syld 48	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
150	98	sseq1d 3969	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
151	150	rexbidva 3189	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
152	151	adantr 486	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
153	149, 152	sylibrd 262	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
154	153	ralrimiva 3159	. . . . . . 7 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
155		nnex 12256	. . . . . . . . 9 ⊢ ℕ ∈ V
156	155	mptex 7228	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) ∈ V
157		feq1 6687	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓:ℕ⟶𝐽 ↔ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽))
158		fveq1 6884	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘𝑘) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
159	158	eleq2d 2851	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝐴 ∈ (𝑓‘𝑘) ↔ 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
160		fveq1 6884	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)))
161	160, 158	sseq12d 3971	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
162	159, 161	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
163	162	ralbidv 3190	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
164	158	sseq1d 3969	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘𝑘) ⊆ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
165	164	rexbidv 3191	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
166	165	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
167	166	ralbidv 3190	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
168	157, 163, 167	3anbi123d 1464	. . . . . . . 8 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))))
169	156, 168	spcev 3567	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
170	75, 116, 154, 169	syl3anc 1398	. . . . . 6 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
171	170	expr 462	. . . . 5 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
172	171	adantrrl 737	. . . 4 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
173	172	exlimdv 1966	. . 3 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
174	39, 173	mpd 16	. 2 ⊢ (((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
175	2, 174	rexlimddv 3174	1 ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  {crab 3418  Vcvv 3457   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  ∪ cuni 4874  ∩ cint 4914   class class class wbr 5111   ↦ cmpt 5194  dom cdm 5663  ran crn 5664   ↾ cres 5665   “ cima 5666  Fun wfun 6534   Fn wfn 6535  ⟶wf 6536  –onto→wfo 6538  ‘cfv 6540  (class class class)co 7419  ωcom 7868   ≈ cen 8946   ≼ cdom 8947   ≺ csdm 8948  Fincfn 8949  1c1 11118   + caddc 11120  ℕcn 12250  ...cfz 13553  Topctop 23102  1^stωc1stc 23646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-inf2 9617  ax-cnex 11173  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-1st 7992  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-fin 8953  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-nn 12251  df-n0 12522  df-z 12609  df-uz 12881  df-fz 13554  df-top 23103  df-1stc 23648

This theorem is used by:  1stcelcls  23671