| Step | Hyp | Ref
 | Expression | 
| 1 |   | suceq 4437 | 
. . . . 5
⊢ (𝑛 = (◡𝑁‘𝑃) → suc 𝑛 = suc (◡𝑁‘𝑃)) | 
| 2 | 1 | raleqdv 2699 | 
. . . 4
⊢ (𝑛 = (◡𝑁‘𝑃) → (∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) | 
| 3 | 2 | rexbidv 2498 | 
. . 3
⊢ (𝑛 = (◡𝑁‘𝑃) → (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∃𝑘 ∈ ω ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) | 
| 4 |   | ennnfonelemh.ne | 
. . 3
⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗)) | 
| 5 |   | ennnfonelemh.n | 
. . . . . . 7
⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) | 
| 6 | 5 | frechashgf1o 10520 | 
. . . . . 6
⊢ 𝑁:ω–1-1-onto→ℕ0 | 
| 7 |   | f1ocnv 5517 | 
. . . . . 6
⊢ (𝑁:ω–1-1-onto→ℕ0 → ◡𝑁:ℕ0–1-1-onto→ω) | 
| 8 | 6, 7 | ax-mp 5 | 
. . . . 5
⊢ ◡𝑁:ℕ0–1-1-onto→ω | 
| 9 |   | f1of 5504 | 
. . . . 5
⊢ (◡𝑁:ℕ0–1-1-onto→ω → ◡𝑁:ℕ0⟶ω) | 
| 10 | 8, 9 | mp1i 10 | 
. . . 4
⊢ (𝜑 → ◡𝑁:ℕ0⟶ω) | 
| 11 |   | ennnfonelemex.p | 
. . . 4
⊢ (𝜑 → 𝑃 ∈
ℕ0) | 
| 12 | 10, 11 | ffvelcdmd 5698 | 
. . 3
⊢ (𝜑 → (◡𝑁‘𝑃) ∈ ω) | 
| 13 | 3, 4, 12 | rspcdva 2873 | 
. 2
⊢ (𝜑 → ∃𝑘 ∈ ω ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) | 
| 14 |   | f1of 5504 | 
. . . . 5
⊢ (𝑁:ω–1-1-onto→ℕ0 → 𝑁:ω⟶ℕ0) | 
| 15 | 6, 14 | mp1i 10 | 
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 𝑁:ω⟶ℕ0) | 
| 16 |   | peano2 4631 | 
. . . . 5
⊢ (𝑘 ∈ ω → suc 𝑘 ∈
ω) | 
| 17 | 16 | ad2antrl 490 | 
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → suc 𝑘 ∈ ω) | 
| 18 | 15, 17 | ffvelcdmd 5698 | 
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝑁‘suc 𝑘) ∈
ℕ0) | 
| 19 |   | ennnfonelemh.f | 
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ω–onto→𝐴) | 
| 20 | 19 | ad2antrr 488 | 
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝐹:ω–onto→𝐴) | 
| 21 |   | fofun 5481 | 
. . . . . . . 8
⊢ (𝐹:ω–onto→𝐴 → Fun 𝐹) | 
| 22 | 20, 21 | syl 14 | 
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → Fun 𝐹) | 
| 23 |   | vex 2766 | 
. . . . . . . . . 10
⊢ 𝑘 ∈ V | 
| 24 | 23 | sucid 4452 | 
. . . . . . . . 9
⊢ 𝑘 ∈ suc 𝑘 | 
| 25 |   | simprl 529 | 
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 𝑘 ∈ ω) | 
| 26 | 25 | adantr 276 | 
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝑘 ∈ ω) | 
| 27 |   | fof 5480 | 
. . . . . . . . . . . 12
⊢ (𝐹:ω–onto→𝐴 → 𝐹:ω⟶𝐴) | 
| 28 |   | fdm 5413 | 
. . . . . . . . . . . 12
⊢ (𝐹:ω⟶𝐴 → dom 𝐹 = ω) | 
| 29 | 20, 27, 28 | 3syl 17 | 
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → dom 𝐹 = ω) | 
| 30 | 26, 29 | eleqtrrd 2276 | 
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → 𝑘 ∈ dom 𝐹) | 
| 31 |   | funfvima 5794 | 
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑘 ∈ dom 𝐹) → (𝑘 ∈ suc 𝑘 → (𝐹‘𝑘) ∈ (𝐹 “ suc 𝑘))) | 
| 32 | 22, 30, 31 | syl2anc 411 | 
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝑘 ∈ suc 𝑘 → (𝐹‘𝑘) ∈ (𝐹 “ suc 𝑘))) | 
| 33 | 24, 32 | mpi 15 | 
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹‘𝑘) ∈ (𝐹 “ suc 𝑘)) | 
| 34 |   | simpr 110 | 
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) | 
| 35 |   | ennnfonelemh.dceq | 
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) | 
| 36 | 35 | adantr 276 | 
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) | 
| 37 | 19 | adantr 276 | 
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 𝐹:ω–onto→𝐴) | 
| 38 | 4 | adantr 276 | 
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗)) | 
| 39 |   | fveq2 5558 | 
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑎 → (𝐹‘𝑗) = (𝐹‘𝑎)) | 
| 40 | 39 | neeq2d 2386 | 
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑎 → ((𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ (𝐹‘𝑘) ≠ (𝐹‘𝑎))) | 
| 41 | 40 | cbvralv 2729 | 
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑗 ∈
suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∀𝑎 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑎)) | 
| 42 | 41 | rexbii 2504 | 
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑘 ∈
ω ∀𝑗 ∈
suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑎)) | 
| 43 |   | fveq2 5558 | 
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑏 → (𝐹‘𝑘) = (𝐹‘𝑏)) | 
| 44 | 43 | neeq1d 2385 | 
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑏 → ((𝐹‘𝑘) ≠ (𝐹‘𝑎) ↔ (𝐹‘𝑏) ≠ (𝐹‘𝑎))) | 
| 45 | 44 | ralbidv 2497 | 
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑏 → (∀𝑎 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑎) ↔ ∀𝑎 ∈ suc 𝑛(𝐹‘𝑏) ≠ (𝐹‘𝑎))) | 
| 46 | 45 | cbvrexv 2730 | 
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑘 ∈
ω ∀𝑎 ∈
suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑎) ↔ ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑏) ≠ (𝐹‘𝑎)) | 
| 47 | 42, 46 | bitri 184 | 
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑘 ∈
ω ∀𝑗 ∈
suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑏) ≠ (𝐹‘𝑎)) | 
| 48 | 47 | ralbii 2503 | 
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ω ∃𝑘 ∈
ω ∀𝑗 ∈
suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∀𝑛 ∈ ω ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑏) ≠ (𝐹‘𝑎)) | 
| 49 | 38, 48 | sylib 122 | 
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ∀𝑛 ∈ ω ∃𝑏 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑏) ≠ (𝐹‘𝑎)) | 
| 50 |   | ennnfonelemh.g | 
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦
if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {〈dom 𝑥, (𝐹‘𝑦)〉}))) | 
| 51 |   | ennnfonelemh.j | 
. . . . . . . . . . . . . . . . 17
⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1)))) | 
| 52 |   | ennnfonelemh.h | 
. . . . . . . . . . . . . . . . 17
⊢ 𝐻 = seq0(𝐺, 𝐽) | 
| 53 | 36, 37, 49, 50, 5, 51, 52, 18 | ennnfonelemhf1o 12630 | 
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (◡𝑁‘(𝑁‘suc 𝑘)))) | 
| 54 |   | f1ofun 5506 | 
. . . . . . . . . . . . . . . 16
⊢ ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (◡𝑁‘(𝑁‘suc 𝑘))) → Fun (𝐻‘(𝑁‘suc 𝑘))) | 
| 55 | 53, 54 | syl 14 | 
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → Fun (𝐻‘(𝑁‘suc 𝑘))) | 
| 56 | 55 | ad2antrr 488 | 
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻‘𝑃)) → Fun (𝐻‘(𝑁‘suc 𝑘))) | 
| 57 | 11 | adantr 276 | 
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 𝑃 ∈
ℕ0) | 
| 58 | 6, 14 | mp1i 10 | 
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → 𝑁:ω⟶ℕ0) | 
| 59 | 16 | adantl 277 | 
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → suc 𝑘 ∈
ω) | 
| 60 | 58, 59 | ffvelcdmd 5698 | 
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → (𝑁‘suc 𝑘) ∈
ℕ0) | 
| 61 | 60 | adantrr 479 | 
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝑁‘suc 𝑘) ∈
ℕ0) | 
| 62 | 57 | nn0red 9303 | 
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 𝑃 ∈ ℝ) | 
| 63 | 61 | nn0red 9303 | 
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝑁‘suc 𝑘) ∈ ℝ) | 
| 64 |   | f1ocnvfv2 5825 | 
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁:ω–1-1-onto→ℕ0 ∧ 𝑃 ∈ ℕ0) → (𝑁‘(◡𝑁‘𝑃)) = 𝑃) | 
| 65 | 6, 57, 64 | sylancr 414 | 
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝑁‘(◡𝑁‘𝑃)) = 𝑃) | 
| 66 | 12 | adantr 276 | 
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (◡𝑁‘𝑃) ∈ ω) | 
| 67 |   | simprr 531 | 
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) | 
| 68 | 37, 25, 66, 67 | ennnfonelemk 12617 | 
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (◡𝑁‘𝑃) ∈ 𝑘) | 
| 69 |   | elelsuc 4444 | 
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡𝑁‘𝑃) ∈ 𝑘 → (◡𝑁‘𝑃) ∈ suc 𝑘) | 
| 70 | 68, 69 | syl 14 | 
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (◡𝑁‘𝑃) ∈ suc 𝑘) | 
| 71 |   | 0zd 9338 | 
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 0 ∈ ℤ) | 
| 72 | 71, 5, 66, 17 | frec2uzltd 10495 | 
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ((◡𝑁‘𝑃) ∈ suc 𝑘 → (𝑁‘(◡𝑁‘𝑃)) < (𝑁‘suc 𝑘))) | 
| 73 | 70, 72 | mpd 13 | 
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝑁‘(◡𝑁‘𝑃)) < (𝑁‘suc 𝑘)) | 
| 74 | 65, 73 | eqbrtrrd 4057 | 
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 𝑃 < (𝑁‘suc 𝑘)) | 
| 75 | 62, 63, 74 | ltled 8145 | 
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → 𝑃 ≤ (𝑁‘suc 𝑘)) | 
| 76 | 36, 37, 38, 50, 5, 51, 52, 57, 61, 75 | ennnfoneleminc 12628 | 
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝐻‘𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘))) | 
| 77 | 76 | ad2antrr 488 | 
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻‘𝑃)) → (𝐻‘𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘))) | 
| 78 |   | simpr 110 | 
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻‘𝑃)) → 𝑠 ∈ dom (𝐻‘𝑃)) | 
| 79 |   | funssfv 5584 | 
. . . . . . . . . . . . . 14
⊢ ((Fun
(𝐻‘(𝑁‘suc 𝑘)) ∧ (𝐻‘𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)) ∧ 𝑠 ∈ dom (𝐻‘𝑃)) → ((𝐻‘(𝑁‘suc 𝑘))‘𝑠) = ((𝐻‘𝑃)‘𝑠)) | 
| 80 | 56, 77, 78, 79 | syl3anc 1249 | 
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻‘𝑃)) → ((𝐻‘(𝑁‘suc 𝑘))‘𝑠) = ((𝐻‘𝑃)‘𝑠)) | 
| 81 | 80 | eqcomd 2202 | 
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ 𝑠 ∈ dom (𝐻‘𝑃)) → ((𝐻‘𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠)) | 
| 82 | 81 | ralrimiva 2570 | 
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ∀𝑠 ∈ dom (𝐻‘𝑃)((𝐻‘𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠)) | 
| 83 | 36, 37, 49, 50, 5, 51, 52, 57 | ennnfonelemhf1o 12630 | 
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (◡𝑁‘𝑃))) | 
| 84 |   | f1ofun 5506 | 
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (◡𝑁‘𝑃)) → Fun (𝐻‘𝑃)) | 
| 85 | 83, 84 | syl 14 | 
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → Fun (𝐻‘𝑃)) | 
| 86 |   | eqfunfv 5664 | 
. . . . . . . . . . . . 13
⊢ ((Fun
(𝐻‘𝑃) ∧ Fun (𝐻‘(𝑁‘suc 𝑘))) → ((𝐻‘𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻‘𝑃)((𝐻‘𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠)))) | 
| 87 | 85, 55, 86 | syl2anc 411 | 
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ((𝐻‘𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻‘𝑃)((𝐻‘𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠)))) | 
| 88 | 87 | adantr 276 | 
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ((𝐻‘𝑃) = (𝐻‘(𝑁‘suc 𝑘)) ↔ (dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∧ ∀𝑠 ∈ dom (𝐻‘𝑃)((𝐻‘𝑃)‘𝑠) = ((𝐻‘(𝑁‘suc 𝑘))‘𝑠)))) | 
| 89 | 34, 82, 88 | mpbir2and 946 | 
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐻‘𝑃) = (𝐻‘(𝑁‘suc 𝑘))) | 
| 90 | 89 | rneqd 4895 | 
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻‘𝑃) = ran (𝐻‘(𝑁‘suc 𝑘))) | 
| 91 |   | dff1o5 5513 | 
. . . . . . . . . . . 12
⊢ ((𝐻‘𝑃):dom (𝐻‘𝑃)–1-1-onto→(𝐹 “ (◡𝑁‘𝑃)) ↔ ((𝐻‘𝑃):dom (𝐻‘𝑃)–1-1→(𝐹 “ (◡𝑁‘𝑃)) ∧ ran (𝐻‘𝑃) = (𝐹 “ (◡𝑁‘𝑃)))) | 
| 92 | 83, 91 | sylib 122 | 
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ((𝐻‘𝑃):dom (𝐻‘𝑃)–1-1→(𝐹 “ (◡𝑁‘𝑃)) ∧ ran (𝐻‘𝑃) = (𝐹 “ (◡𝑁‘𝑃)))) | 
| 93 | 92 | simprd 114 | 
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ran (𝐻‘𝑃) = (𝐹 “ (◡𝑁‘𝑃))) | 
| 94 | 93 | adantr 276 | 
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻‘𝑃) = (𝐹 “ (◡𝑁‘𝑃))) | 
| 95 |   | f1ocnvfv1 5824 | 
. . . . . . . . . . . . . . . 16
⊢ ((𝑁:ω–1-1-onto→ℕ0 ∧ suc 𝑘 ∈ ω) → (◡𝑁‘(𝑁‘suc 𝑘)) = suc 𝑘) | 
| 96 | 6, 17, 95 | sylancr 414 | 
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (◡𝑁‘(𝑁‘suc 𝑘)) = suc 𝑘) | 
| 97 | 96 | imaeq2d 5009 | 
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝐹 “ (◡𝑁‘(𝑁‘suc 𝑘))) = (𝐹 “ suc 𝑘)) | 
| 98 |   | f1oeq3 5494 | 
. . . . . . . . . . . . . 14
⊢ ((𝐹 “ (◡𝑁‘(𝑁‘suc 𝑘))) = (𝐹 “ suc 𝑘) → ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (◡𝑁‘(𝑁‘suc 𝑘))) ↔ (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘))) | 
| 99 | 97, 98 | syl 14 | 
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ (◡𝑁‘(𝑁‘suc 𝑘))) ↔ (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘))) | 
| 100 | 53, 99 | mpbid 147 | 
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘)) | 
| 101 |   | dff1o5 5513 | 
. . . . . . . . . . . 12
⊢ ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1-onto→(𝐹 “ suc 𝑘) ↔ ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1→(𝐹 “ suc 𝑘) ∧ ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘))) | 
| 102 | 100, 101 | sylib 122 | 
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ((𝐻‘(𝑁‘suc 𝑘)):dom (𝐻‘(𝑁‘suc 𝑘))–1-1→(𝐹 “ suc 𝑘) ∧ ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘))) | 
| 103 | 102 | simprd 114 | 
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘)) | 
| 104 | 103 | adantr 276 | 
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ran (𝐻‘(𝑁‘suc 𝑘)) = (𝐹 “ suc 𝑘)) | 
| 105 | 90, 94, 104 | 3eqtr3d 2237 | 
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹 “ (◡𝑁‘𝑃)) = (𝐹 “ suc 𝑘)) | 
| 106 | 33, 105 | eleqtrrd 2276 | 
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → (𝐹‘𝑘) ∈ (𝐹 “ (◡𝑁‘𝑃))) | 
| 107 |   | fvelima 5612 | 
. . . . . . 7
⊢ ((Fun
𝐹 ∧ (𝐹‘𝑘) ∈ (𝐹 “ (◡𝑁‘𝑃))) → ∃𝑞 ∈ (◡𝑁‘𝑃)(𝐹‘𝑞) = (𝐹‘𝑘)) | 
| 108 | 22, 106, 107 | syl2anc 411 | 
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ∃𝑞 ∈ (◡𝑁‘𝑃)(𝐹‘𝑞) = (𝐹‘𝑘)) | 
| 109 |   | simprr 531 | 
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (◡𝑁‘𝑃) ∧ (𝐹‘𝑞) = (𝐹‘𝑘))) → (𝐹‘𝑞) = (𝐹‘𝑘)) | 
| 110 |   | fveq2 5558 | 
. . . . . . . . . 10
⊢ (𝑗 = 𝑞 → (𝐹‘𝑗) = (𝐹‘𝑞)) | 
| 111 | 110 | neeq2d 2386 | 
. . . . . . . . 9
⊢ (𝑗 = 𝑞 → ((𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ (𝐹‘𝑘) ≠ (𝐹‘𝑞))) | 
| 112 | 67 | ad2antrr 488 | 
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (◡𝑁‘𝑃) ∧ (𝐹‘𝑞) = (𝐹‘𝑘))) → ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) | 
| 113 |   | elelsuc 4444 | 
. . . . . . . . . 10
⊢ (𝑞 ∈ (◡𝑁‘𝑃) → 𝑞 ∈ suc (◡𝑁‘𝑃)) | 
| 114 | 113 | ad2antrl 490 | 
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (◡𝑁‘𝑃) ∧ (𝐹‘𝑞) = (𝐹‘𝑘))) → 𝑞 ∈ suc (◡𝑁‘𝑃)) | 
| 115 | 111, 112,
114 | rspcdva 2873 | 
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (◡𝑁‘𝑃) ∧ (𝐹‘𝑞) = (𝐹‘𝑘))) → (𝐹‘𝑘) ≠ (𝐹‘𝑞)) | 
| 116 | 115 | necomd 2453 | 
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (◡𝑁‘𝑃) ∧ (𝐹‘𝑞) = (𝐹‘𝑘))) → (𝐹‘𝑞) ≠ (𝐹‘𝑘)) | 
| 117 | 109, 116 | pm2.21ddne 2450 | 
. . . . . 6
⊢ ((((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) ∧ (𝑞 ∈ (◡𝑁‘𝑃) ∧ (𝐹‘𝑞) = (𝐹‘𝑘))) → ⊥) | 
| 118 | 108, 117 | rexlimddv 2619 | 
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) ∧ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) → ⊥) | 
| 119 | 118 | inegd 1383 | 
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ¬ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘))) | 
| 120 |   | dmss 4865 | 
. . . . . 6
⊢ ((𝐻‘𝑃) ⊆ (𝐻‘(𝑁‘suc 𝑘)) → dom (𝐻‘𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘))) | 
| 121 | 76, 120 | syl 14 | 
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → dom (𝐻‘𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘))) | 
| 122 | 35, 19, 4, 50, 5, 51, 52, 11 | ennnfonelemom 12625 | 
. . . . . . 7
⊢ (𝜑 → dom (𝐻‘𝑃) ∈ ω) | 
| 123 | 122 | adantr 276 | 
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → dom (𝐻‘𝑃) ∈ ω) | 
| 124 | 42 | a1i 9 | 
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑎))) | 
| 125 | 124 | ralbidv 2497 | 
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗) ↔ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑎))) | 
| 126 | 38, 125 | mpbid 147 | 
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑎 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑎)) | 
| 127 | 36, 37, 126, 50, 5, 51, 52, 61 | ennnfonelemom 12625 | 
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω) | 
| 128 |   | nntri1 6554 | 
. . . . . 6
⊢ ((dom
(𝐻‘𝑃) ∈ ω ∧ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω) → (dom (𝐻‘𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)) ↔ ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻‘𝑃))) | 
| 129 | 123, 127,
128 | syl2anc 411 | 
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (dom (𝐻‘𝑃) ⊆ dom (𝐻‘(𝑁‘suc 𝑘)) ↔ ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻‘𝑃))) | 
| 130 | 121, 129 | mpbid 147 | 
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ¬ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻‘𝑃)) | 
| 131 |   | nntri3or 6551 | 
. . . . 5
⊢ ((dom
(𝐻‘𝑃) ∈ ω ∧ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ ω) → (dom (𝐻‘𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻‘𝑃))) | 
| 132 | 123, 127,
131 | syl2anc 411 | 
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → (dom (𝐻‘𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘𝑃) = dom (𝐻‘(𝑁‘suc 𝑘)) ∨ dom (𝐻‘(𝑁‘suc 𝑘)) ∈ dom (𝐻‘𝑃))) | 
| 133 | 119, 130,
132 | ecase23d 1361 | 
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → dom (𝐻‘𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘))) | 
| 134 |   | fveq2 5558 | 
. . . . . 6
⊢ (𝑖 = (𝑁‘suc 𝑘) → (𝐻‘𝑖) = (𝐻‘(𝑁‘suc 𝑘))) | 
| 135 | 134 | dmeqd 4868 | 
. . . . 5
⊢ (𝑖 = (𝑁‘suc 𝑘) → dom (𝐻‘𝑖) = dom (𝐻‘(𝑁‘suc 𝑘))) | 
| 136 | 135 | eleq2d 2266 | 
. . . 4
⊢ (𝑖 = (𝑁‘suc 𝑘) → (dom (𝐻‘𝑃) ∈ dom (𝐻‘𝑖) ↔ dom (𝐻‘𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘)))) | 
| 137 | 136 | rspcev 2868 | 
. . 3
⊢ (((𝑁‘suc 𝑘) ∈ ℕ0 ∧ dom (𝐻‘𝑃) ∈ dom (𝐻‘(𝑁‘suc 𝑘))) → ∃𝑖 ∈ ℕ0 dom (𝐻‘𝑃) ∈ dom (𝐻‘𝑖)) | 
| 138 | 18, 133, 137 | syl2anc 411 | 
. 2
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ ∀𝑗 ∈ suc (◡𝑁‘𝑃)(𝐹‘𝑘) ≠ (𝐹‘𝑗))) → ∃𝑖 ∈ ℕ0 dom (𝐻‘𝑃) ∈ dom (𝐻‘𝑖)) | 
| 139 | 13, 138 | rexlimddv 2619 | 
1
⊢ (𝜑 → ∃𝑖 ∈ ℕ0 dom (𝐻‘𝑃) ∈ dom (𝐻‘𝑖)) |