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

Theorem 1stcfb 23273
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 23272 . 2 ((𝐽 ∈ 1stω ∧ 𝐴𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))
3 simplr 766 . . . . . . . . 9 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝐴𝑋)
4 eleq2 2814 . . . . . . . . . . 11 (𝑧 = 𝑋 → (𝐴𝑧𝐴𝑋))
5 sseq2 4001 . . . . . . . . . . . . 13 (𝑧 = 𝑋 → (𝑤𝑧𝑤𝑋))
65anbi2d 628 . . . . . . . . . . . 12 (𝑧 = 𝑋 → ((𝐴𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝑋)))
76rexbidv 3170 . . . . . . . . . . 11 (𝑧 = 𝑋 → (∃𝑤𝑥 (𝐴𝑤𝑤𝑧) ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑋)))
84, 7imbi12d 344 . . . . . . . . . 10 (𝑧 = 𝑋 → ((𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ↔ (𝐴𝑋 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋))))
9 simprrr 779 . . . . . . . . . 10 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))
10 1stctop 23271 . . . . . . . . . . . 12 (𝐽 ∈ 1stω → 𝐽 ∈ Top)
1110ad2antrr 723 . . . . . . . . . . 11 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝐽 ∈ Top)
121topopn 22732 . . . . . . . . . . 11 (𝐽 ∈ Top → 𝑋𝐽)
1311, 12syl 17 . . . . . . . . . 10 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑋𝐽)
148, 9, 13rspcdva 3605 . . . . . . . . 9 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (𝐴𝑋 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋)))
153, 14mpd 15 . . . . . . . 8 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑤𝑥 (𝐴𝑤𝑤𝑋))
16 simpl 482 . . . . . . . . 9 ((𝐴𝑤𝑤𝑋) → 𝐴𝑤)
1716reximi 3076 . . . . . . . 8 (∃𝑤𝑥 (𝐴𝑤𝑤𝑋) → ∃𝑤𝑥 𝐴𝑤)
1815, 17syl 17 . . . . . . 7 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑤𝑥 𝐴𝑤)
19 eleq2w 2809 . . . . . . . 8 (𝑤 = 𝑎 → (𝐴𝑤𝐴𝑎))
2019cbvrexvw 3227 . . . . . . 7 (∃𝑤𝑥 𝐴𝑤 ↔ ∃𝑎𝑥 𝐴𝑎)
2118, 20sylib 217 . . . . . 6 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑎𝑥 𝐴𝑎)
22 rabn0 4378 . . . . . 6 ({𝑎𝑥𝐴𝑎} ≠ ∅ ↔ ∃𝑎𝑥 𝐴𝑎)
2321, 22sylibr 233 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → {𝑎𝑥𝐴𝑎} ≠ ∅)
24 vex 3470 . . . . . . 7 𝑥 ∈ V
2524rabex 5323 . . . . . 6 {𝑎𝑥𝐴𝑎} ∈ V
26250sdom 9104 . . . . 5 (∅ ≺ {𝑎𝑥𝐴𝑎} ↔ {𝑎𝑥𝐴𝑎} ≠ ∅)
2723, 26sylibr 233 . . . 4 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∅ ≺ {𝑎𝑥𝐴𝑎})
28 ssrab2 4070 . . . . . 6 {𝑎𝑥𝐴𝑎} ⊆ 𝑥
29 ssdomg 8993 . . . . . 6 (𝑥 ∈ V → ({𝑎𝑥𝐴𝑎} ⊆ 𝑥 → {𝑎𝑥𝐴𝑎} ≼ 𝑥))
3024, 28, 29mp2 9 . . . . 5 {𝑎𝑥𝐴𝑎} ≼ 𝑥
31 simprrl 778 . . . . . 6 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑥 ≼ ω)
32 nnenom 13943 . . . . . . 7 ℕ ≈ ω
3332ensymi 8997 . . . . . 6 ω ≈ ℕ
34 domentr 9006 . . . . . 6 ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
3531, 33, 34sylancl 585 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → 𝑥 ≼ ℕ)
36 domtr 9000 . . . . 5 (({𝑎𝑥𝐴𝑎} ≼ 𝑥𝑥 ≼ ℕ) → {𝑎𝑥𝐴𝑎} ≼ ℕ)
3730, 35, 36sylancr 586 . . . 4 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → {𝑎𝑥𝐴𝑎} ≼ ℕ)
38 fodomr 9125 . . . 4 ((∅ ≺ {𝑎𝑥𝐴𝑎} ∧ {𝑎𝑥𝐴𝑎} ≼ ℕ) → ∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})
3927, 37, 38syl2anc 583 . . 3 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})
4010ad3antrrr 727 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → 𝐽 ∈ Top)
41 imassrn 6061 . . . . . . . . . 10 (𝑔 “ (1...𝑛)) ⊆ ran 𝑔
42 forn 6799 . . . . . . . . . . . . 13 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ran 𝑔 = {𝑎𝑥𝐴𝑎})
4342ad2antll 726 . . . . . . . . . . . 12 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ran 𝑔 = {𝑎𝑥𝐴𝑎})
44 simprll 776 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑥 ∈ 𝒫 𝐽)
4544elpwid 4604 . . . . . . . . . . . . 13 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑥𝐽)
4628, 45sstrid 3986 . . . . . . . . . . . 12 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → {𝑎𝑥𝐴𝑎} ⊆ 𝐽)
4743, 46eqsstrd 4013 . . . . . . . . . . 11 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ran 𝑔𝐽)
4847adantr 480 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → ran 𝑔𝐽)
4941, 48sstrid 3986 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ⊆ 𝐽)
50 fz1ssnn 13530 . . . . . . . . . . . . . 14 (1...𝑛) ⊆ ℕ
51 fof 6796 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → 𝑔:ℕ⟶{𝑎𝑥𝐴𝑎})
5251ad2antll 726 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑔:ℕ⟶{𝑎𝑥𝐴𝑎})
5352fdmd 6719 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → dom 𝑔 = ℕ)
5450, 53sseqtrrid 4028 . . . . . . . . . . . . 13 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (1...𝑛) ⊆ dom 𝑔)
5554adantr 480 . . . . . . . . . . . 12 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ dom 𝑔)
56 sseqin2 4208 . . . . . . . . . . . 12 ((1...𝑛) ⊆ dom 𝑔 ↔ (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
5755, 56sylib 217 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) = (1...𝑛))
58 elfz1end 13529 . . . . . . . . . . . 12 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
59 ne0i 4327 . . . . . . . . . . . . 13 (𝑛 ∈ (1...𝑛) → (1...𝑛) ≠ ∅)
6059adantl 481 . . . . . . . . . . . 12 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ (1...𝑛)) → (1...𝑛) ≠ ∅)
6158, 60sylan2b 593 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ≠ ∅)
6257, 61eqnetrd 3000 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
63 imadisj 6070 . . . . . . . . . . 11 ((𝑔 “ (1...𝑛)) = ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) = ∅)
6463necon3bii 2985 . . . . . . . . . 10 ((𝑔 “ (1...𝑛)) ≠ ∅ ↔ (dom 𝑔 ∩ (1...𝑛)) ≠ ∅)
6562, 64sylibr 233 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ≠ ∅)
66 fzfid 13936 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin)
6752ffund 6712 . . . . . . . . . . 11 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → Fun 𝑔)
68 fores 6806 . . . . . . . . . . 11 ((Fun 𝑔 ∧ (1...𝑛) ⊆ dom 𝑔) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
6967, 55, 68syl2an2r 682 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛)))
70 fofi 9335 . . . . . . . . . 10 (((1...𝑛) ∈ Fin ∧ (𝑔 ↾ (1...𝑛)):(1...𝑛)–onto→(𝑔 “ (1...𝑛))) → (𝑔 “ (1...𝑛)) ∈ Fin)
7166, 69, 70syl2anc 583 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ Fin)
72 fiinopn 22727 . . . . . . . . . 10 (𝐽 ∈ Top → (((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin) → (𝑔 “ (1...𝑛)) ∈ 𝐽))
7372imp 406 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((𝑔 “ (1...𝑛)) ⊆ 𝐽 ∧ (𝑔 “ (1...𝑛)) ≠ ∅ ∧ (𝑔 “ (1...𝑛)) ∈ Fin)) → (𝑔 “ (1...𝑛)) ∈ 𝐽)
7440, 49, 65, 71, 73syl13anc 1369 . . . . . . . 8 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑛 ∈ ℕ) → (𝑔 “ (1...𝑛)) ∈ 𝐽)
7574fmpttd 7107 . . . . . . 7 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽)
76 imassrn 6061 . . . . . . . . . . . . 13 (𝑔 “ (1...𝑘)) ⊆ ran 𝑔
7743adantr 480 . . . . . . . . . . . . 13 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ran 𝑔 = {𝑎𝑥𝐴𝑎})
7876, 77sseqtrid 4027 . . . . . . . . . . . 12 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ {𝑎𝑥𝐴𝑎})
79 id 22 . . . . . . . . . . . . . 14 (𝐴𝑛𝐴𝑛)
8079rgenw 3057 . . . . . . . . . . . . 13 𝑛𝑥 (𝐴𝑛𝐴𝑛)
81 eleq2w 2809 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (𝐴𝑎𝐴𝑛))
8281ralrab 3682 . . . . . . . . . . . . 13 (∀𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛 ↔ ∀𝑛𝑥 (𝐴𝑛𝐴𝑛))
8380, 82mpbir 230 . . . . . . . . . . . 12 𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛
84 ssralv 4043 . . . . . . . . . . . 12 ((𝑔 “ (1...𝑘)) ⊆ {𝑎𝑥𝐴𝑎} → (∀𝑛 ∈ {𝑎𝑥𝐴𝑎}𝐴𝑛 → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
8578, 83, 84mpisyl 21 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛)
86 elintg 4949 . . . . . . . . . . . 12 (𝐴𝑋 → (𝐴 (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
8786ad3antlr 728 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 (𝑔 “ (1...𝑘)) ↔ ∀𝑛 ∈ (𝑔 “ (1...𝑘))𝐴𝑛))
8885, 87mpbird 257 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 (𝑔 “ (1...𝑘)))
89 eqid 2724 . . . . . . . . . . 11 (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))
90 oveq2 7410 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (1...𝑛) = (1...𝑘))
9190imaeq2d 6050 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
9291inteqd 4946 . . . . . . . . . . 11 (𝑛 = 𝑘 (𝑔 “ (1...𝑛)) = (𝑔 “ (1...𝑘)))
93 simpr 484 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
9474ralrimiva 3138 . . . . . . . . . . . 12 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽)
9592eleq1d 2810 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ( (𝑔 “ (1...𝑛)) ∈ 𝐽 (𝑔 “ (1...𝑘)) ∈ 𝐽))
9695rspccva 3603 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ∈ 𝐽)
9794, 96sylan 579 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ∈ 𝐽)
9889, 92, 93, 97fvmptd3 7012 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) = (𝑔 “ (1...𝑘)))
9988, 98eleqtrrd 2828 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
100 fzssp1 13542 . . . . . . . . . . . 12 (1...𝑘) ⊆ (1...(𝑘 + 1))
101 imass2 6092 . . . . . . . . . . . 12 ((1...𝑘) ⊆ (1...(𝑘 + 1)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
102100, 101mp1i 13 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))))
103 intss 4964 . . . . . . . . . . 11 ((𝑔 “ (1...𝑘)) ⊆ (𝑔 “ (1...(𝑘 + 1))) → (𝑔 “ (1...(𝑘 + 1))) ⊆ (𝑔 “ (1...𝑘)))
104102, 103syl 17 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ⊆ (𝑔 “ (1...𝑘)))
105 oveq2 7410 . . . . . . . . . . . . 13 (𝑛 = (𝑘 + 1) → (1...𝑛) = (1...(𝑘 + 1)))
106105imaeq2d 6050 . . . . . . . . . . . 12 (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
107106inteqd 4946 . . . . . . . . . . 11 (𝑛 = (𝑘 + 1) → (𝑔 “ (1...𝑛)) = (𝑔 “ (1...(𝑘 + 1))))
108 peano2nn 12222 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
109108adantl 481 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
110107eleq1d 2810 . . . . . . . . . . . . 13 (𝑛 = (𝑘 + 1) → ( (𝑔 “ (1...𝑛)) ∈ 𝐽 (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽))
111110rspccva 3603 . . . . . . . . . . . 12 ((∀𝑛 ∈ ℕ (𝑔 “ (1...𝑛)) ∈ 𝐽 ∧ (𝑘 + 1) ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
11294, 108, 111syl2an 595 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝑔 “ (1...(𝑘 + 1))) ∈ 𝐽)
11389, 107, 109, 112fvmptd3 7012 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) = (𝑔 “ (1...(𝑘 + 1))))
114104, 113, 983sstr4d 4022 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
11599, 114jca 511 . . . . . . . 8 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
116115ralrimiva 3138 . . . . . . 7 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
117 simprlr 777 . . . . . . . . . . 11 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))
118 eleq2w 2809 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝐴𝑧𝐴𝑦))
119 sseq2 4001 . . . . . . . . . . . . . . 15 (𝑧 = 𝑦 → (𝑤𝑧𝑤𝑦))
120119anbi2d 628 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → ((𝐴𝑤𝑤𝑧) ↔ (𝐴𝑤𝑤𝑦)))
121120rexbidv 3170 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (∃𝑤𝑥 (𝐴𝑤𝑤𝑧) ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
122118, 121imbi12d 344 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ((𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ↔ (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦))))
123122rspccva 3603 . . . . . . . . . . 11 ((∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
124117, 123sylan 579 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑦)))
125 eleq2w 2809 . . . . . . . . . . . 12 (𝑎 = 𝑤 → (𝐴𝑎𝐴𝑤))
126125rexrab 3685 . . . . . . . . . . 11 (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑤𝑥 (𝐴𝑤𝑤𝑦))
12743rexeqdv 3318 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦))
128 fofn 6798 . . . . . . . . . . . . . . . 16 (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → 𝑔 Fn ℕ)
129128ad2antll 726 . . . . . . . . . . . . . . 15 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → 𝑔 Fn ℕ)
130 sseq1 4000 . . . . . . . . . . . . . . . 16 (𝑤 = (𝑔𝑘) → (𝑤𝑦 ↔ (𝑔𝑘) ⊆ 𝑦))
131130rexrn 7079 . . . . . . . . . . . . . . 15 (𝑔 Fn ℕ → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
132129, 131syl 17 . . . . . . . . . . . . . 14 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ ran 𝑔 𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
133127, 132bitr3d 281 . . . . . . . . . . . . 13 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
134133adantr 480 . . . . . . . . . . . 12 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦))
135 elfz1end 13529 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (1...𝑘))
136 fz1ssnn 13530 . . . . . . . . . . . . . . . . . 18 (1...𝑘) ⊆ ℕ
13753adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → dom 𝑔 = ℕ)
138136, 137sseqtrrid 4028 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (1...𝑘) ⊆ dom 𝑔)
139 funfvima2 7225 . . . . . . . . . . . . . . . . 17 ((Fun 𝑔 ∧ (1...𝑘) ⊆ dom 𝑔) → (𝑘 ∈ (1...𝑘) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘))))
14067, 138, 139syl2an2r 682 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝑘 ∈ (1...𝑘) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘))))
141140imp 406 . . . . . . . . . . . . . . 15 (((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ (1...𝑘)) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘)))
142135, 141sylan2b 593 . . . . . . . . . . . . . 14 (((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ ℕ) → (𝑔𝑘) ∈ (𝑔 “ (1...𝑘)))
143 intss1 4958 . . . . . . . . . . . . . 14 ((𝑔𝑘) ∈ (𝑔 “ (1...𝑘)) → (𝑔 “ (1...𝑘)) ⊆ (𝑔𝑘))
144 sstr2 3982 . . . . . . . . . . . . . 14 ( (𝑔 “ (1...𝑘)) ⊆ (𝑔𝑘) → ((𝑔𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
145142, 143, 1443syl 18 . . . . . . . . . . . . 13 (((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑔𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
146145reximdva 3160 . . . . . . . . . . . 12 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑘 ∈ ℕ (𝑔𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
147134, 146sylbid 239 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤 ∈ {𝑎𝑥𝐴𝑎}𝑤𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
148126, 147biimtrrid 242 . . . . . . . . . 10 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑤𝑥 (𝐴𝑤𝑤𝑦) → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
149124, 148syld 47 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
15098sseq1d 4006 . . . . . . . . . . 11 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑘 ∈ ℕ) → (((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 (𝑔 “ (1...𝑘)) ⊆ 𝑦))
151150rexbidva 3168 . . . . . . . . . 10 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
152151adantr 480 . . . . . . . . 9 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ (𝑔 “ (1...𝑘)) ⊆ 𝑦))
153149, 152sylibrd 259 . . . . . . . 8 ((((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) ∧ 𝑦𝐽) → (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
154153ralrimiva 3138 . . . . . . 7 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
155 nnex 12216 . . . . . . . . 9 ℕ ∈ V
156155mptex 7217 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) ∈ V
157 feq1 6689 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓:ℕ⟶𝐽 ↔ (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽))
158 fveq1 6881 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓𝑘) = ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))
159158eleq2d 2811 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝐴 ∈ (𝑓𝑘) ↔ 𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
160 fveq1 6881 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (𝑓‘(𝑘 + 1)) = ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)))
161160, 158sseq12d 4008 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘) ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)))
162159, 161anbi12d 630 . . . . . . . . . 10 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ↔ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))))
163162ralbidv 3169 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ↔ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘))))
164158sseq1d 4006 . . . . . . . . . . . 12 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓𝑘) ⊆ 𝑦 ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
165164rexbidv 3170 . . . . . . . . . . 11 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦 ↔ ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))
166165imbi2d 340 . . . . . . . . . 10 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦) ↔ (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
167166ralbidv 3169 . . . . . . . . 9 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → (∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦) ↔ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)))
168157, 163, 1673anbi123d 1432 . . . . . . . 8 (𝑓 = (𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))) → ((𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)) ↔ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦))))
169156, 168spcev 3588 . . . . . . 7 (((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛))):ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ∧ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘(𝑘 + 1)) ⊆ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ ((𝑛 ∈ ℕ ↦ (𝑔 “ (1...𝑛)))‘𝑘) ⊆ 𝑦)) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
17075, 116, 154, 169syl3anc 1368 . . . . . 6 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ ((𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))) ∧ 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎})) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
171170expr 456 . . . . 5 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧)))) → (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
172171adantrrl 721 . . . 4 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
173172exlimdv 1928 . . 3 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → (∃𝑔 𝑔:ℕ–onto→{𝑎𝑥𝐴𝑎} → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦))))
17439, 173mpd 15 . 2 (((𝐽 ∈ 1stω ∧ 𝐴𝑋) ∧ (𝑥 ∈ 𝒫 𝐽 ∧ (𝑥 ≼ ω ∧ ∀𝑧𝐽 (𝐴𝑧 → ∃𝑤𝑥 (𝐴𝑤𝑤𝑧))))) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
1752, 174rexlimddv 3153 1 ((𝐽 ∈ 1stω ∧ 𝐴𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓𝑘)) ∧ ∀𝑦𝐽 (𝐴𝑦 → ∃𝑘 ∈ ℕ (𝑓𝑘) ⊆ 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2932  wral 3053  wrex 3062  {crab 3424  Vcvv 3466  cin 3940  wss 3941  c0 4315  𝒫 cpw 4595   cuni 4900   cint 4941   class class class wbr 5139  cmpt 5222  dom cdm 5667  ran crn 5668  cres 5669  cima 5670  Fun wfun 6528   Fn wfn 6529  wf 6530  ontowfo 6532  cfv 6534  (class class class)co 7402  ωcom 7849  cen 8933  cdom 8934  csdm 8935  Fincfn 8936  1c1 11108   + caddc 11110  cn 12210  ...cfz 13482  Topctop 22719  1stωc1stc 23265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-nn 12211  df-n0 12471  df-z 12557  df-uz 12821  df-fz 13483  df-top 22720  df-1stc 23267
This theorem is referenced by:  1stcelcls  23289
  Copyright terms: Public domain W3C validator