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

Theorem ennnfonelemex 11997
 Description: Lemma for ennnfone 12008. 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 4334 . . . . 5 (𝑛 = (𝑁𝑃) → suc 𝑛 = suc (𝑁𝑃))
21raleqdv 2636 . . . 4 (𝑛 = (𝑁𝑃) → (∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗)))
32rexbidv 2440 . . 3 (𝑛 = (𝑁𝑃) → (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑘 ∈ ω ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗)))
4 ennnfonelemh.ne . . 3 (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
5 ennnfonelemh.n . . . . . . 7 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
65frechashgf1o 10259 . . . . . 6 𝑁:ω–1-1-onto→ℕ0
7 f1ocnv 5391 . . . . . 6 (𝑁:ω–1-1-onto→ℕ0𝑁:ℕ01-1-onto→ω)
86, 7ax-mp 5 . . . . 5 𝑁:ℕ01-1-onto→ω
9 f1of 5378 . . . . 5 (𝑁:ℕ01-1-onto→ω → 𝑁:ℕ0⟶ω)
108, 9mp1i 10 . . . 4 (𝜑𝑁:ℕ0⟶ω)
11 ennnfonelemex.p . . . 4 (𝜑𝑃 ∈ ℕ0)
1210, 11ffvelrnd 5567 . . 3 (𝜑 → (𝑁𝑃) ∈ ω)
133, 4, 12rspcdva 2799 . 2 (𝜑 → ∃𝑘 ∈ ω ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))
14 f1of 5378 . . . . 5 (𝑁:ω–1-1-onto→ℕ0𝑁:ω⟶ℕ0)
156, 14mp1i 10 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑁:ω⟶ℕ0)
16 peano2 4519 . . . . 5 (𝑘 ∈ ω → suc 𝑘 ∈ ω)
1716ad2antrl 482 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → suc 𝑘 ∈ ω)
1815, 17ffvelrnd 5567 . . 3 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘suc 𝑘) ∈ ℕ0)
19 ennnfonelemh.f . . . . . . . . 9 (𝜑𝐹:ω–onto𝐴)
2019ad2antrr 480 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝐹:ω–onto𝐴)
21 fofun 5357 . . . . . . . 8 (𝐹:ω–onto𝐴 → Fun 𝐹)
2220, 21syl 14 . . . . . . 7 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → Fun 𝐹)
23 vex 2693 . . . . . . . . . 10 𝑘 ∈ V
2423sucid 4349 . . . . . . . . 9 𝑘 ∈ suc 𝑘
25 simprl 521 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑘 ∈ ω)
2625adantr 274 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝑘 ∈ ω)
27 fof 5356 . . . . . . . . . . . 12 (𝐹:ω–onto𝐴𝐹:ω⟶𝐴)
28 fdm 5289 . . . . . . . . . . . 12 (𝐹:ω⟶𝐴 → dom 𝐹 = ω)
2920, 27, 283syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → dom 𝐹 = ω)
3026, 29eleqtrrd 2220 . . . . . . . . . 10 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝑘 ∈ dom 𝐹)
31 funfvima 5660 . . . . . . . . . 10 ((Fun 𝐹𝑘 ∈ dom 𝐹) → (𝑘 ∈ suc 𝑘 → (𝐹𝑘) ∈ (𝐹 “ suc 𝑘)))
3222, 30, 31syl2anc 409 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝑘 ∈ suc 𝑘 → (𝐹𝑘) ∈ (𝐹 “ suc 𝑘)))
3324, 32mpi 15 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹𝑘) ∈ (𝐹 “ suc 𝑘))
34 simpr 109 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)))
35 ennnfonelemh.dceq . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
3635adantr 274 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
3719adantr 274 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝐹:ω–onto𝐴)
384adantr 274 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
39 fveq2 5432 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑎 → (𝐹𝑗) = (𝐹𝑎))
4039neeq2d 2328 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑎 → ((𝐹𝑘) ≠ (𝐹𝑗) ↔ (𝐹𝑘) ≠ (𝐹𝑎)))
4140cbvralv 2658 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎))
4241rexbii 2446 . . . . . . . . . . . . . . . . . . . 20 (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎))
43 fveq2 5432 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑏 → (𝐹𝑘) = (𝐹𝑏))
4443neeq1d 2327 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑏 → ((𝐹𝑘) ≠ (𝐹𝑎) ↔ (𝐹𝑏) ≠ (𝐹𝑎)))
4544ralbidv 2439 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑏 → (∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎)))
4645cbvrexv 2659 . . . . . . . . . . . . . . . . . . . 20 (∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎) ↔ ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎))
4742, 46bitri 183 . . . . . . . . . . . . . . . . . . 19 (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎))
4847ralbii 2445 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑛 ∈ ω ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑏) ≠ (𝐹𝑎))
4938, 48sylib 121 . . . . . . . . . . . . . . . . 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 11996 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (𝑁‘(𝑁‘suc 𝑘))))
54 f1ofun 5380 . . . . . . . . . . . . . . . 16 ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (𝑁‘(𝑁‘suc 𝑘))) → Fun (𝐻‘(𝑁‘suc 𝑘)))
5553, 54syl 14 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → Fun (𝐻‘(𝑁‘suc 𝑘)))
5655ad2antrr 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → Fun (𝐻‘(𝑁‘suc 𝑘)))
5711adantr 274 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 ∈ ℕ0)
586, 14mp1i 10 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ω) → 𝑁:ω⟶ℕ0)
5916adantl 275 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ω) → suc 𝑘 ∈ ω)
6058, 59ffvelrnd 5567 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ω) → (𝑁‘suc 𝑘) ∈ ℕ0)
6160adantrr 471 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘suc 𝑘) ∈ ℕ0)
6257nn0red 9082 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 ∈ ℝ)
6361nn0red 9082 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘suc 𝑘) ∈ ℝ)
64 f1ocnvfv2 5690 . . . . . . . . . . . . . . . . . . 19 ((𝑁:ω–1-1-onto→ℕ0𝑃 ∈ ℕ0) → (𝑁‘(𝑁𝑃)) = 𝑃)
656, 57, 64sylancr 411 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘(𝑁𝑃)) = 𝑃)
6612adantr 274 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁𝑃) ∈ ω)
67 simprr 522 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))
6837, 25, 66, 67ennnfonelemk 11983 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁𝑃) ∈ 𝑘)
69 elelsuc 4341 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑃) ∈ 𝑘 → (𝑁𝑃) ∈ suc 𝑘)
7068, 69syl 14 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁𝑃) ∈ suc 𝑘)
71 0zd 9117 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 0 ∈ ℤ)
7271, 5, 66, 17frec2uzltd 10234 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝑁𝑃) ∈ suc 𝑘 → (𝑁‘(𝑁𝑃)) < (𝑁‘suc 𝑘)))
7370, 72mpd 13 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘(𝑁𝑃)) < (𝑁‘suc 𝑘))
7465, 73eqbrtrrd 3961 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 < (𝑁‘suc 𝑘))
7562, 63, 74ltled 7932 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → 𝑃 ≤ (𝑁‘suc 𝑘))
7636, 37, 38, 50, 5, 51, 52, 57, 61, 75ennnfoneleminc 11994 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)))
7776ad2antrr 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → (𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)))
78 simpr 109 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → 𝑠 ∈ dom (𝐻𝑃))
79 funssfv 5458 . . . . . . . . . . . . . 14 ((Fun (𝐻‘(𝑁‘suc 𝑘)) ∧ (𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)) ∧ 𝑠 ∈ dom (𝐻𝑃)) → ((𝐻‘(𝑁‘suc 𝑘))‘𝑠) = ((𝐻𝑃)‘𝑠))
8056, 77, 78, 79syl3anc 1217 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → ((𝐻‘(𝑁‘suc 𝑘))‘𝑠) = ((𝐻𝑃)‘𝑠))
8180eqcomd 2146 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻𝑃)) → ((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))
8281ralrimiva 2509 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))
8336, 37, 49, 50, 5, 51, 52, 57ennnfonelemhf1o 11996 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)))
84 f1ofun 5380 . . . . . . . . . . . . . 14 ((𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)) → Fun (𝐻𝑃))
8583, 84syl 14 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → Fun (𝐻𝑃))
86 eqfunfv 5534 . . . . . . . . . . . . 13 ((Fun (𝐻𝑃) ∧ Fun (𝐻‘(𝑁‘suc 𝑘))) → ((𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))))
8785, 55, 86syl2anc 409 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))))
8887adantr 274 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ((𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻𝑃)((𝐻𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠))))
8934, 82, 88mpbir2and 929 . . . . . . . . . 10 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐻𝑃) = (𝐻‘(𝑁‘suc 𝑘)))
9089rneqd 4779 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻𝑃) = ran (𝐻‘(𝑁‘suc 𝑘)))
91 dff1o5 5387 . . . . . . . . . . . 12 ((𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)) ↔ ((𝐻𝑃):dom (𝐻𝑃)–1-1→(𝐹 “ (𝑁𝑃)) ∧ ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃))))
9283, 91sylib 121 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝐻𝑃):dom (𝐻𝑃)–1-1→(𝐹 “ (𝑁𝑃)) ∧ ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃))))
9392simprd 113 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃)))
9493adantr 274 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻𝑃) = (𝐹 “ (𝑁𝑃)))
95 f1ocnvfv1 5689 . . . . . . . . . . . . . . . 16 ((𝑁:ω–1-1-onto→ℕ0 ∧ suc 𝑘 ∈ ω) → (𝑁‘(𝑁‘suc 𝑘)) = suc 𝑘)
966, 17, 95sylancr 411 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝑁‘(𝑁‘suc 𝑘)) = suc 𝑘)
9796imaeq2d 4892 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐹 “ (𝑁‘(𝑁‘suc 𝑘))) = (𝐹 “ suc 𝑘))
98 f1oeq3 5369 . . . . . . . . . . . . . 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 146 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘))
101 dff1o5 5387 . . . . . . . . . . . 12 ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘) ↔ ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1→(𝐹 “ suc 𝑘) ∧ ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘)))
102100, 101sylib 121 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1→(𝐹 “ suc 𝑘) ∧ ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘)))
103102simprd 113 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘))
104103adantr 274 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘))
10590, 94, 1043eqtr3d 2181 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹 “ (𝑁𝑃)) = (𝐹 “ suc 𝑘))
10633, 105eleqtrrd 2220 . . . . . . 7 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹𝑘) ∈ (𝐹 “ (𝑁𝑃)))
107 fvelima 5484 . . . . . . 7 ((Fun 𝐹 ∧ (𝐹𝑘) ∈ (𝐹 “ (𝑁𝑃))) → ∃𝑞 ∈ (𝑁𝑃)(𝐹𝑞) = (𝐹𝑘))
10822, 106, 107syl2anc 409 . . . . . 6 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ∃𝑞 ∈ (𝑁𝑃)(𝐹𝑞) = (𝐹𝑘))
109 simprr 522 . . . . . . 7 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → (𝐹𝑞) = (𝐹𝑘))
110 fveq2 5432 . . . . . . . . . 10 (𝑗 = 𝑞 → (𝐹𝑗) = (𝐹𝑞))
111110neeq2d 2328 . . . . . . . . 9 (𝑗 = 𝑞 → ((𝐹𝑘) ≠ (𝐹𝑗) ↔ (𝐹𝑘) ≠ (𝐹𝑞)))
11267ad2antrr 480 . . . . . . . . 9 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))
113 elelsuc 4341 . . . . . . . . . 10 (𝑞 ∈ (𝑁𝑃) → 𝑞 ∈ suc (𝑁𝑃))
114113ad2antrl 482 . . . . . . . . 9 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → 𝑞 ∈ suc (𝑁𝑃))
115111, 112, 114rspcdva 2799 . . . . . . . 8 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → (𝐹𝑘) ≠ (𝐹𝑞))
116115necomd 2395 . . . . . . 7 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → (𝐹𝑞) ≠ (𝐹𝑘))
117109, 116pm2.21ddne 2392 . . . . . 6 ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (𝑁𝑃) ∧ (𝐹𝑞) = (𝐹𝑘))) → ⊥)
118108, 117rexlimddv 2558 . . . . 5 (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) ∧ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ⊥)
119118inegd 1351 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ¬ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)))
120 dmss 4749 . . . . . 6 ((𝐻𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)) → dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)))
12176, 120syl 14 . . . . 5 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)))
12235, 19, 4, 50, 5, 51, 52, 11ennnfonelemom 11991 . . . . . . 7 (𝜑 → dom (𝐻𝑃) ∈ ω)
123122adantr 274 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻𝑃) ∈ ω)
12442a1i 9 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎)))
125124ralbidv 2439 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗) ↔ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎)))
12638, 125mpbid 146 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑎))
12736, 37, 126, 50, 5, 51, 52, 61ennnfonelemom 11991 . . . . . 6 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω)
128 nntri1 6403 . . . . . 6 ((dom (𝐻𝑃) ∈ ω ∧ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω) → (dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)) ↔ ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
129123, 127, 128syl2anc 409 . . . . 5 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (dom (𝐻𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)) ↔ ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
130121, 129mpbid 146 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃))
131 nntri3or 6400 . . . . 5 ((dom (𝐻𝑃) ∈ ω ∧ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω) → (dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
132123, 127, 131syl2anc 409 . . . 4 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → (dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻𝑃)))
133119, 130, 132ecase23d 1329 . . 3 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)))
134 fveq2 5432 . . . . . 6 (𝑖 = (𝑁‘suc 𝑘) → (𝐻𝑖) = (𝐻‘(𝑁‘suc 𝑘)))
135134dmeqd 4752 . . . . 5 (𝑖 = (𝑁‘suc 𝑘) → dom (𝐻𝑖) = dom (𝐻‘(𝑁‘suc 𝑘)))
136135eleq2d 2210 . . . 4 (𝑖 = (𝑁‘suc 𝑘) → (dom (𝐻𝑃) ∈ dom (𝐻𝑖) ↔ dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘))))
137136rspcev 2794 . . 3 (((𝑁‘suc 𝑘) ∈ ℕ0 ∧ dom (𝐻𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘))) → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
13818, 133, 137syl2anc 409 . 2 ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (𝑁𝑃)(𝐹𝑘) ≠ (𝐹𝑗))) → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
13913, 138rexlimddv 2558 1 (𝜑 → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 820   ∨ w3o 962   = wceq 1332  ⊥wfal 1337   ∈ wcel 1481   ≠ wne 2309  ∀wral 2417  ∃wrex 2418   ∪ cun 3075   ⊆ wss 3077  ∅c0 3369  ifcif 3480  {csn 3533  ⟨cop 3536   class class class wbr 3938   ↦ cmpt 3998  suc csuc 4297  ωcom 4514  ◡ccnv 4549  dom cdm 4550  ran crn 4551   “ cima 4553  Fun wfun 5128  ⟶wf 5130  –1-1→wf1 5131  –onto→wfo 5132  –1-1-onto→wf1o 5133  ‘cfv 5134  (class class class)co 5785   ∈ cmpo 5787  freccfrec 6298   ↑pm cpm 6554  0cc0 7671  1c1 7672   + caddc 7674   < clt 7851   − cmin 7984  ℕ0cn0 9028  ℤcz 9105  seqcseq 10276 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-iinf 4512  ax-cnex 7762  ax-resscn 7763  ax-1cn 7764  ax-1re 7765  ax-icn 7766  ax-addcl 7767  ax-addrcl 7768  ax-mulcl 7769  ax-addcom 7771  ax-addass 7773  ax-distr 7775  ax-i2m1 7776  ax-0lt1 7777  ax-0id 7779  ax-rnegex 7780  ax-cnre 7782  ax-pre-ltirr 7783  ax-pre-ltwlin 7784  ax-pre-lttrn 7785  ax-pre-ltadd 7787 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4225  df-iord 4298  df-on 4300  df-ilim 4301  df-suc 4303  df-iom 4515  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-rn 4561  df-res 4562  df-ima 4563  df-iota 5099  df-fun 5136  df-fn 5137  df-f 5138  df-f1 5139  df-fo 5140  df-f1o 5141  df-fv 5142  df-riota 5741  df-ov 5788  df-oprab 5789  df-mpo 5790  df-1st 6049  df-2nd 6050  df-recs 6213  df-frec 6299  df-pm 6556  df-pnf 7853  df-mnf 7854  df-xr 7855  df-ltxr 7856  df-le 7857  df-sub 7986  df-neg 7987  df-inn 8772  df-n0 9029  df-z 9106  df-uz 9378  df-seqfrec 10277 This theorem is referenced by:  ennnfonelemhom  11998
 Copyright terms: Public domain W3C validator