Theorem 1stcfb 21757

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 21756	. 2 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
3		simplr 756	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐴 ∈ 𝑋)
4		eleq2 2854	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋))
5		sseq2 3883	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑋 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑋))
6	5	anbi2d 619	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
7	6	rexbidv 3242	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑋 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
8	4, 7	imbi12d 337	. . . . . . . . . 10 ⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))))
9		simprrr 769	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
10		1stctop 21755	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ 1st𝜔 → 𝐽 ∈ Top)
11	10	ad2antrr 713	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝐽 ∈ Top)
12	1	topopn 21218	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽)
13	11, 12	syl 17	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑋 ∈ 𝐽)
14	8, 9, 13	rspcdva 3541	. . . . . . . . 9 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝐴 ∈ 𝑋 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋)))
15	3, 14	mpd 15	. . . . . . . 8 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋))
16		simpl 475	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → 𝐴 ∈ 𝑤)
17	16	reximi 3190	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑋) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
18	15, 17	syl 17	. . . . . . 7 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤)
19		eleq2w 2849	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑎))
20	19	cbvrexv 3384	. . . . . . 7 ⊢ (∃𝑤 ∈ 𝑥 𝐴 ∈ 𝑤 ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
21	18, 20	sylib 210	. . . . . 6 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
22		rabn0 4225	. . . . . 6 ⊢ ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝑥 𝐴 ∈ 𝑎)
23	21, 22	sylibr 226	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
24		vex 3418	. . . . . . 7 ⊢ 𝑥 ∈ V
25	24	rabex 5091	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∈ V
26	25	0sdom 8444	. . . . 5 ⊢ (∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ↔ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≠ ∅)
27	23, 26	sylibr 226	. . . 4 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
28		ssrab2 3946	. . . . . 6 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥
29		ssdomg 8352	. . . . . 6 ⊢ (𝑥 ∈ V → ({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝑥 → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥))
30	24, 28, 29	mp2 9	. . . . 5 ⊢ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥
31		simprrl 768	. . . . . 6 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ω)
32		nnenom 13163	. . . . . . 7 ⊢ ℕ ≈ ω
33	32	ensymi 8356	. . . . . 6 ⊢ ω ≈ ℕ
34		domentr 8365	. . . . . 6 ⊢ ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
35	31, 33, 34	sylancl 577	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → 𝑥 ≼ ℕ)
36		domtr 8359	. . . . 5 ⊢ (({𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ 𝑥 ∧ 𝑥 ≼ ℕ) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
37	30, 35, 36	sylancr 578	. . . 4 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ)
38		fodomr 8464	. . . 4 ⊢ ((∅ ≺ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ∧ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
39	27, 37, 38	syl2anc 576	. . 3 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
40	10	ad3antrrr 717	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → 𝐽 ∈ Top)
41		imassrn 5781	. . . . . . . . . 10 ⊢ (𝑔 “ (1...𝑛)) ⊆ ran 𝑔
42		forn 6422	. . . . . . . . . . . . 13 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
43	42	ad2antll 716	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
44		simprll 766	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ∈ 𝒫 𝐽)
45	44	elpwid 4434	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑥 ⊆ 𝐽)
46	28, 45	syl5ss 3869	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} ⊆ 𝐽)
47	43, 46	eqsstrd 3895	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ran 𝑔 ⊆ 𝐽)
48	47	adantr 473	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ran 𝑔 ⊆ 𝐽)
49	41, 48	syl5ss 3869	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ⊆ 𝐽)
50		fz1ssnn 12754	. . . . . . . . . . . . . 14 ⊢ (1...𝑛) ⊆ ℕ
51		fof 6419	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
52	51	ad2antll 716	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔:ℕ⟶{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
53	52	fdmd 6353	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → dom 𝑔 = ℕ)
54	50, 53	syl5sseqr 3910	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (1...𝑛) ⊆ dom 𝑔)
55	54	adantr 473	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ dom 𝑔)
56		sseqin2 4079	. . . . . . . . . . . 12 ⊢ ((1...𝑛) ⊆ dom 𝑔 ↔ (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
57	55, 56	sylib 210	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
58		elfz1end 12753	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
59		ne0i 4186	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...𝑛) → (1...𝑛) ≠ ∅)
60	59	adantl 474	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ (1...𝑛)) → (1...𝑛) ≠ ∅)
61	58, 60	sylan2b 584	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ≠ ∅)
62	57, 61	eqnetrd 3034	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
63		imadisj 5788	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑛)) = ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) = ∅)
64	63	necon3bii 3019	. . . . . . . . . 10 ⊢ ((𝑔 “ (1...𝑛)) ≠ ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
65	62, 64	sylibr 226	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ≠ ∅)
66		fzfid 13156	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
67	52	ffund 6348	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → Fun 𝑔)
68		fores 6429	. . . . . . . . . . 11 ⊢ ((Fun 𝑔 ∧ (1...𝑛) ⊆ dom 𝑔) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
69	67, 55, 68	syl2an2r 672	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
70		fofi 8605	. . . . . . . . . 10 ⊢ (((1...𝑛) ∈ Fin ∧ (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛))) → (𝑔 “ (1...𝑛)) ∈ Fin)
71	66, 69, 70	syl2anc 576	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ Fin)
72		fiinopn 21213	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽))
73	72	imp 398	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin)) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
74	40, 49, 65, 71, 73	syl13anc 1352	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑛 ∈ ℕ) → ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
75	74	fmpttd 6702	. . . . . . 7 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽)
76		imassrn 5781	. . . . . . . . . . . . 13 ⊢ (𝑔 “ (1...𝑘)) ⊆ ran 𝑔
77	43	adantr 473	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ran 𝑔 = {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
78	76, 77	syl5sseq 3909	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})
79		id 22	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
80	79	rgenw 3100	. . . . . . . . . . . . 13 ⊢ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛)
81		eleq2w 2849	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑛 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑛))
82	81	ralrab 3601	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 ↔ ∀𝑛 ∈ 𝑥 (𝐴 ∈ 𝑛 → 𝐴 ∈ 𝑛))
83	80, 82	mpbir 223	. . . . . . . . . . . 12 ⊢ ∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛
84		ssralv 3923	. . . . . . . . . . . 12 ⊢ ((𝑔 “ (1...𝑘)) ⊆ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → (∀𝑛 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝐴 ∈ 𝑛 → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
85	78, 83, 84	mpisyl 21	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛)
86		elintg 4757	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
87	86	ad3antlr 718	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ∩ (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴 ∈ 𝑛))
88	85, 87	mpbird 249	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ∩ (𝑔 “ (1...𝑘)))
89		eqid 2778	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))
90		oveq2 6984	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
91	90	imaeq2d 5770	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
92	91	inteqd 4754	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...𝑘)))
93		simpr 477	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
94	74	ralrimiva 3132	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽)
95	92	eleq1d 2850	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽))
96	95	rspccva 3534	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
97	94, 96	sylan 572	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...𝑘)) ∈ 𝐽)
98	89, 92, 93, 97	fvmptd3 6617	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) = ∩ (𝑔 “ (1...𝑘)))
99	88, 98	eleqtrrd 2869	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
100		fzssp1 12766	. . . . . . . . . . . 12 ⊢ (1...𝑘) ⊆ (1...(𝑘 + 1))
101		imass2 5805	. . . . . . . . . . . 12 ⊢ ((1...𝑘) ⊆ (1...(𝑘 + 1)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
102	100, 101	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
103		intss 4770	. . . . . . . . . . 11 ⊢ ((𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
104	102, 103	syl 17	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ⊆ ∩ (𝑔 “ (1...𝑘)))
105		oveq2 6984	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
106	105	imaeq2d 5770	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
107	106	inteqd 4754	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑘 + 1) → ∩ (𝑔 “ (1...𝑛)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
108		peano2nn 11453	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
109	108	adantl 474	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
110	107	eleq1d 2850	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑘 + 1) → (∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ↔ ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽))
111	110	rspccva 3534	. . . . . . . . . . . 12 ⊢ ((∀𝑛 ∈ ℕ ∩ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ (𝑘 + 1) ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
112	94, 108, 111	syl2an 586	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ∩ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
113	89, 107, 109, 112	fvmptd3 6617	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = ∩ (𝑔 “ (1...(𝑘 + 1))))
114	104, 113, 98	3sstr4d 3904	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
115	99, 114	jca 504	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
116	115	ralrimiva 3132	. . . . . . 7 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
117		simprlr 767	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
118		eleq2w 2849	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦))
119		sseq2 3883	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑦 → (𝑤 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑦))
120	119	anbi2d 619	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
121	120	rexbidv 3242	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
122	118, 121	imbi12d 337	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ((𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))))
123	122	rspccva 3534	. . . . . . . . . . 11 ⊢ ((∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
124	117, 123	sylan 572	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)))
125		eleq2w 2849	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
126	125	rexrab 3603	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦))
127	43	rexeqdv 3356	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦))
128		fofn 6421	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → 𝑔 Fn ℕ)
129	128	ad2antll 716	. . . . . . . . . . . . . . 15 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → 𝑔 Fn ℕ)
130		sseq1 3882	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = (𝑔‘𝑘) → (𝑤 ⊆ 𝑦 ↔ (𝑔‘𝑘) ⊆ 𝑦))
131	130	rexrn 6678	. . . . . . . . . . . . . . 15 ⊢ (𝑔 Fn ℕ → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
132	129, 131	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
133	127, 132	bitr3d 273	. . . . . . . . . . . . 13 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
134	133	adantr 473	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦))
135		elfz1end 12753	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈ (1...𝑘))
136		fz1ssnn 12754	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑘) ⊆ ℕ
137	53	adantr 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → dom 𝑔 = ℕ)
138	136, 137	syl5sseqr 3910	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (1...𝑘) ⊆ dom 𝑔)
139		funfvima2 6819	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑔 ∧ (1...𝑘) ⊆ dom 𝑔) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
140	67, 138, 139	syl2an2r 672	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝑘 ∈ (1...𝑘) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘))))
141	140	imp 398	. . . . . . . . . . . . . . 15 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ (1...𝑘)) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
142	135, 141	sylan2b 584	. . . . . . . . . . . . . 14 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → (𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)))
143		intss1 4764	. . . . . . . . . . . . . 14 ⊢ ((𝑔‘𝑘) ∈ (𝑔 “ (1...𝑘)) → ∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘))
144		sstr2 3865	. . . . . . . . . . . . . 14 ⊢ (∩ (𝑔 “ (1...𝑘)) ⊆ (𝑔‘𝑘) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
145	142, 143, 144	3syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑔‘𝑘) ⊆ 𝑦 → ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
146	145	reximdva 3219	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ (𝑔‘𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
147	134, 146	sylbid 232	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ {𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎}𝑤 ⊆ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
148	126, 147	syl5bir 235	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
149	124, 148	syld 47	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
150	98	sseq1d 3888	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
151	150	rexbidva 3241	. . . . . . . . . 10 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
152	151	adantr 473	. . . . . . . . 9 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ∩ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
153	149, 152	sylibrd 251	. . . . . . . 8 ⊢ ((((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) ∧ 𝑦 ∈ 𝐽) → (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
154	153	ralrimiva 3132	. . . . . . 7 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
155		nnex 11446	. . . . . . . . 9 ⊢ ℕ ∈ V
156	155	mptex 6812	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) ∈ V
157		feq1 6325	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓:ℕ⟶𝐽 ↔ (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽))
158		fveq1 6498	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘𝑘) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))
159	158	eleq2d 2851	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝐴 ∈ (𝑓‘𝑘) ↔ 𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
160		fveq1 6498	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (𝑓‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)))
161	160, 158	sseq12d 3890	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)))
162	159, 161	anbi12d 621	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
163	162	ralbidv 3147	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ↔ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘))))
164	158	sseq1d 3888	. . . . . . . . . . . 12 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓‘𝑘) ⊆ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
165	164	rexbidv 3242	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
166	165	imbi2d 333	. . . . . . . . . 10 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
167	166	ralbidv 3147	. . . . . . . . 9 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → (∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
168	157, 163, 167	3anbi123d 1415	. . . . . . . 8 ⊢ (𝑓 = (𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))) → ((𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)) ↔ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))))
169	156, 168	spcev 3525	. . . . . . 7 ⊢ (((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ ∩ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
170	75, 116, 154, 169	syl3anc 1351	. . . . . 6 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ∧ 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎})) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
171	170	expr 449	. . . . 5 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
172	171	adantrrl 711	. . . 4 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
173	172	exlimdv 1892	. . 3 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → (∃𝑔 𝑔:ℕ–onto→{𝑎 ∈ 𝑥 ∣ 𝐴 ∈ 𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))))
174	39, 173	mpd 15	. 2 ⊢ (((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 → ∃𝑤 ∈ 𝑥 (𝐴 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
175	2, 174	rexlimddv 3236	1 ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507  ∃wex 1742   ∈ wcel 2050   ≠ wne 2967  ∀wral 3088  ∃wrex 3089  {crab 3092  Vcvv 3415   ∩ cin 3828   ⊆ wss 3829  ∅c0 4178  𝒫 cpw 4422  ∪ cuni 4712  ∩ cint 4749   class class class wbr 4929   ↦ cmpt 5008  dom cdm 5407  ran crn 5408   ↾ cres 5409   “ cima 5410  Fun wfun 6182   Fn wfn 6183  ⟶wf 6184  –onto→wfo 6186  ‘cfv 6188  (class class class)co 6976  ωcom 7396   ≈ cen 8303   ≼ cdom 8304   ≺ csdm 8305  Fincfn 8306  1c1 10336   + caddc 10338  ℕcn 11439  ...cfz 12708  Topctop 21205  1^st𝜔c1stc 21749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-oadd 7909  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-nn 11440  df-n0 11708  df-z 11794  df-uz 12059  df-fz 12709  df-top 21206  df-1stc 21751

This theorem is referenced by:  1stcelcls  21773