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

Theorem 1stcfb 21158
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 21157 . 2 ((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))
3 1stctop 21156 . . . . . . . . . . 11 (𝐽 ∈ 1st𝜔 → 𝐽 ∈ Top)
43ad2antrr 761 . . . . . . . . . 10 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝐽 ∈ Top)
51topopn 20636 . . . . . . . . . 10 (𝐽 ∈ Top → 𝑋𝐽)
64, 5syl 17 . . . . . . . . 9 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑋𝐽)
7 simprrr 804 . . . . . . . . 9 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))
8 simplr 791 . . . . . . . . 9 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝐴𝑋)
9 eleq2 2687 . . . . . . . . . . 11 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
10 sseq2 3606 . . . . . . . . . . . . 13 (𝑧 = 𝑋 → (𝑤𝑧𝑤𝑋))
1110anbi2d 739 . . . . . . . . . . . 12 (𝑧 = 𝑋 → ((𝐴𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝑋)))
1211rexbidv 3045 . . . . . . . . . . 11 (𝑧 = 𝑋 → (∃𝑤𝑥 (𝐴𝑤𝑤𝑧) ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑋)))
139, 12imbi12d 334 . . . . . . . . . 10 (𝑧 = 𝑋 → ((𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ↔ (𝐴𝑋 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋))))
1413rspcv 3291 . . . . . . . . 9 (𝑋𝐽 → (∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) → (𝐴𝑋 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋))))
156, 7, 8, 14syl3c 66 . . . . . . . 8 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋))
16 simpl 473 . . . . . . . . 9 ((𝐴𝑤𝑤𝑋) → 𝐴𝑤)
1716reximi 3005 . . . . . . . 8 (∃𝑤𝑥 (𝐴𝑤𝑤𝑋) → ∃𝑤𝑥 𝐴𝑤)
1815, 17syl 17 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑤𝑥 𝐴𝑤)
19 eleq2 2687 . . . . . . . 8 (𝑤 = 𝑎 → (𝐴𝑤𝐴𝑎))
2019cbvrexv 3160 . . . . . . 7 (∃𝑤𝑥 𝐴𝑤 ↔ ∃𝑎𝑥 𝐴𝑎)
2118, 20sylib 208 . . . . . 6 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑎𝑥 𝐴𝑎)
22 rabn0 3932 . . . . . 6 ({𝑎𝑥𝐴𝑎} ≠ ∅ ↔ ∃𝑎𝑥 𝐴𝑎)
2321, 22sylibr 224 . . . . 5 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → {𝑎𝑥𝐴𝑎} ≠ ∅)
24 vex 3189 . . . . . . 7 𝑥 ∈ V
2524rabex 4773 . . . . . 6 {𝑎𝑥𝐴𝑎} ∈ V
26250sdom 8035 . . . . 5 (∅ ≺ {𝑎𝑥𝐴𝑎} ↔ {𝑎𝑥𝐴𝑎} ≠ ∅)
2723, 26sylibr 224 . . . 4 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∅ ≺ {𝑎𝑥𝐴𝑎})
28 ssrab2 3666 . . . . . 6 {𝑎𝑥𝐴𝑎} ⊆ 𝑥
29 ssdomg 7945 . . . . . 6 (𝑥 ∈ V → ({𝑎𝑥𝐴𝑎} ⊆ 𝑥 → {𝑎𝑥𝐴𝑎} ≼ 𝑥))
3024, 28, 29mp2 9 . . . . 5 {𝑎𝑥𝐴𝑎} ≼ 𝑥
31 simprrl 803 . . . . . 6 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑥 ≼ ω)
32 nnenom 12719 . . . . . . 7 ℕ ≈ ω
3332ensymi 7950 . . . . . 6 ω ≈ ℕ
34 domentr 7959 . . . . . 6 ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
3531, 33, 34sylancl 693 . . . . 5 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑥 ≼ ℕ)
36 domtr 7953 . . . . 5 (({𝑎𝑥𝐴𝑎} ≼ 𝑥𝑥 ≼ ℕ) → {𝑎𝑥𝐴𝑎} ≼ ℕ)
3730, 35, 36sylancr 694 . . . 4 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → {𝑎𝑥𝐴𝑎} ≼ ℕ)
38 fodomr 8055 . . . 4 ((∅ ≺ {𝑎𝑥𝐴𝑎} ∧ {𝑎𝑥𝐴𝑎} ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})
3927, 37, 38syl2anc 692 . . 3 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})
403ad3antrrr 765 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → 𝐽 ∈ Top)
41 imassrn 5436 . . . . . . . . . 10 (𝑔 “ (1...𝑛)) ⊆ ran 𝑔
42 forn 6075 . . . . . . . . . . . . 13 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ran 𝑔 = {𝑎𝑥𝐴𝑎})
4342ad2antll 764 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ran 𝑔 = {𝑎𝑥𝐴𝑎})
44 simprll 801 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑥 ∈ 𝒫 𝐽)
4544elpwid 4141 . . . . . . . . . . . . 13 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑥𝐽)
4628, 45syl5ss 3594 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → {𝑎𝑥𝐴𝑎} ⊆ 𝐽)
4743, 46eqsstrd 3618 . . . . . . . . . . 11 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ran 𝑔𝐽)
4847adantr 481 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → ran 𝑔𝐽)
4941, 48syl5ss 3594 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ⊆ 𝐽)
50 elfznn 12312 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
5150ssriv 3587 . . . . . . . . . . . . . 14 (1...𝑛) ⊆ ℕ
52 fof 6072 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → 𝑔:ℕ⟶{𝑎𝑥𝐴𝑎})
5352ad2antll 764 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑔:ℕ⟶{𝑎𝑥𝐴𝑎})
54 fdm 6008 . . . . . . . . . . . . . . 15 (𝑔:ℕ⟶{𝑎𝑥𝐴𝑎} → dom 𝑔 = ℕ)
5553, 54syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → dom 𝑔 = ℕ)
5651, 55syl5sseqr 3633 . . . . . . . . . . . . 13 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (1...𝑛) ⊆ dom 𝑔)
5756adantr 481 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ dom 𝑔)
58 sseqin2 3795 . . . . . . . . . . . 12 ((1...𝑛) ⊆ dom 𝑔 ↔ (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
5957, 58sylib 208 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
60 elfz1end 12313 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
61 ne0i 3897 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑛) → (1...𝑛) ≠ ∅)
6261adantl 482 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ (1...𝑛)) → (1...𝑛) ≠ ∅)
6360, 62sylan2b 492 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ≠ ∅)
6459, 63eqnetrd 2857 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
65 imadisj 5443 . . . . . . . . . . 11 ((𝑔 “ (1...𝑛)) = ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) = ∅)
6665necon3bii 2842 . . . . . . . . . 10 ((𝑔 “ (1...𝑛)) ≠ ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
6764, 66sylibr 224 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ≠ ∅)
68 fzfid 12712 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
69 ffun 6005 . . . . . . . . . . . . 13 (𝑔:ℕ⟶{𝑎𝑥𝐴𝑎} → Fun 𝑔)
7053, 69syl 17 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → Fun 𝑔)
7170adantr 481 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → Fun 𝑔)
72 fores 6081 . . . . . . . . . . 11 ((Fun 𝑔 ∧ (1...𝑛) ⊆ dom 𝑔) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
7371, 57, 72syl2anc 692 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
74 fofi 8196 . . . . . . . . . 10 (((1...𝑛) ∈ Fin ∧ (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛))) → (𝑔 “ (1...𝑛)) ∈ Fin)
7568, 73, 74syl2anc 692 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ Fin)
76 fiinopn 20631 . . . . . . . . . 10 (𝐽 ∈ Top → (((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin) → (𝑔 “ (1...𝑛)) ∈ 𝐽))
7776imp 445 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin)) → (𝑔 “ (1...𝑛)) ∈ 𝐽)
7840, 49, 67, 75, 77syl13anc 1325 . . . . . . . 8 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ 𝐽)
79 eqid 2621 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))
8078, 79fmptd 6340 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽)
81 imassrn 5436 . . . . . . . . . . . . 13 (𝑔 “ (1...𝑘)) ⊆ ran 𝑔
8243adantr 481 . . . . . . . . . . . . 13 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ran 𝑔 = {𝑎𝑥𝐴𝑎})
8381, 82syl5sseq 3632 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ {𝑎𝑥𝐴𝑎})
84 id 22 . . . . . . . . . . . . . 14 (𝐴𝑛𝐴𝑛)
8584rgenw 2919 . . . . . . . . . . . . 13 𝑛𝑥 (𝐴𝑛𝐴𝑛)
86 eleq2 2687 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (𝐴𝑎𝐴𝑛))
8786ralrab 3350 . . . . . . . . . . . . 13 (∀𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛 ↔ ∀𝑛𝑥 (𝐴𝑛𝐴𝑛))
8885, 87mpbir 221 . . . . . . . . . . . 12 𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛
89 ssralv 3645 . . . . . . . . . . . 12 ((𝑔 “ (1...𝑘)) ⊆ {𝑎𝑥𝐴𝑎} → (∀𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛 → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
9083, 88, 89mpisyl 21 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛)
91 elintg 4448 . . . . . . . . . . . 12 (𝐴𝑋 → (𝐴 (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
9291ad3antlr 766 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
9390, 92mpbird 247 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 (𝑔 “ (1...𝑘)))
94 simpr 477 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
9578ralrimiva 2960 . . . . . . . . . . . 12 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽)
96 oveq2 6612 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
9796imaeq2d 5425 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
9897inteqd 4445 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
9998eleq1d 2683 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ( (𝑔 “ (1...𝑛)) ∈ 𝐽 (𝑔 “ (1...𝑘)) ∈ 𝐽))
10099rspccva 3294 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ∈ 𝐽)
10195, 100sylan 488 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ∈ 𝐽)
10298, 79fvmptg 6237 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (𝑔 “ (1...𝑘)) ∈ 𝐽) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) = (𝑔 “ (1...𝑘)))
10394, 101, 102syl2anc 692 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) = (𝑔 “ (1...𝑘)))
10493, 103eleqtrrd 2701 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
105 fzssp1 12326 . . . . . . . . . . . 12 (1...𝑘) ⊆ (1...(𝑘 + 1))
106 imass2 5460 . . . . . . . . . . . 12 ((1...𝑘) ⊆ (1...(𝑘 + 1)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
107105, 106mp1i 13 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
108 intss 4463 . . . . . . . . . . 11 ((𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))) → (𝑔 “ (1...(𝑘 + 1))) ⊆ (𝑔 “ (1...𝑘)))
109107, 108syl 17 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ⊆ (𝑔 “ (1...𝑘)))
110 peano2nn 10976 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
111110adantl 482 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
112 oveq2 6612 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
113112imaeq2d 5425 . . . . . . . . . . . . . . 15 (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
114113inteqd 4445 . . . . . . . . . . . . . 14 (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
115114eleq1d 2683 . . . . . . . . . . . . 13 (𝑛 = (𝑘 + 1) → ( (𝑔 “ (1...𝑛)) ∈ 𝐽 (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽))
116115rspccva 3294 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ (𝑘 + 1) ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
11795, 110, 116syl2an 494 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
118114, 79fvmptg 6237 . . . . . . . . . . 11 (((𝑘 + 1) ∈ ℕ ∧ (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = (𝑔 “ (1...(𝑘 + 1))))
119111, 117, 118syl2anc 692 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = (𝑔 “ (1...(𝑘 + 1))))
120109, 119, 1033sstr4d 3627 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
121104, 120jca 554 . . . . . . . 8 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
122121ralrimiva 2960 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
123 simprlr 802 . . . . . . . . . . 11 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))
124 eleq2 2687 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝐴𝑧𝐴𝑦))
125 sseq2 3606 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑤𝑧𝑤𝑦))
126125anbi2d 739 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐴𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝑦)))
127126rexbidv 3045 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (∃𝑤𝑥 (𝐴𝑤𝑤𝑧) ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
128124, 127imbi12d 334 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ((𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ↔ (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦))))
129128rspccva 3294 . . . . . . . . . . 11 ((∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
130123, 129sylan 488 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
131 eleq2 2687 . . . . . . . . . . . 12 (𝑎 = 𝑤 → (𝐴𝑎𝐴𝑤))
132131rexrab 3352 . . . . . . . . . . 11 (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑦))
13343rexeqdv 3134 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦))
134 fofn 6074 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → 𝑔 Fn ℕ)
135134ad2antll 764 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑔 Fn ℕ)
136 sseq1 3605 . . . . . . . . . . . . . . . 16 (𝑤 = (𝑔𝑘) → (𝑤𝑦 ↔ (𝑔𝑘) ⊆ 𝑦))
137136rexrn 6317 . . . . . . . . . . . . . . 15 (𝑔 Fn ℕ → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
138135, 137syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
139133, 138bitr3d 270 . . . . . . . . . . . . 13 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
140139adantr 481 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
141 elfz1end 12313 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (1...𝑘))
14270adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → Fun 𝑔)
143 elfznn 12312 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
144143ssriv 3587 . . . . . . . . . . . . . . . . . 18 (1...𝑘) ⊆ ℕ
14555adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → dom 𝑔 = ℕ)
146144, 145syl5sseqr 3633 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (1...𝑘) ⊆ dom 𝑔)
147 funfvima2 6447 . . . . . . . . . . . . . . . . 17 ((Fun 𝑔 ∧ (1...𝑘) ⊆ dom 𝑔) → (𝑘 ∈ (1...𝑘) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘))))
148142, 146, 147syl2anc 692 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝑘 ∈ (1...𝑘) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘))))
149148imp 445 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ (1...𝑘)) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘)))
150141, 149sylan2b 492 . . . . . . . . . . . . . 14 (((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ ℕ) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘)))
151 intss1 4457 . . . . . . . . . . . . . 14 ((𝑔𝑘) ∈ (𝑔 “ (1...𝑘)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔𝑘))
152 sstr2 3590 . . . . . . . . . . . . . 14 ( (𝑔 “ (1...𝑘)) ⊆ (𝑔𝑘) → ((𝑔𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
153150, 151, 1523syl 18 . . . . . . . . . . . . 13 (((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑔𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
154153reximdva 3011 . . . . . . . . . . . 12 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
155140, 154sylbid 230 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
156132, 155syl5bir 233 . . . . . . . . . 10 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤𝑥 (𝐴𝑤𝑤𝑦) → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
157130, 156syld 47 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
158103sseq1d 3611 . . . . . . . . . . 11 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
159158rexbidva 3042 . . . . . . . . . 10 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
160159adantr 481 . . . . . . . . 9 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
161157, 160sylibrd 249 . . . . . . . 8 ((((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
162161ralrimiva 2960 . . . . . . 7 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
163 nnex 10970 . . . . . . . . 9 ℕ ∈ V
164163mptex 6440 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) ∈ V
165 feq1 5983 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓:ℕ⟶𝐽 ↔ (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽))
166 fveq1 6147 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓𝑘) = ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
167166eleq2d 2684 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝐴 ∈ (𝑓𝑘) ↔ 𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
168 fveq1 6147 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)))
169168, 166sseq12d 3613 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘) ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
170167, 169anbi12d 746 . . . . . . . . . 10 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ↔ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))))
171170ralbidv 2980 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ↔ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))))
172166sseq1d 3611 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓𝑘) ⊆ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
173172rexbidv 3045 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
174173imbi2d 330 . . . . . . . . . 10 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦) ↔ (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
175174ralbidv 2980 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦) ↔ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
176165, 171, 1753anbi123d 1396 . . . . . . . 8 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)) ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))))
177164, 176spcev 3286 . . . . . . 7 (((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
17880, 122, 162, 177syl3anc 1323 . . . . . 6 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
179178expr 642 . . . . 5 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))) → (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
180179adantrrl 759 . . . 4 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
181180exlimdv 1858 . . 3 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
18239, 181mpd 15 . 2 (((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
1832, 182rexlimddv 3028 1 ((𝐽 ∈ 1st𝜔 ∧ 𝐴𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  cin 3554  wss 3555  c0 3891  𝒫 cpw 4130   cuni 4402   cint 4440   class class class wbr 4613  cmpt 4673  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  Fun wfun 5841   Fn wfn 5842  wf 5843  ontowfo 5845  cfv 5847  (class class class)co 6604  ωcom 7012  cen 7896  cdom 7897  csdm 7898  Fincfn 7899  1c1 9881   + caddc 9883  cn 10964  ...cfz 12268  Topctop 20617  1st𝜔c1stc 21150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-top 20621  df-1stc 21152
This theorem is referenced by:  1stcelcls  21174
  Copyright terms: Public domain W3C validator