ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ennnfonelemex GIF version

Theorem ennnfonelemex 12468
Description: Lemma for ennnfone 12479. Extending the sequence (𝐻𝑃) to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
ennnfonelemh.f (𝜑𝐹:ω–onto𝐴)
ennnfonelemh.ne (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
ennnfonelemh.g 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
ennnfonelemh.n 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
ennnfonelemh.j 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
ennnfonelemh.h 𝐻 = seq0(𝐺, 𝐽)
ennnfonelemex.p (𝜑𝑃 ∈ ℕ0)
Assertion
Ref Expression
ennnfonelemex (𝜑 → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
Distinct variable groups:   𝐴,𝑗,𝑥,𝑦   𝑗,𝐹,𝑘,𝑛   𝑥,𝐹,𝑦   𝑗,𝐺   𝑗,𝐻,𝑘,𝑛   𝑖,𝐻,𝑘   𝑥,𝐻,𝑦,𝑘   𝑗,𝐽   𝑗,𝑁,𝑘,𝑛   𝑖,𝑁   𝑥,𝑁,𝑦   𝑃,𝑗,𝑘,𝑛   𝑥,𝑃,𝑦   𝑃,𝑖   𝜑,𝑗,𝑘,𝑛   𝜑,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑖)   𝐴(𝑖,𝑘,𝑛)   𝐹(𝑖)   𝐺(𝑥,𝑦,𝑖,𝑘,𝑛)   𝐽(𝑥,𝑦,𝑖,𝑘,𝑛)

Proof of Theorem ennnfonelemex
Dummy variables 𝑎 𝑏 𝑞 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suceq 4420 . . . . 5 (𝑛 = (𝑁𝑃) → suc 𝑛 = suc (𝑁𝑃))
21raleqdv 2692 . . . 4 (𝑛 = (𝑁𝑃) → (∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗)))
32rexbidv 2491 . . 3 (𝑛 = (𝑁𝑃) → (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑘 ∈ ω ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗)))
4 ennnfonelemh.ne . . 3 (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
5 ennnfonelemh.n . . . . . . 7 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
65frechashgf1o 10461 . . . . . 6 𝑁:ω–1-1-onto→ℕ0
7 f1ocnv 5493 . . . . . 6 (𝑁:ω–1-1-onto→ℕ0𝑁:ℕ01-1-onto→ω)
86, 7ax-mp 5 . . . . 5 𝑁:ℕ01-1-onto→ω
9 f1of 5480 . . . . 5 (𝑁:ℕ01-1-onto→ω → 𝑁:ℕ0⟶ω)
108, 9mp1i 10 . . . 4 (𝜑𝑁:ℕ0⟶ω)
11 ennnfonelemex.p . . . 4 (𝜑𝑃 ∈ ℕ0)
1210, 11ffvelcdmd 5673 . . 3 (𝜑 → (𝑁𝑃) ∈ ω)
133, 4, 12rspcdva 2861 . 2 (𝜑 → ∃𝑘 ∈ ω ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))
14 f1of 5480 . . . . 5 (𝑁:ω–1-1-onto→ℕ0𝑁:ω⟶ℕ0)
156, 14mp1i 10 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑁:ω⟶ℕ0)
16 peano2 4612 . . . . 5 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
1716ad2antrl 490 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → suc 𝑘 ∈ ω)
1815, 17ffvelcdmd 5673 . . 3 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘suc 𝑘) ∈ ℕ0)
19 ennnfonelemh.f . . . . . . . . 9 (𝜑𝐹:ω–onto𝐴)
2019ad2antrr 488 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝐹:ω–onto𝐴)
21 fofun 5458 . . . . . . . 8 (𝐹:ω–onto𝐴 → Fun 𝐹)
2220, 21syl 14 . . . . . . 7 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → Fun 𝐹)
23 vex 2755 . . . . . . . . . 10 𝑘 ∈ V
2423sucid 4435 . . . . . . . . 9 𝑘 ∈ suc 𝑘
25 simprl 529 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑘 ∈ ω)
2625adantr 276 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝑘 ∈ ω)
27 fof 5457 . . . . . . . . . . . 12 (𝐹:ω–onto𝐴𝐹:ω⟶𝐴)
28 fdm 5390 . . . . . . . . . . . 12 (𝐹:ω⟶𝐴 → dom 𝐹 = ω)
2920, 27, 283syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → dom 𝐹 = ω)
3026, 29eleqtrrd 2269 . . . . . . . . . 10 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝑘 ∈ dom 𝐹)
31 funfvima 5769 . . . . . . . . . 10 ((Fun 𝐹𝑘 ∈ dom 𝐹) → (𝑘 ∈ suc 𝑘 → (𝐹𝑘) ∈ (𝐹 “ suc 𝑘)))
3222, 30, 31syl2anc 411 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝑘 ∈ suc 𝑘 → (𝐹𝑘) ∈ (𝐹 “ suc 𝑘)))
3324, 32mpi 15 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹𝑘) ∈ (𝐹 “ suc 𝑘))
34 simpr 110 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)))
35 ennnfonelemh.dceq . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
3635adantr 276 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
3719adantr 276 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝐹:ω–onto𝐴)
384adantr 276 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
39 fveq2 5534 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑎 → (𝐹𝑗) = (𝐹𝑎))
4039neeq2d 2379 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑎 → ((𝐹𝑘) ≠ (𝐹𝑗) ↔ (𝐹𝑘) ≠ (𝐹𝑎)))
4140cbvralv 2718 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎))
4241rexbii 2497 . . . . . . . . . . . . . . . . . . . 20 (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎))
43 fveq2 5534 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑏 → (𝐹𝑘) = (𝐹𝑏))
4443neeq1d 2378 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑏 → ((𝐹𝑘) ≠ (𝐹𝑎) ↔ (𝐹𝑏) ≠ (𝐹𝑎)))
4544ralbidv 2490 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑏 → (∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎)))
4645cbvrexv 2719 . . . . . . . . . . . . . . . . . . . 20 (∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎) ↔ ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎))
4742, 46bitri 184 . . . . . . . . . . . . . . . . . . 19 (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎))
4847ralbii 2496 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑛 ∈ ω ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎))
4938, 48sylib 122 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑛 ∈ ω ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎))
50 ennnfonelemh.g . . . . . . . . . . . . . . . . 17 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
51 ennnfonelemh.j . . . . . . . . . . . . . . . . 17 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
52 ennnfonelemh.h . . . . . . . . . . . . . . . . 17 𝐻 = seq0(𝐺, 𝐽)
5336, 37, 49, 50, 5, 51, 52, 18ennnfonelemhf1o 12467 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (𝑁‘(𝑁‘suc 𝑘))))
54 f1ofun 5482 . . . . . . . . . . . . . . . 16 ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (𝑁‘(𝑁‘suc 𝑘))) → Fun (𝐻‘(𝑁‘suc 𝑘)))
5553, 54syl 14 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → Fun (𝐻‘(𝑁‘suc 𝑘)))
5655ad2antrr 488 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → Fun (𝐻‘(𝑁‘suc 𝑘)))
5711adantr 276 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 ∈ ℕ0)
586, 14mp1i 10 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ω) → 𝑁:ω⟶ℕ0)
5916adantl 277 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ω) → suc 𝑘 ∈ ω)
6058, 59ffvelcdmd 5673 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ω) → (𝑁‘suc 𝑘) ∈ ℕ0)
6160adantrr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘suc 𝑘) ∈ ℕ0)
6257nn0red 9261 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 ∈ ℝ)
6361nn0red 9261 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘suc 𝑘) ∈ ℝ)
64 f1ocnvfv2 5800 . . . . . . . . . . . . . . . . . . 19 ((𝑁:ω–1-1-onto→ℕ0𝑃 ∈ ℕ0) → (𝑁‘(𝑁𝑃)) = 𝑃)
656, 57, 64sylancr 414 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘(𝑁𝑃)) = 𝑃)
6612adantr 276 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁𝑃) ∈ ω)
67 simprr 531 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))
6837, 25, 66, 67ennnfonelemk 12454 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁𝑃) ∈ 𝑘)
69 elelsuc 4427 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑃) ∈ 𝑘 → (𝑁𝑃) ∈ suc 𝑘)
7068, 69syl 14 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁𝑃) ∈ suc 𝑘)
71 0zd 9296 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 0 ∈ ℤ)
7271, 5, 66, 17frec2uzltd 10436 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝑁𝑃) ∈ suc 𝑘 → (𝑁‘(𝑁𝑃)) < (𝑁‘suc 𝑘)))
7370, 72mpd 13 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘(𝑁𝑃)) < (𝑁‘suc 𝑘))
7465, 73eqbrtrrd 4042 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 < (𝑁‘suc 𝑘))
7562, 63, 74ltled 8107 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 ≤ (𝑁‘suc 𝑘))
7636, 37, 38, 50, 5, 51, 52, 57, 61, 75ennnfoneleminc 12465 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)))
7776ad2antrr 488 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → (𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)))
78 simpr 110 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → 𝑠 ∈ dom (𝐻𝑃))
79 funssfv 5560 . . . . . . . . . . . . . 14 ((Fun (𝐻‘(𝑁‘suc 𝑘)) ∧ (𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)) ∧ 𝑠 ∈ dom (𝐻𝑃)) → ((𝐻‘(𝑁‘suc 𝑘))‘𝑠) = ((𝐻𝑃)‘𝑠))
8056, 77, 78, 79syl3anc 1249 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → ((𝐻‘(𝑁‘suc 𝑘))‘𝑠) = ((𝐻𝑃)‘𝑠))
8180eqcomd 2195 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → ((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))
8281ralrimiva 2563 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))
8336, 37, 49, 50, 5, 51, 52, 57ennnfonelemhf1o 12467 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)))
84 f1ofun 5482 . . . . . . . . . . . . . 14 ((𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)) → Fun (𝐻𝑃))
8583, 84syl 14 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → Fun (𝐻𝑃))
86 eqfunfv 5639 . . . . . . . . . . . . 13 ((Fun (𝐻𝑃) ∧ Fun (𝐻‘(𝑁‘suc 𝑘))) → ((𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))))
8785, 55, 86syl2anc 411 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))))
8887adantr 276 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ((𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))))
8934, 82, 88mpbir2and 946 . . . . . . . . . 10 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)))
9089rneqd 4874 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻𝑃) = ran (𝐻‘(𝑁‘suc 𝑘)))
91 dff1o5 5489 . . . . . . . . . . . 12 ((𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)) ↔ ((𝐻𝑃):dom (𝐻𝑃)–1-1→(𝐹 “ (𝑁𝑃)) ∧ ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃))))
9283, 91sylib 122 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝐻𝑃):dom (𝐻𝑃)–1-1→(𝐹 “ (𝑁𝑃)) ∧ ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃))))
9392simprd 114 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃)))
9493adantr 276 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃)))
95 f1ocnvfv1 5799 . . . . . . . . . . . . . . . 16 ((𝑁:ω–1-1-onto→ℕ0 ∧ suc 𝑘 ∈ ω) → (𝑁‘(𝑁‘suc 𝑘)) = suc 𝑘)
966, 17, 95sylancr 414 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘(𝑁‘suc 𝑘)) = suc 𝑘)
9796imaeq2d 4988 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐹 “ (𝑁‘(𝑁‘suc 𝑘))) = (𝐹 “ suc 𝑘))
98 f1oeq3 5470 . . . . . . . . . . . . . 14 ((𝐹 “ (𝑁‘(𝑁‘suc 𝑘))) = (𝐹 “ suc 𝑘) → ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (𝑁‘(𝑁‘suc 𝑘))) ↔ (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘)))
9997, 98syl 14 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (𝑁‘(𝑁‘suc 𝑘))) ↔ (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘)))
10053, 99mpbid 147 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘))
101 dff1o5 5489 . . . . . . . . . . . 12 ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘) ↔ ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1→(𝐹 “ suc 𝑘) ∧ ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘)))
102100, 101sylib 122 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1→(𝐹 “ suc 𝑘) ∧ ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘)))
103102simprd 114 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘))
104103adantr 276 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘))
10590, 94, 1043eqtr3d 2230 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹 “ (𝑁𝑃)) = (𝐹 “ suc 𝑘))
10633, 105eleqtrrd 2269 . . . . . . 7 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹𝑘) ∈ (𝐹 “ (𝑁𝑃)))
107 fvelima 5588 . . . . . . 7 ((Fun 𝐹 ∧ (𝐹𝑘) ∈ (𝐹 “ (𝑁𝑃))) → ∃𝑞 ∈ (𝑁𝑃)(𝐹𝑞) = (𝐹𝑘))
10822, 106, 107syl2anc 411 . . . . . 6 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ∃𝑞 ∈ (𝑁𝑃)(𝐹𝑞) = (𝐹𝑘))
109 simprr 531 . . . . . . 7 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → (𝐹𝑞) = (𝐹𝑘))
110 fveq2 5534 . . . . . . . . . 10 (𝑗 = 𝑞 → (𝐹𝑗) = (𝐹𝑞))
111110neeq2d 2379 . . . . . . . . 9 (𝑗 = 𝑞 → ((𝐹𝑘) ≠ (𝐹𝑗) ↔ (𝐹𝑘) ≠ (𝐹𝑞)))
11267ad2antrr 488 . . . . . . . . 9 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))
113 elelsuc 4427 . . . . . . . . . 10 (𝑞 ∈ (𝑁𝑃) → 𝑞 ∈ suc (𝑁𝑃))
114113ad2antrl 490 . . . . . . . . 9 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → 𝑞 ∈ suc (𝑁𝑃))
115111, 112, 114rspcdva 2861 . . . . . . . 8 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → (𝐹𝑘) ≠ (𝐹𝑞))
116115necomd 2446 . . . . . . 7 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → (𝐹𝑞) ≠ (𝐹𝑘))
117109, 116pm2.21ddne 2443 . . . . . 6 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → ⊥)
118108, 117rexlimddv 2612 . . . . 5 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ⊥)
119118inegd 1383 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ¬ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)))
120 dmss 4844 . . . . . 6 ((𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)) → dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)))
12176, 120syl 14 . . . . 5 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)))
12235, 19, 4, 50, 5, 51, 52, 11ennnfonelemom 12462 . . . . . . 7 (𝜑 → dom (𝐻𝑃) ∈ ω)
123122adantr 276 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻𝑃) ∈ ω)
12442a1i 9 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎)))
125124ralbidv 2490 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎)))
12638, 125mpbid 147 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎))
12736, 37, 126, 50, 5, 51, 52, 61ennnfonelemom 12462 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω)
128 nntri1 6522 . . . . . 6 ((dom (𝐻𝑃) ∈ ω ∧ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω) → (dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)) ↔ ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
129123, 127, 128syl2anc 411 . . . . 5 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)) ↔ ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
130121, 129mpbid 147 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃))
131 nntri3or 6519 . . . . 5 ((dom (𝐻𝑃) ∈ ω ∧ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω) → (dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
132123, 127, 131syl2anc 411 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
133119, 130, 132ecase23d 1361 . . 3 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)))
134 fveq2 5534 . . . . . 6 (𝑖 = (𝑁‘suc 𝑘) → (𝐻𝑖) = (𝐻‘(𝑁‘suc 𝑘)))
135134dmeqd 4847 . . . . 5 (𝑖 = (𝑁‘suc 𝑘) → dom (𝐻𝑖) = dom (𝐻‘(𝑁‘suc 𝑘)))
136135eleq2d 2259 . . . 4 (𝑖 = (𝑁‘suc 𝑘) → (dom (𝐻𝑃) ∈ dom (𝐻𝑖) ↔ dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘))))
137136rspcev 2856 . . 3 (((𝑁‘suc 𝑘) ∈ ℕ0 ∧ dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘))) → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
13818, 133, 137syl2anc 411 . 2 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
13913, 138rexlimddv 2612 1 (𝜑 → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  DECID wdc 835  w3o 979   = wceq 1364  wfal 1369  wcel 2160  wne 2360  wral 2468  wrex 2469  cun 3142  wss 3144  c0 3437  ifcif 3549  {csn 3607  cop 3610   class class class wbr 4018  cmpt 4079  suc csuc 4383  ωcom 4607  ccnv 4643  dom cdm 4644  ran crn 4645  cima 4647  Fun wfun 5229  wf 5231  1-1wf1 5232  ontowfo 5233  1-1-ontowf1o 5234  cfv 5235  (class class class)co 5897  cmpo 5899  freccfrec 6416  pm cpm 6676  0cc0 7842  1c1 7843   + caddc 7845   < clt 8023  cmin 8159  0cn0 9207  cz 9284  seqcseq 10478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605  ax-cnex 7933  ax-resscn 7934  ax-1cn 7935  ax-1re 7936  ax-icn 7937  ax-addcl 7938  ax-addrcl 7939  ax-mulcl 7940  ax-addcom 7942  ax-addass 7944  ax-distr 7946  ax-i2m1 7947  ax-0lt1 7948  ax-0id 7950  ax-rnegex 7951  ax-cnre 7953  ax-pre-ltirr 7954  ax-pre-ltwlin 7955  ax-pre-lttrn 7956  ax-pre-ltadd 7958
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-iord 4384  df-on 4386  df-ilim 4387  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-riota 5852  df-ov 5900  df-oprab 5901  df-mpo 5902  df-1st 6166  df-2nd 6167  df-recs 6331  df-frec 6417  df-pm 6678  df-pnf 8025  df-mnf 8026  df-xr 8027  df-ltxr 8028  df-le 8029  df-sub 8161  df-neg 8162  df-inn 8951  df-n0 9208  df-z 9285  df-uz 9560  df-seqfrec 10479
This theorem is referenced by:  ennnfonelemhom  12469
  Copyright terms: Public domain W3C validator