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

Theorem ctinfomlemom 11779
Description: Lemma for ctinfom 11780. Converting between ω and 0. (Contributed by Jim Kingdon, 10-Aug-2023.)
Hypotheses
Ref Expression
ctinfom.n 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
ctinfom.g 𝐺 = (𝐹𝑁)
ctinfom.f (𝜑𝐹:ω–onto𝐴)
ctinfom.inf (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹𝑛))
Assertion
Ref Expression
ctinfomlemom (𝜑 → (𝐺:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖)))
Distinct variable groups:   𝑖,𝐹,𝑥   𝑛,𝐹   𝑗,𝐺,𝑘   𝑖,𝑁,𝑗,𝑘   𝑛,𝑁,𝑘   𝑥,𝑁,𝑘   𝑖,𝑚,𝑗,𝑘   𝜑,𝑖,𝑘,𝑚,𝑥   𝑚,𝑛
Allowed substitution hints:   𝜑(𝑗,𝑛)   𝐴(𝑥,𝑖,𝑗,𝑘,𝑚,𝑛)   𝐹(𝑗,𝑘,𝑚)   𝐺(𝑥,𝑖,𝑚,𝑛)   𝑁(𝑚)

Proof of Theorem ctinfomlemom
StepHypRef Expression
1 ctinfom.f . . . 4 (𝜑𝐹:ω–onto𝐴)
2 ctinfom.n . . . . . . 7 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
32frechashgf1o 10088 . . . . . 6 𝑁:ω–1-1-onto→ℕ0
4 f1ocnv 5334 . . . . . 6 (𝑁:ω–1-1-onto→ℕ0𝑁:ℕ01-1-onto→ω)
53, 4ax-mp 7 . . . . 5 𝑁:ℕ01-1-onto→ω
6 f1ofo 5328 . . . . 5 (𝑁:ℕ01-1-onto→ω → 𝑁:ℕ0onto→ω)
75, 6ax-mp 7 . . . 4 𝑁:ℕ0onto→ω
8 foco 5311 . . . 4 ((𝐹:ω–onto𝐴𝑁:ℕ0onto→ω) → (𝐹𝑁):ℕ0onto𝐴)
91, 7, 8sylancl 407 . . 3 (𝜑 → (𝐹𝑁):ℕ0onto𝐴)
10 ctinfom.g . . . 4 𝐺 = (𝐹𝑁)
11 foeq1 5297 . . . 4 (𝐺 = (𝐹𝑁) → (𝐺:ℕ0onto𝐴 ↔ (𝐹𝑁):ℕ0onto𝐴))
1210, 11ax-mp 7 . . 3 (𝐺:ℕ0onto𝐴 ↔ (𝐹𝑁):ℕ0onto𝐴)
139, 12sylibr 133 . 2 (𝜑𝐺:ℕ0onto𝐴)
14 imaeq2 4833 . . . . . . . 8 (𝑛 = suc (𝑁𝑚) → (𝐹𝑛) = (𝐹 “ suc (𝑁𝑚)))
1514eleq2d 2182 . . . . . . 7 (𝑛 = suc (𝑁𝑚) → ((𝐹𝑘) ∈ (𝐹𝑛) ↔ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚))))
1615notbid 639 . . . . . 6 (𝑛 = suc (𝑁𝑚) → (¬ (𝐹𝑘) ∈ (𝐹𝑛) ↔ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚))))
1716rexbidv 2410 . . . . 5 (𝑛 = suc (𝑁𝑚) → (∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹𝑛) ↔ ∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚))))
18 ctinfom.inf . . . . . 6 (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹𝑛))
1918adantr 272 . . . . 5 ((𝜑𝑚 ∈ ℕ0) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹𝑛))
20 f1of 5321 . . . . . . . . 9 (𝑁:ℕ01-1-onto→ω → 𝑁:ℕ0⟶ω)
215, 20ax-mp 7 . . . . . . . 8 𝑁:ℕ0⟶ω
2221a1i 9 . . . . . . 7 ((𝜑𝑚 ∈ ℕ0) → 𝑁:ℕ0⟶ω)
23 simpr 109 . . . . . . 7 ((𝜑𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
2422, 23ffvelrnd 5508 . . . . . 6 ((𝜑𝑚 ∈ ℕ0) → (𝑁𝑚) ∈ ω)
25 peano2 4467 . . . . . 6 ((𝑁𝑚) ∈ ω → suc (𝑁𝑚) ∈ ω)
2624, 25syl 14 . . . . 5 ((𝜑𝑚 ∈ ℕ0) → suc (𝑁𝑚) ∈ ω)
2717, 19, 26rspcdva 2763 . . . 4 ((𝜑𝑚 ∈ ℕ0) → ∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))
28 f1of 5321 . . . . . . . 8 (𝑁:ω–1-1-onto→ℕ0𝑁:ω⟶ℕ0)
293, 28ax-mp 7 . . . . . . 7 𝑁:ω⟶ℕ0
3029a1i 9 . . . . . 6 (((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) → 𝑁:ω⟶ℕ0)
31 simprl 503 . . . . . 6 (((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) → 𝑘 ∈ ω)
3230, 31ffvelrnd 5508 . . . . 5 (((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) → (𝑁𝑘) ∈ ℕ0)
3310fveq1i 5374 . . . . . . . . . . 11 (𝐺‘(𝑁𝑘)) = ((𝐹𝑁)‘(𝑁𝑘))
3432adantr 272 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁𝑘) ∈ ℕ0)
35 fvco3 5444 . . . . . . . . . . . 12 ((𝑁:ℕ0⟶ω ∧ (𝑁𝑘) ∈ ℕ0) → ((𝐹𝑁)‘(𝑁𝑘)) = (𝐹‘(𝑁‘(𝑁𝑘))))
3621, 34, 35sylancr 408 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐹𝑁)‘(𝑁𝑘)) = (𝐹‘(𝑁‘(𝑁𝑘))))
3733, 36syl5eq 2157 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝐺‘(𝑁𝑘)) = (𝐹‘(𝑁‘(𝑁𝑘))))
3831adantr 272 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 𝑘 ∈ ω)
39 f1ocnvfv1 5630 . . . . . . . . . . . . 13 ((𝑁:ω–1-1-onto→ℕ0𝑘 ∈ ω) → (𝑁‘(𝑁𝑘)) = 𝑘)
403, 39mpan 418 . . . . . . . . . . . 12 (𝑘 ∈ ω → (𝑁‘(𝑁𝑘)) = 𝑘)
4140fveq2d 5377 . . . . . . . . . . 11 (𝑘 ∈ ω → (𝐹‘(𝑁‘(𝑁𝑘))) = (𝐹𝑘))
4238, 41syl 14 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝐹‘(𝑁‘(𝑁𝑘))) = (𝐹𝑘))
4337, 42eqtrd 2145 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝐺‘(𝑁𝑘)) = (𝐹𝑘))
44 simplrr 508 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))
4543, 44eqneltrd 2208 . . . . . . . 8 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ¬ (𝐺‘(𝑁𝑘)) ∈ (𝐹 “ suc (𝑁𝑚)))
46 simpr 109 . . . . . . . . 9 (((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) ∧ (𝐺‘(𝑁𝑘)) = (𝐺𝑖)) → (𝐺‘(𝑁𝑘)) = (𝐺𝑖))
4710fveq1i 5374 . . . . . . . . . . . 12 (𝐺𝑖) = ((𝐹𝑁)‘𝑖)
48 elfznn0 9781 . . . . . . . . . . . . . 14 (𝑖 ∈ (0...𝑚) → 𝑖 ∈ ℕ0)
4948adantl 273 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖 ∈ ℕ0)
50 fvco3 5444 . . . . . . . . . . . . 13 ((𝑁:ℕ0⟶ω ∧ 𝑖 ∈ ℕ0) → ((𝐹𝑁)‘𝑖) = (𝐹‘(𝑁𝑖)))
5121, 49, 50sylancr 408 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐹𝑁)‘𝑖) = (𝐹‘(𝑁𝑖)))
5247, 51syl5eq 2157 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝐺𝑖) = (𝐹‘(𝑁𝑖)))
53 elfzle2 9695 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0...𝑚) → 𝑖𝑚)
5453adantl 273 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖𝑚)
55 0zd 8964 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 0 ∈ ℤ)
5621a1i 9 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 𝑁:ℕ0⟶ω)
5756, 49ffvelrnd 5508 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁𝑖) ∈ ω)
5824ad2antrr 477 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁𝑚) ∈ ω)
5955, 2, 57, 58frec2uzled 10089 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ((𝑁𝑖) ⊆ (𝑁𝑚) ↔ (𝑁‘(𝑁𝑖)) ≤ (𝑁‘(𝑁𝑚))))
60 f1ocnvfv2 5631 . . . . . . . . . . . . . . . . 17 ((𝑁:ω–1-1-onto→ℕ0𝑖 ∈ ℕ0) → (𝑁‘(𝑁𝑖)) = 𝑖)
613, 49, 60sylancr 408 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁‘(𝑁𝑖)) = 𝑖)
6223ad2antrr 477 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 𝑚 ∈ ℕ0)
63 f1ocnvfv2 5631 . . . . . . . . . . . . . . . . 17 ((𝑁:ω–1-1-onto→ℕ0𝑚 ∈ ℕ0) → (𝑁‘(𝑁𝑚)) = 𝑚)
643, 62, 63sylancr 408 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁‘(𝑁𝑚)) = 𝑚)
6561, 64breq12d 3906 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ((𝑁‘(𝑁𝑖)) ≤ (𝑁‘(𝑁𝑚)) ↔ 𝑖𝑚))
6659, 65bitrd 187 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ((𝑁𝑖) ⊆ (𝑁𝑚) ↔ 𝑖𝑚))
6754, 66mpbird 166 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁𝑖) ⊆ (𝑁𝑚))
68 nnsssuc 6350 . . . . . . . . . . . . . 14 (((𝑁𝑖) ∈ ω ∧ (𝑁𝑚) ∈ ω) → ((𝑁𝑖) ⊆ (𝑁𝑚) ↔ (𝑁𝑖) ∈ suc (𝑁𝑚)))
6957, 58, 68syl2anc 406 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ((𝑁𝑖) ⊆ (𝑁𝑚) ↔ (𝑁𝑖) ∈ suc (𝑁𝑚)))
7067, 69mpbid 146 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁𝑖) ∈ suc (𝑁𝑚))
711ad3antrrr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 𝐹:ω–onto𝐴)
72 fof 5301 . . . . . . . . . . . . . . 15 (𝐹:ω–onto𝐴𝐹:ω⟶𝐴)
7371, 72syl 14 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → 𝐹:ω⟶𝐴)
7473ffund 5232 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → Fun 𝐹)
7573fdmd 5235 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → dom 𝐹 = ω)
7657, 75eleqtrrd 2192 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝑁𝑖) ∈ dom 𝐹)
77 funfvima 5601 . . . . . . . . . . . . 13 ((Fun 𝐹 ∧ (𝑁𝑖) ∈ dom 𝐹) → ((𝑁𝑖) ∈ suc (𝑁𝑚) → (𝐹‘(𝑁𝑖)) ∈ (𝐹 “ suc (𝑁𝑚))))
7874, 76, 77syl2anc 406 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ((𝑁𝑖) ∈ suc (𝑁𝑚) → (𝐹‘(𝑁𝑖)) ∈ (𝐹 “ suc (𝑁𝑚))))
7970, 78mpd 13 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝐹‘(𝑁𝑖)) ∈ (𝐹 “ suc (𝑁𝑚)))
8052, 79eqeltrd 2189 . . . . . . . . . 10 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝐺𝑖) ∈ (𝐹 “ suc (𝑁𝑚)))
8180adantr 272 . . . . . . . . 9 (((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) ∧ (𝐺‘(𝑁𝑘)) = (𝐺𝑖)) → (𝐺𝑖) ∈ (𝐹 “ suc (𝑁𝑚)))
8246, 81eqeltrd 2189 . . . . . . . 8 (((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) ∧ (𝐺‘(𝑁𝑘)) = (𝐺𝑖)) → (𝐺‘(𝑁𝑘)) ∈ (𝐹 “ suc (𝑁𝑚)))
8345, 82mtand 637 . . . . . . 7 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → ¬ (𝐺‘(𝑁𝑘)) = (𝐺𝑖))
8483neqned 2287 . . . . . 6 ((((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) ∧ 𝑖 ∈ (0...𝑚)) → (𝐺‘(𝑁𝑘)) ≠ (𝐺𝑖))
8584ralrimiva 2477 . . . . 5 (((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) → ∀𝑖 ∈ (0...𝑚)(𝐺‘(𝑁𝑘)) ≠ (𝐺𝑖))
86 fveq2 5373 . . . . . . . 8 (𝑗 = (𝑁𝑘) → (𝐺𝑗) = (𝐺‘(𝑁𝑘)))
8786neeq1d 2298 . . . . . . 7 (𝑗 = (𝑁𝑘) → ((𝐺𝑗) ≠ (𝐺𝑖) ↔ (𝐺‘(𝑁𝑘)) ≠ (𝐺𝑖)))
8887ralbidv 2409 . . . . . 6 (𝑗 = (𝑁𝑘) → (∀𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖) ↔ ∀𝑖 ∈ (0...𝑚)(𝐺‘(𝑁𝑘)) ≠ (𝐺𝑖)))
8988rspcev 2758 . . . . 5 (((𝑁𝑘) ∈ ℕ0 ∧ ∀𝑖 ∈ (0...𝑚)(𝐺‘(𝑁𝑘)) ≠ (𝐺𝑖)) → ∃𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖))
9032, 85, 89syl2anc 406 . . . 4 (((𝜑𝑚 ∈ ℕ0) ∧ (𝑘 ∈ ω ∧ ¬ (𝐹𝑘) ∈ (𝐹 “ suc (𝑁𝑚)))) → ∃𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖))
9127, 90rexlimddv 2526 . . 3 ((𝜑𝑚 ∈ ℕ0) → ∃𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖))
9291ralrimiva 2477 . 2 (𝜑 → ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖))
9313, 92jca 302 1 (𝜑 → (𝐺:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104   = wceq 1312  wcel 1461  wne 2280  wral 2388  wrex 2389  wss 3035   class class class wbr 3893  cmpt 3947  suc csuc 4245  ωcom 4462  ccnv 4496  dom cdm 4497  cima 4500  ccom 4501  Fun wfun 5073  wf 5075  ontowfo 5077  1-1-ontowf1o 5078  cfv 5079  (class class class)co 5726  freccfrec 6239  0cc0 7541  1c1 7542   + caddc 7544  cle 7719  0cn0 8875  cz 8952  ...cfz 9677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-addcom 7639  ax-addass 7641  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-0id 7647  ax-rnegex 7648  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-ltadd 7655
This theorem depends on definitions:  df-bi 116  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-iord 4246  df-on 4248  df-ilim 4249  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-recs 6154  df-frec 6240  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-inn 8625  df-n0 8876  df-z 8953  df-uz 9223  df-fz 9678
This theorem is referenced by:  ctinfom  11780
  Copyright terms: Public domain W3C validator