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

Theorem ennnfonelemex 12415
Description: Lemma for ennnfone 12426. 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 4403 . . . . 5 (𝑛 = (β—‘π‘β€˜π‘ƒ) β†’ suc 𝑛 = suc (β—‘π‘β€˜π‘ƒ))
21raleqdv 2679 . . . 4 (𝑛 = (β—‘π‘β€˜π‘ƒ) β†’ (βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—)))
32rexbidv 2478 . . 3 (𝑛 = (β—‘π‘β€˜π‘ƒ) β†’ (βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—)))
4 ennnfonelemh.ne . . 3 (πœ‘ β†’ βˆ€π‘› ∈ Ο‰ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))
5 ennnfonelemh.n . . . . . . 7 𝑁 = frec((π‘₯ ∈ β„€ ↦ (π‘₯ + 1)), 0)
65frechashgf1o 10428 . . . . . 6 𝑁:ω–1-1-ontoβ†’β„•0
7 f1ocnv 5475 . . . . . 6 (𝑁:ω–1-1-ontoβ†’β„•0 β†’ ◑𝑁:β„•0–1-1-ontoβ†’Ο‰)
86, 7ax-mp 5 . . . . 5 ◑𝑁:β„•0–1-1-ontoβ†’Ο‰
9 f1of 5462 . . . . 5 (◑𝑁:β„•0–1-1-ontoβ†’Ο‰ β†’ ◑𝑁:β„•0βŸΆΟ‰)
108, 9mp1i 10 . . . 4 (πœ‘ β†’ ◑𝑁:β„•0βŸΆΟ‰)
11 ennnfonelemex.p . . . 4 (πœ‘ β†’ 𝑃 ∈ β„•0)
1210, 11ffvelcdmd 5653 . . 3 (πœ‘ β†’ (β—‘π‘β€˜π‘ƒ) ∈ Ο‰)
133, 4, 12rspcdva 2847 . 2 (πœ‘ β†’ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))
14 f1of 5462 . . . . 5 (𝑁:ω–1-1-ontoβ†’β„•0 β†’ 𝑁:Ο‰βŸΆβ„•0)
156, 14mp1i 10 . . . 4 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ 𝑁:Ο‰βŸΆβ„•0)
16 peano2 4595 . . . . 5 (π‘˜ ∈ Ο‰ β†’ suc π‘˜ ∈ Ο‰)
1716ad2antrl 490 . . . 4 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ suc π‘˜ ∈ Ο‰)
1815, 17ffvelcdmd 5653 . . 3 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (π‘β€˜suc π‘˜) ∈ β„•0)
19 ennnfonelemh.f . . . . . . . . 9 (πœ‘ β†’ 𝐹:ω–onto→𝐴)
2019ad2antrr 488 . . . . . . . 8 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ 𝐹:ω–onto→𝐴)
21 fofun 5440 . . . . . . . 8 (𝐹:ω–onto→𝐴 β†’ Fun 𝐹)
2220, 21syl 14 . . . . . . 7 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ Fun 𝐹)
23 vex 2741 . . . . . . . . . 10 π‘˜ ∈ V
2423sucid 4418 . . . . . . . . 9 π‘˜ ∈ suc π‘˜
25 simprl 529 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ π‘˜ ∈ Ο‰)
2625adantr 276 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ π‘˜ ∈ Ο‰)
27 fof 5439 . . . . . . . . . . . 12 (𝐹:ω–onto→𝐴 β†’ 𝐹:Ο‰βŸΆπ΄)
28 fdm 5372 . . . . . . . . . . . 12 (𝐹:Ο‰βŸΆπ΄ β†’ dom 𝐹 = Ο‰)
2920, 27, 283syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ dom 𝐹 = Ο‰)
3026, 29eleqtrrd 2257 . . . . . . . . . 10 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ π‘˜ ∈ dom 𝐹)
31 funfvima 5749 . . . . . . . . . 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 5516 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = π‘Ž β†’ (πΉβ€˜π‘—) = (πΉβ€˜π‘Ž))
4039neeq2d 2366 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = π‘Ž β†’ ((πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ (πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž)))
4140cbvralv 2704 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž))
4241rexbii 2484 . . . . . . . . . . . . . . . . . . . 20 (βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž))
43 fveq2 5516 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ = 𝑏 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘))
4443neeq1d 2365 . . . . . . . . . . . . . . . . . . . . . 22 (π‘˜ = 𝑏 β†’ ((πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž) ↔ (πΉβ€˜π‘) β‰  (πΉβ€˜π‘Ž)))
4544ralbidv 2477 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ = 𝑏 β†’ (βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž) ↔ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘) β‰  (πΉβ€˜π‘Ž)))
4645cbvrexv 2705 . . . . . . . . . . . . . . . . . . . 20 (βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž) ↔ βˆƒπ‘ ∈ Ο‰ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘) β‰  (πΉβ€˜π‘Ž))
4742, 46bitri 184 . . . . . . . . . . . . . . . . . . 19 (βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ βˆƒπ‘ ∈ Ο‰ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘) β‰  (πΉβ€˜π‘Ž))
4847ralbii 2483 . . . . . . . . . . . . . . . . . 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 12414 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (π»β€˜(π‘β€˜suc π‘˜)):dom (π»β€˜(π‘β€˜suc π‘˜))–1-1-ontoβ†’(𝐹 β€œ (β—‘π‘β€˜(π‘β€˜suc π‘˜))))
54 f1ofun 5464 . . . . . . . . . . . . . . . 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 5653 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ Ο‰) β†’ (π‘β€˜suc π‘˜) ∈ β„•0)
6160adantrr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (π‘β€˜suc π‘˜) ∈ β„•0)
6257nn0red 9230 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ 𝑃 ∈ ℝ)
6361nn0red 9230 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (π‘β€˜suc π‘˜) ∈ ℝ)
64 f1ocnvfv2 5779 . . . . . . . . . . . . . . . . . . 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 12401 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (β—‘π‘β€˜π‘ƒ) ∈ π‘˜)
69 elelsuc 4410 . . . . . . . . . . . . . . . . . . . 20 ((β—‘π‘β€˜π‘ƒ) ∈ π‘˜ β†’ (β—‘π‘β€˜π‘ƒ) ∈ suc π‘˜)
7068, 69syl 14 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (β—‘π‘β€˜π‘ƒ) ∈ suc π‘˜)
71 0zd 9265 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ 0 ∈ β„€)
7271, 5, 66, 17frec2uzltd 10403 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ ((β—‘π‘β€˜π‘ƒ) ∈ suc π‘˜ β†’ (π‘β€˜(β—‘π‘β€˜π‘ƒ)) < (π‘β€˜suc π‘˜)))
7370, 72mpd 13 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (π‘β€˜(β—‘π‘β€˜π‘ƒ)) < (π‘β€˜suc π‘˜))
7465, 73eqbrtrrd 4028 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ 𝑃 < (π‘β€˜suc π‘˜))
7562, 63, 74ltled 8076 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ 𝑃 ≀ (π‘β€˜suc π‘˜))
7636, 37, 38, 50, 5, 51, 52, 57, 61, 75ennnfoneleminc 12412 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (π»β€˜π‘ƒ) βŠ† (π»β€˜(π‘β€˜suc π‘˜)))
7776ad2antrr 488 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ 𝑠 ∈ dom (π»β€˜π‘ƒ)) β†’ (π»β€˜π‘ƒ) βŠ† (π»β€˜(π‘β€˜suc π‘˜)))
78 simpr 110 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ 𝑠 ∈ dom (π»β€˜π‘ƒ)) β†’ 𝑠 ∈ dom (π»β€˜π‘ƒ))
79 funssfv 5542 . . . . . . . . . . . . . 14 ((Fun (π»β€˜(π‘β€˜suc π‘˜)) ∧ (π»β€˜π‘ƒ) βŠ† (π»β€˜(π‘β€˜suc π‘˜)) ∧ 𝑠 ∈ dom (π»β€˜π‘ƒ)) β†’ ((π»β€˜(π‘β€˜suc π‘˜))β€˜π‘ ) = ((π»β€˜π‘ƒ)β€˜π‘ ))
8056, 77, 78, 79syl3anc 1238 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ 𝑠 ∈ dom (π»β€˜π‘ƒ)) β†’ ((π»β€˜(π‘β€˜suc π‘˜))β€˜π‘ ) = ((π»β€˜π‘ƒ)β€˜π‘ ))
8180eqcomd 2183 . . . . . . . . . . . 12 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ 𝑠 ∈ dom (π»β€˜π‘ƒ)) β†’ ((π»β€˜π‘ƒ)β€˜π‘ ) = ((π»β€˜(π‘β€˜suc π‘˜))β€˜π‘ ))
8281ralrimiva 2550 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ βˆ€π‘  ∈ dom (π»β€˜π‘ƒ)((π»β€˜π‘ƒ)β€˜π‘ ) = ((π»β€˜(π‘β€˜suc π‘˜))β€˜π‘ ))
8336, 37, 49, 50, 5, 51, 52, 57ennnfonelemhf1o 12414 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (π»β€˜π‘ƒ):dom (π»β€˜π‘ƒ)–1-1-ontoβ†’(𝐹 β€œ (β—‘π‘β€˜π‘ƒ)))
84 f1ofun 5464 . . . . . . . . . . . . . 14 ((π»β€˜π‘ƒ):dom (π»β€˜π‘ƒ)–1-1-ontoβ†’(𝐹 β€œ (β—‘π‘β€˜π‘ƒ)) β†’ Fun (π»β€˜π‘ƒ))
8583, 84syl 14 . . . . . . . . . . . . 13 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ Fun (π»β€˜π‘ƒ))
86 eqfunfv 5619 . . . . . . . . . . . . 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 944 . . . . . . . . . 10 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ (π»β€˜π‘ƒ) = (π»β€˜(π‘β€˜suc π‘˜)))
9089rneqd 4857 . . . . . . . . 9 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ ran (π»β€˜π‘ƒ) = ran (π»β€˜(π‘β€˜suc π‘˜)))
91 dff1o5 5471 . . . . . . . . . . . 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 5778 . . . . . . . . . . . . . . . 16 ((𝑁:ω–1-1-ontoβ†’β„•0 ∧ suc π‘˜ ∈ Ο‰) β†’ (β—‘π‘β€˜(π‘β€˜suc π‘˜)) = suc π‘˜)
966, 17, 95sylancr 414 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (β—‘π‘β€˜(π‘β€˜suc π‘˜)) = suc π‘˜)
9796imaeq2d 4971 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (𝐹 β€œ (β—‘π‘β€˜(π‘β€˜suc π‘˜))) = (𝐹 β€œ suc π‘˜))
98 f1oeq3 5452 . . . . . . . . . . . . . 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 5471 . . . . . . . . . . . 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 2218 . . . . . . . 8 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ (𝐹 β€œ (β—‘π‘β€˜π‘ƒ)) = (𝐹 β€œ suc π‘˜))
10633, 105eleqtrrd 2257 . . . . . . 7 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ (πΉβ€˜π‘˜) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘ƒ)))
107 fvelima 5568 . . . . . . 7 ((Fun 𝐹 ∧ (πΉβ€˜π‘˜) ∈ (𝐹 β€œ (β—‘π‘β€˜π‘ƒ))) β†’ βˆƒπ‘ž ∈ (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))
10822, 106, 107syl2anc 411 . . . . . 6 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ βˆƒπ‘ž ∈ (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))
109 simprr 531 . . . . . . 7 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ (π‘ž ∈ (β—‘π‘β€˜π‘ƒ) ∧ (πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))) β†’ (πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))
110 fveq2 5516 . . . . . . . . . 10 (𝑗 = π‘ž β†’ (πΉβ€˜π‘—) = (πΉβ€˜π‘ž))
111110neeq2d 2366 . . . . . . . . 9 (𝑗 = π‘ž β†’ ((πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ (πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘ž)))
11267ad2antrr 488 . . . . . . . . 9 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ (π‘ž ∈ (β—‘π‘β€˜π‘ƒ) ∧ (πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))) β†’ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))
113 elelsuc 4410 . . . . . . . . . 10 (π‘ž ∈ (β—‘π‘β€˜π‘ƒ) β†’ π‘ž ∈ suc (β—‘π‘β€˜π‘ƒ))
114113ad2antrl 490 . . . . . . . . 9 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ (π‘ž ∈ (β—‘π‘β€˜π‘ƒ) ∧ (πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))) β†’ π‘ž ∈ suc (β—‘π‘β€˜π‘ƒ))
115111, 112, 114rspcdva 2847 . . . . . . . 8 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ (π‘ž ∈ (β—‘π‘β€˜π‘ƒ) ∧ (πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))) β†’ (πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘ž))
116115necomd 2433 . . . . . . 7 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ (π‘ž ∈ (β—‘π‘β€˜π‘ƒ) ∧ (πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))) β†’ (πΉβ€˜π‘ž) β‰  (πΉβ€˜π‘˜))
117109, 116pm2.21ddne 2430 . . . . . 6 ((((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) ∧ (π‘ž ∈ (β—‘π‘β€˜π‘ƒ) ∧ (πΉβ€˜π‘ž) = (πΉβ€˜π‘˜))) β†’ βŠ₯)
118108, 117rexlimddv 2599 . . . . 5 (((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) ∧ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ βŠ₯)
119118inegd 1372 . . . 4 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ Β¬ dom (π»β€˜π‘ƒ) = dom (π»β€˜(π‘β€˜suc π‘˜)))
120 dmss 4827 . . . . . 6 ((π»β€˜π‘ƒ) βŠ† (π»β€˜(π‘β€˜suc π‘˜)) β†’ dom (π»β€˜π‘ƒ) βŠ† dom (π»β€˜(π‘β€˜suc π‘˜)))
12176, 120syl 14 . . . . 5 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ dom (π»β€˜π‘ƒ) βŠ† dom (π»β€˜(π‘β€˜suc π‘˜)))
12235, 19, 4, 50, 5, 51, 52, 11ennnfonelemom 12409 . . . . . . 7 (πœ‘ β†’ dom (π»β€˜π‘ƒ) ∈ Ο‰)
123122adantr 276 . . . . . 6 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ dom (π»β€˜π‘ƒ) ∈ Ο‰)
12442a1i 9 . . . . . . . . 9 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž)))
125124ralbidv 2477 . . . . . . . 8 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ (βˆ€π‘› ∈ Ο‰ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘— ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—) ↔ βˆ€π‘› ∈ Ο‰ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž)))
12638, 125mpbid 147 . . . . . . 7 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ βˆ€π‘› ∈ Ο‰ βˆƒπ‘˜ ∈ Ο‰ βˆ€π‘Ž ∈ suc 𝑛(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘Ž))
12736, 37, 126, 50, 5, 51, 52, 61ennnfonelemom 12409 . . . . . 6 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ dom (π»β€˜(π‘β€˜suc π‘˜)) ∈ Ο‰)
128 nntri1 6497 . . . . . 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 6494 . . . . 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 1350 . . 3 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ dom (π»β€˜π‘ƒ) ∈ dom (π»β€˜(π‘β€˜suc π‘˜)))
134 fveq2 5516 . . . . . 6 (𝑖 = (π‘β€˜suc π‘˜) β†’ (π»β€˜π‘–) = (π»β€˜(π‘β€˜suc π‘˜)))
135134dmeqd 4830 . . . . 5 (𝑖 = (π‘β€˜suc π‘˜) β†’ dom (π»β€˜π‘–) = dom (π»β€˜(π‘β€˜suc π‘˜)))
136135eleq2d 2247 . . . 4 (𝑖 = (π‘β€˜suc π‘˜) β†’ (dom (π»β€˜π‘ƒ) ∈ dom (π»β€˜π‘–) ↔ dom (π»β€˜π‘ƒ) ∈ dom (π»β€˜(π‘β€˜suc π‘˜))))
137136rspcev 2842 . . 3 (((π‘β€˜suc π‘˜) ∈ β„•0 ∧ dom (π»β€˜π‘ƒ) ∈ dom (π»β€˜(π‘β€˜suc π‘˜))) β†’ βˆƒπ‘– ∈ β„•0 dom (π»β€˜π‘ƒ) ∈ dom (π»β€˜π‘–))
13818, 133, 137syl2anc 411 . 2 ((πœ‘ ∧ (π‘˜ ∈ Ο‰ ∧ βˆ€π‘— ∈ suc (β—‘π‘β€˜π‘ƒ)(πΉβ€˜π‘˜) β‰  (πΉβ€˜π‘—))) β†’ βˆƒπ‘– ∈ β„•0 dom (π»β€˜π‘ƒ) ∈ dom (π»β€˜π‘–))
13913, 138rexlimddv 2599 1 (πœ‘ β†’ βˆƒπ‘– ∈ β„•0 dom (π»β€˜π‘ƒ) ∈ dom (π»β€˜π‘–))
Colors of variables: wff set class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 104   ↔ wb 105  DECID wdc 834   ∨ w3o 977   = wceq 1353  βŠ₯wfal 1358   ∈ wcel 2148   β‰  wne 2347  βˆ€wral 2455  βˆƒwrex 2456   βˆͺ cun 3128   βŠ† wss 3130  βˆ…c0 3423  ifcif 3535  {csn 3593  βŸ¨cop 3596   class class class wbr 4004   ↦ cmpt 4065  suc csuc 4366  Ο‰com 4590  β—‘ccnv 4626  dom cdm 4627  ran crn 4628   β€œ cima 4630  Fun wfun 5211  βŸΆwf 5213  β€“1-1β†’wf1 5214  β€“ontoβ†’wfo 5215  β€“1-1-ontoβ†’wf1o 5216  β€˜cfv 5217  (class class class)co 5875   ∈ cmpo 5877  freccfrec 6391   ↑pm cpm 6649  0cc0 7811  1c1 7812   + caddc 7814   < clt 7992   βˆ’ cmin 8128  β„•0cn0 9176  β„€cz 9253  seqcseq 10445
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588  ax-cnex 7902  ax-resscn 7903  ax-1cn 7904  ax-1re 7905  ax-icn 7906  ax-addcl 7907  ax-addrcl 7908  ax-mulcl 7909  ax-addcom 7911  ax-addass 7913  ax-distr 7915  ax-i2m1 7916  ax-0lt1 7917  ax-0id 7919  ax-rnegex 7920  ax-cnre 7922  ax-pre-ltirr 7923  ax-pre-ltwlin 7924  ax-pre-lttrn 7925  ax-pre-ltadd 7927
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-ilim 4370  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-riota 5831  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-recs 6306  df-frec 6392  df-pm 6651  df-pnf 7994  df-mnf 7995  df-xr 7996  df-ltxr 7997  df-le 7998  df-sub 8130  df-neg 8131  df-inn 8920  df-n0 9177  df-z 9254  df-uz 9529  df-seqfrec 10446
This theorem is referenced by:  ennnfonelemhom  12416
  Copyright terms: Public domain W3C validator