MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1stcfb Structured version   Visualization version   GIF version

Theorem 1stcfb 21528
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.
StepHypRef Expression
1 1stcclb.1 . . 3 𝑋 = 𝐽
211stcclb 21527 . 2 ((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))
3 simplr 785 . . . . . . . . 9 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝐴𝑋)
4 eleq2 2833 . . . . . . . . . . 11 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
5 sseq2 3787 . . . . . . . . . . . . 13 (𝑧 = 𝑋 → (𝑤𝑧𝑤𝑋))
65anbi2d 622 . . . . . . . . . . . 12 (𝑧 = 𝑋 → ((𝐴𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝑋)))
76rexbidv 3199 . . . . . . . . . . 11 (𝑧 = 𝑋 → (∃𝑤𝑥 (𝐴𝑤𝑤𝑧) ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑋)))
84, 7imbi12d 335 . . . . . . . . . 10 (𝑧 = 𝑋 → ((𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ↔ (𝐴𝑋 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋))))
9 simprrr 800 . . . . . . . . . 10 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))
10 1stctop 21526 . . . . . . . . . . . 12 (𝐽 ∈ 1st𝜔 → 𝐽 ∈ Top)
1110ad2antrr 717 . . . . . . . . . . 11 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝐽 ∈ Top)
121topopn 20990 . . . . . . . . . . 11 (𝐽 ∈ Top → 𝑋𝐽)
1311, 12syl 17 . . . . . . . . . 10 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑋𝐽)
148, 9, 13rspcdva 3467 . . . . . . . . 9 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (𝐴𝑋 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋)))
153, 14mpd 15 . . . . . . . 8 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋))
16 simpl 474 . . . . . . . . 9 ((𝐴𝑤𝑤𝑋) → 𝐴𝑤)
1716reximi 3157 . . . . . . . 8 (∃𝑤𝑥 (𝐴𝑤𝑤𝑋) → ∃𝑤𝑥 𝐴𝑤)
1815, 17syl 17 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑤𝑥 𝐴𝑤)
19 eleq2w 2828 . . . . . . . 8 (𝑤 = 𝑎 → (𝐴𝑤𝐴𝑎))
2019cbvrexv 3320 . . . . . . 7 (∃𝑤𝑥 𝐴𝑤 ↔ ∃𝑎𝑥 𝐴𝑎)
2118, 20sylib 209 . . . . . 6 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑎𝑥 𝐴𝑎)
22 rabn0 4122 . . . . . 6 ({𝑎𝑥𝐴𝑎} ≠ ∅ ↔ ∃𝑎𝑥 𝐴𝑎)
2321, 22sylibr 225 . . . . 5 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → {𝑎𝑥𝐴𝑎} ≠ ∅)
24 vex 3353 . . . . . . 7 𝑥 ∈ V
2524rabex 4973 . . . . . 6 {𝑎𝑥𝐴𝑎} ∈ V
26250sdom 8298 . . . . 5 (∅ ≺ {𝑎𝑥𝐴𝑎} ↔ {𝑎𝑥𝐴𝑎} ≠ ∅)
2723, 26sylibr 225 . . . 4 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∅ ≺ {𝑎𝑥𝐴𝑎})
28 ssrab2 3847 . . . . . 6 {𝑎𝑥𝐴𝑎} ⊆ 𝑥
29 ssdomg 8206 . . . . . 6 (𝑥 ∈ V → ({𝑎𝑥𝐴𝑎} ⊆ 𝑥 → {𝑎𝑥𝐴𝑎} ≼ 𝑥))
3024, 28, 29mp2 9 . . . . 5 {𝑎𝑥𝐴𝑎} ≼ 𝑥
31 simprrl 799 . . . . . 6 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑥 ≼ ω)
32 nnenom 12987 . . . . . . 7 ℕ ≈ ω
3332ensymi 8210 . . . . . 6 ω ≈ ℕ
34 domentr 8219 . . . . . 6 ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
3531, 33, 34sylancl 580 . . . . 5 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑥 ≼ ℕ)
36 domtr 8213 . . . . 5 (({𝑎𝑥𝐴𝑎} ≼ 𝑥𝑥 ≼ ℕ) → {𝑎𝑥𝐴𝑎} ≼ ℕ)
3730, 35, 36sylancr 581 . . . 4 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → {𝑎𝑥𝐴𝑎} ≼ ℕ)
38 fodomr 8318 . . . 4 ((∅ ≺ {𝑎𝑥𝐴𝑎} ∧ {𝑎𝑥𝐴𝑎} ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})
3927, 37, 38syl2anc 579 . . 3 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})
4010ad3antrrr 721 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → 𝐽 ∈ Top)
41 imassrn 5659 . . . . . . . . . 10 (𝑔 “ (1...𝑛)) ⊆ ran 𝑔
42 forn 6301 . . . . . . . . . . . . 13 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ran 𝑔 = {𝑎𝑥𝐴𝑎})
4342ad2antll 720 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ran 𝑔 = {𝑎𝑥𝐴𝑎})
44 simprll 797 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑥 ∈ 𝒫 𝐽)
4544elpwid 4327 . . . . . . . . . . . . 13 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑥𝐽)
4628, 45syl5ss 3772 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → {𝑎𝑥𝐴𝑎} ⊆ 𝐽)
4743, 46eqsstrd 3799 . . . . . . . . . . 11 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ran 𝑔𝐽)
4847adantr 472 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → ran 𝑔𝐽)
4941, 48syl5ss 3772 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ⊆ 𝐽)
50 elfznn 12577 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
5150ssriv 3765 . . . . . . . . . . . . . 14 (1...𝑛) ⊆ ℕ
52 fof 6298 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → 𝑔:ℕ⟶{𝑎𝑥𝐴𝑎})
5352ad2antll 720 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑔:ℕ⟶{𝑎𝑥𝐴𝑎})
5453fdmd 6232 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → dom 𝑔 = ℕ)
5551, 54syl5sseqr 3814 . . . . . . . . . . . . 13 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (1...𝑛) ⊆ dom 𝑔)
5655adantr 472 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ dom 𝑔)
57 sseqin2 3979 . . . . . . . . . . . 12 ((1...𝑛) ⊆ dom 𝑔 ↔ (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
5856, 57sylib 209 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
59 elfz1end 12578 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
60 ne0i 4085 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑛) → (1...𝑛) ≠ ∅)
6160adantl 473 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ (1...𝑛)) → (1...𝑛) ≠ ∅)
6259, 61sylan2b 587 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ≠ ∅)
6358, 62eqnetrd 3004 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
64 imadisj 5666 . . . . . . . . . . 11 ((𝑔 “ (1...𝑛)) = ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) = ∅)
6564necon3bii 2989 . . . . . . . . . 10 ((𝑔 “ (1...𝑛)) ≠ ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
6663, 65sylibr 225 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ≠ ∅)
67 fzfid 12980 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
6853ffund 6227 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → Fun 𝑔)
6968adantr 472 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → Fun 𝑔)
70 fores 6307 . . . . . . . . . . 11 ((Fun 𝑔 ∧ (1...𝑛) ⊆ dom 𝑔) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
7169, 56, 70syl2anc 579 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
72 fofi 8459 . . . . . . . . . 10 (((1...𝑛) ∈ Fin ∧ (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛))) → (𝑔 “ (1...𝑛)) ∈ Fin)
7367, 71, 72syl2anc 579 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ Fin)
74 fiinopn 20985 . . . . . . . . . 10 (𝐽 ∈ Top → (((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin) → (𝑔 “ (1...𝑛)) ∈ 𝐽))
7574imp 395 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin)) → (𝑔 “ (1...𝑛)) ∈ 𝐽)
7640, 49, 66, 73, 75syl13anc 1491 . . . . . . . 8 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ 𝐽)
7776fmpttd 6575 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽)
78 imassrn 5659 . . . . . . . . . . . . 13 (𝑔 “ (1...𝑘)) ⊆ ran 𝑔
7943adantr 472 . . . . . . . . . . . . 13 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ran 𝑔 = {𝑎𝑥𝐴𝑎})
8078, 79syl5sseq 3813 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ {𝑎𝑥𝐴𝑎})
81 id 22 . . . . . . . . . . . . . 14 (𝐴𝑛𝐴𝑛)
8281rgenw 3071 . . . . . . . . . . . . 13 𝑛𝑥 (𝐴𝑛𝐴𝑛)
83 eleq2w 2828 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (𝐴𝑎𝐴𝑛))
8483ralrab 3525 . . . . . . . . . . . . 13 (∀𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛 ↔ ∀𝑛𝑥 (𝐴𝑛𝐴𝑛))
8582, 84mpbir 222 . . . . . . . . . . . 12 𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛
86 ssralv 3826 . . . . . . . . . . . 12 ((𝑔 “ (1...𝑘)) ⊆ {𝑎𝑥𝐴𝑎} → (∀𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛 → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
8780, 85, 86mpisyl 21 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛)
88 elintg 4641 . . . . . . . . . . . 12 (𝐴𝑋 → (𝐴 (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
8988ad3antlr 722 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
9087, 89mpbird 248 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 (𝑔 “ (1...𝑘)))
91 simpr 477 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
9276ralrimiva 3113 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽)
93 oveq2 6850 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
9493imaeq2d 5648 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
9594inteqd 4638 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
9695eleq1d 2829 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ( (𝑔 “ (1...𝑛)) ∈ 𝐽 (𝑔 “ (1...𝑘)) ∈ 𝐽))
9796rspccva 3460 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ∈ 𝐽)
9892, 97sylan 575 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ∈ 𝐽)
99 eqid 2765 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))
10095, 99fvmptg 6469 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (𝑔 “ (1...𝑘)) ∈ 𝐽) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) = (𝑔 “ (1...𝑘)))
10191, 98, 100syl2anc 579 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) = (𝑔 “ (1...𝑘)))
10290, 101eleqtrrd 2847 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
103 fzssp1 12591 . . . . . . . . . . . 12 (1...𝑘) ⊆ (1...(𝑘 + 1))
104 imass2 5683 . . . . . . . . . . . 12 ((1...𝑘) ⊆ (1...(𝑘 + 1)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
105103, 104mp1i 13 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
106 intss 4654 . . . . . . . . . . 11 ((𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))) → (𝑔 “ (1...(𝑘 + 1))) ⊆ (𝑔 “ (1...𝑘)))
107105, 106syl 17 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ⊆ (𝑔 “ (1...𝑘)))
108 peano2nn 11288 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
109108adantl 473 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
110 oveq2 6850 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
111110imaeq2d 5648 . . . . . . . . . . . . . . 15 (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
112111inteqd 4638 . . . . . . . . . . . . . 14 (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
113112eleq1d 2829 . . . . . . . . . . . . 13 (𝑛 = (𝑘 + 1) → ( (𝑔 “ (1...𝑛)) ∈ 𝐽 (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽))
114113rspccva 3460 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ (𝑘 + 1) ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
11592, 108, 114syl2an 589 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
116112, 99fvmptg 6469 . . . . . . . . . . 11 (((𝑘 + 1) ∈ ℕ ∧ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = (𝑔 “ (1...(𝑘 + 1))))
117109, 115, 116syl2anc 579 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = (𝑔 “ (1...(𝑘 + 1))))
118107, 117, 1013sstr4d 3808 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
119102, 118jca 507 . . . . . . . 8 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
120119ralrimiva 3113 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
121 simprlr 798 . . . . . . . . . . 11 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))
122 eleq2w 2828 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝐴𝑧𝐴𝑦))
123 sseq2 3787 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑤𝑧𝑤𝑦))
124123anbi2d 622 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐴𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝑦)))
125124rexbidv 3199 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (∃𝑤𝑥 (𝐴𝑤𝑤𝑧) ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
126122, 125imbi12d 335 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ((𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ↔ (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦))))
127126rspccva 3460 . . . . . . . . . . 11 ((∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
128121, 127sylan 575 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
129 eleq2w 2828 . . . . . . . . . . . 12 (𝑎 = 𝑤 → (𝐴𝑎𝐴𝑤))
130129rexrab 3527 . . . . . . . . . . 11 (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑦))
13143rexeqdv 3293 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦))
132 fofn 6300 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → 𝑔 Fn ℕ)
133132ad2antll 720 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑔 Fn ℕ)
134 sseq1 3786 . . . . . . . . . . . . . . . 16 (𝑤 = (𝑔𝑘) → (𝑤𝑦 ↔ (𝑔𝑘) ⊆ 𝑦))
135134rexrn 6551 . . . . . . . . . . . . . . 15 (𝑔 Fn ℕ → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
136133, 135syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
137131, 136bitr3d 272 . . . . . . . . . . . . 13 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
138137adantr 472 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
139 elfz1end 12578 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (1...𝑘))
14068adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → Fun 𝑔)
141 elfznn 12577 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
142141ssriv 3765 . . . . . . . . . . . . . . . . . 18 (1...𝑘) ⊆ ℕ
14354adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → dom 𝑔 = ℕ)
144142, 143syl5sseqr 3814 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (1...𝑘) ⊆ dom 𝑔)
145 funfvima2 6686 . . . . . . . . . . . . . . . . 17 ((Fun 𝑔 ∧ (1...𝑘) ⊆ dom 𝑔) → (𝑘 ∈ (1...𝑘) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘))))
146140, 144, 145syl2anc 579 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝑘 ∈ (1...𝑘) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘))))
147146imp 395 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ (1...𝑘)) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘)))
148139, 147sylan2b 587 . . . . . . . . . . . . . 14 (((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ ℕ) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘)))
149 intss1 4648 . . . . . . . . . . . . . 14 ((𝑔𝑘) ∈ (𝑔 “ (1...𝑘)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔𝑘))
150 sstr2 3768 . . . . . . . . . . . . . 14 ( (𝑔 “ (1...𝑘)) ⊆ (𝑔𝑘) → ((𝑔𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
151148, 149, 1503syl 18 . . . . . . . . . . . . 13 (((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑔𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
152151reximdva 3163 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
153138, 152sylbid 231 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
154130, 153syl5bir 234 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤𝑥 (𝐴𝑤𝑤𝑦) → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
155128, 154syld 47 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
156101sseq1d 3792 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
157156rexbidva 3196 . . . . . . . . . 10 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
158157adantr 472 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
159155, 158sylibrd 250 . . . . . . . 8 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
160159ralrimiva 3113 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
161 nnex 11281 . . . . . . . . 9 ℕ ∈ V
162161mptex 6679 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) ∈ V
163 feq1 6204 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓:ℕ⟶𝐽 ↔ (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽))
164 fveq1 6374 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓𝑘) = ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
165164eleq2d 2830 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝐴 ∈ (𝑓𝑘) ↔ 𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
166 fveq1 6374 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)))
167166, 164sseq12d 3794 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘) ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
168165, 167anbi12d 624 . . . . . . . . . 10 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ↔ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))))
169168ralbidv 3133 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ↔ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))))
170164sseq1d 3792 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓𝑘) ⊆ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
171170rexbidv 3199 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
172171imbi2d 331 . . . . . . . . . 10 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦) ↔ (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
173172ralbidv 3133 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦) ↔ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
174163, 169, 1733anbi123d 1560 . . . . . . . 8 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)) ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))))
175162, 174spcev 3452 . . . . . . 7 (((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
17677, 120, 160, 175syl3anc 1490 . . . . . 6 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
177176expr 448 . . . . 5 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))) → (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
178177adantrrl 715 . . . 4 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
179178exlimdv 2028 . . 3 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
18039, 179mpd 15 . 2 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
1812, 180rexlimddv 3182 1 ((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315   cuni 4594   cint 4633   class class class wbr 4809  cmpt 4888  dom cdm 5277  ran crn 5278  cres 5279  cima 5280  Fun wfun 6062   Fn wfn 6063  wf 6064  ontowfo 6066  cfv 6068  (class class class)co 6842  ωcom 7263  cen 8157  cdom 8158  csdm 8159  Fincfn 8160  1c1 10190   + caddc 10192  cn 11274  ...cfz 12533  Topctop 20977  1st𝜔c1stc 21520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-top 20978  df-1stc 21522
This theorem is referenced by:  1stcelcls  21544
  Copyright terms: Public domain W3C validator