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

Theorem ctinfom 12447
Description: A condition for a set being countably infinite. Restates ennnfone 12444 in terms of ω and function image. Like ennnfone 12444 the condition can be summarized as 𝐴 being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
Assertion
Ref Expression
ctinfom (𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
Distinct variable groups:   𝐴,𝑓,𝑛   𝑥,𝐴,𝑦   𝑓,𝑘,𝑛
Allowed substitution hint:   𝐴(𝑘)

Proof of Theorem ctinfom
Dummy variables 𝑎 𝑑 𝑖 𝑚 𝑔 𝑏 𝑐 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ennnfone 12444 . . . 4 (𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑔(𝑔:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖))))
21simplbi 274 . . 3 (𝐴 ≈ ℕ → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
3 nnenom 10452 . . . . . . 7 ℕ ≈ ω
4 entr 6802 . . . . . . 7 ((𝐴 ≈ ℕ ∧ ℕ ≈ ω) → 𝐴 ≈ ω)
53, 4mpan2 425 . . . . . 6 (𝐴 ≈ ℕ → 𝐴 ≈ ω)
65ensymd 6801 . . . . 5 (𝐴 ≈ ℕ → ω ≈ 𝐴)
7 bren 6765 . . . . 5 (ω ≈ 𝐴 ↔ ∃𝑓 𝑓:ω–1-1-onto𝐴)
86, 7sylib 122 . . . 4 (𝐴 ≈ ℕ → ∃𝑓 𝑓:ω–1-1-onto𝐴)
9 f1ofo 5483 . . . . . . . 8 (𝑓:ω–1-1-onto𝐴𝑓:ω–onto𝐴)
109adantl 277 . . . . . . 7 ((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) → 𝑓:ω–onto𝐴)
11 simpr 110 . . . . . . . . 9 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
12 nnord 4626 . . . . . . . . . . . 12 (𝑛 ∈ ω → Ord 𝑛)
1312adantl 277 . . . . . . . . . . 11 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → Ord 𝑛)
14 ordirr 4556 . . . . . . . . . . 11 (Ord 𝑛 → ¬ 𝑛𝑛)
1513, 14syl 14 . . . . . . . . . 10 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → ¬ 𝑛𝑛)
16 f1of1 5475 . . . . . . . . . . . 12 (𝑓:ω–1-1-onto𝐴𝑓:ω–1-1𝐴)
1716ad2antlr 489 . . . . . . . . . . 11 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → 𝑓:ω–1-1𝐴)
18 omelon 4623 . . . . . . . . . . . . 13 ω ∈ On
1918onelssi 4444 . . . . . . . . . . . 12 (𝑛 ∈ ω → 𝑛 ⊆ ω)
2019adantl 277 . . . . . . . . . . 11 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → 𝑛 ⊆ ω)
21 f1elima 5790 . . . . . . . . . . 11 ((𝑓:ω–1-1𝐴𝑛 ∈ ω ∧ 𝑛 ⊆ ω) → ((𝑓𝑛) ∈ (𝑓𝑛) ↔ 𝑛𝑛))
2217, 11, 20, 21syl3anc 1249 . . . . . . . . . 10 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → ((𝑓𝑛) ∈ (𝑓𝑛) ↔ 𝑛𝑛))
2315, 22mtbird 674 . . . . . . . . 9 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → ¬ (𝑓𝑛) ∈ (𝑓𝑛))
24 fveq2 5530 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝑓𝑘) = (𝑓𝑛))
2524eleq1d 2258 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((𝑓𝑘) ∈ (𝑓𝑛) ↔ (𝑓𝑛) ∈ (𝑓𝑛)))
2625notbid 668 . . . . . . . . . 10 (𝑘 = 𝑛 → (¬ (𝑓𝑘) ∈ (𝑓𝑛) ↔ ¬ (𝑓𝑛) ∈ (𝑓𝑛)))
2726rspcev 2856 . . . . . . . . 9 ((𝑛 ∈ ω ∧ ¬ (𝑓𝑛) ∈ (𝑓𝑛)) → ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))
2811, 23, 27syl2anc 411 . . . . . . . 8 (((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) ∧ 𝑛 ∈ ω) → ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))
2928ralrimiva 2563 . . . . . . 7 ((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))
3010, 29jca 306 . . . . . 6 ((𝐴 ≈ ℕ ∧ 𝑓:ω–1-1-onto𝐴) → (𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
3130ex 115 . . . . 5 (𝐴 ≈ ℕ → (𝑓:ω–1-1-onto𝐴 → (𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
3231eximdv 1891 . . . 4 (𝐴 ≈ ℕ → (∃𝑓 𝑓:ω–1-1-onto𝐴 → ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
338, 32mpd 13 . . 3 (𝐴 ≈ ℕ → ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
342, 33jca 306 . 2 (𝐴 ≈ ℕ → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
35 oveq1 5898 . . . . . . . . 9 (𝑏 = 𝑎 → (𝑏 + 1) = (𝑎 + 1))
3635cbvmptv 4114 . . . . . . . 8 (𝑏 ∈ ℤ ↦ (𝑏 + 1)) = (𝑎 ∈ ℤ ↦ (𝑎 + 1))
37 freceq1 6411 . . . . . . . 8 ((𝑏 ∈ ℤ ↦ (𝑏 + 1)) = (𝑎 ∈ ℤ ↦ (𝑎 + 1)) → frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0) = frec((𝑎 ∈ ℤ ↦ (𝑎 + 1)), 0))
3836, 37ax-mp 5 . . . . . . 7 frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0) = frec((𝑎 ∈ ℤ ↦ (𝑎 + 1)), 0)
39 eqid 2189 . . . . . . 7 (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))
40 simpl 109 . . . . . . 7 ((𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → 𝑓:ω–onto𝐴)
41 fveq2 5530 . . . . . . . . . . . . 13 (𝑘 = 𝑑 → (𝑓𝑘) = (𝑓𝑑))
4241eleq1d 2258 . . . . . . . . . . . 12 (𝑘 = 𝑑 → ((𝑓𝑘) ∈ (𝑓𝑛) ↔ (𝑓𝑑) ∈ (𝑓𝑛)))
4342notbid 668 . . . . . . . . . . 11 (𝑘 = 𝑑 → (¬ (𝑓𝑘) ∈ (𝑓𝑛) ↔ ¬ (𝑓𝑑) ∈ (𝑓𝑛)))
4443cbvrexv 2719 . . . . . . . . . 10 (∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛) ↔ ∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑛))
4544ralbii 2496 . . . . . . . . 9 (∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛) ↔ ∀𝑛 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑛))
46 imaeq2 4981 . . . . . . . . . . . . 13 (𝑛 = 𝑐 → (𝑓𝑛) = (𝑓𝑐))
4746eleq2d 2259 . . . . . . . . . . . 12 (𝑛 = 𝑐 → ((𝑓𝑑) ∈ (𝑓𝑛) ↔ (𝑓𝑑) ∈ (𝑓𝑐)))
4847notbid 668 . . . . . . . . . . 11 (𝑛 = 𝑐 → (¬ (𝑓𝑑) ∈ (𝑓𝑛) ↔ ¬ (𝑓𝑑) ∈ (𝑓𝑐)))
4948rexbidv 2491 . . . . . . . . . 10 (𝑛 = 𝑐 → (∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑛) ↔ ∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑐)))
5049cbvralv 2718 . . . . . . . . 9 (∀𝑛 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑛) ↔ ∀𝑐 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑐))
5145, 50sylbb 123 . . . . . . . 8 (∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛) → ∀𝑐 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑐))
5251adantl 277 . . . . . . 7 ((𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → ∀𝑐 ∈ ω ∃𝑑 ∈ ω ¬ (𝑓𝑑) ∈ (𝑓𝑐))
5338, 39, 40, 52ctinfomlemom 12446 . . . . . 6 ((𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)))
54 vex 2755 . . . . . . . 8 𝑓 ∈ V
55 frecex 6413 . . . . . . . . 9 frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0) ∈ V
5655cnvex 5182 . . . . . . . 8 frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0) ∈ V
5754, 56coex 5189 . . . . . . 7 (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) ∈ V
58 foeq1 5449 . . . . . . . 8 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (𝑔:ℕ0onto𝐴 ↔ (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0onto𝐴))
59 fveq1 5529 . . . . . . . . . . . 12 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (𝑔𝑗) = ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗))
60 fveq1 5529 . . . . . . . . . . . 12 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (𝑔𝑖) = ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖))
6159, 60neeq12d 2380 . . . . . . . . . . 11 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → ((𝑔𝑗) ≠ (𝑔𝑖) ↔ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)))
6261ralbidv 2490 . . . . . . . . . 10 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (∀𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖) ↔ ∀𝑖 ∈ (0...𝑚)((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)))
6362rexbidv 2491 . . . . . . . . 9 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (∃𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖) ↔ ∃𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)))
6463ralbidv 2490 . . . . . . . 8 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → (∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖) ↔ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)))
6558, 64anbi12d 473 . . . . . . 7 (𝑔 = (𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)) → ((𝑔:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖)) ↔ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖))))
6657, 65spcev 2847 . . . . . 6 (((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0)):ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑗) ≠ ((𝑓frec((𝑏 ∈ ℤ ↦ (𝑏 + 1)), 0))‘𝑖)) → ∃𝑔(𝑔:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖)))
6753, 66syl 14 . . . . 5 ((𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → ∃𝑔(𝑔:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖)))
6867exlimiv 1609 . . . 4 (∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → ∃𝑔(𝑔:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖)))
6968anim2i 342 . . 3 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑔(𝑔:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝑔𝑗) ≠ (𝑔𝑖))))
7069, 1sylibr 134 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))) → 𝐴 ≈ ℕ)
7134, 70impbii 126 1 (𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 104  wb 105  DECID wdc 835   = wceq 1364  wex 1503  wcel 2160  wne 2360  wral 2468  wrex 2469  wss 3144   class class class wbr 4018  cmpt 4079  Ord word 4377  ωcom 4604  ccnv 4640  cima 4644  ccom 4645  1-1wf1 5228  ontowfo 5229  1-1-ontowf1o 5230  cfv 5231  (class class class)co 5891  freccfrec 6409  cen 6756  0cc0 7829  1c1 7830   + caddc 7832  cn 8937  0cn0 9194  cz 9271  ...cfz 10026
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 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602  ax-cnex 7920  ax-resscn 7921  ax-1cn 7922  ax-1re 7923  ax-icn 7924  ax-addcl 7925  ax-addrcl 7926  ax-mulcl 7927  ax-addcom 7929  ax-addass 7931  ax-distr 7933  ax-i2m1 7934  ax-0lt1 7935  ax-0id 7937  ax-rnegex 7938  ax-cnre 7940  ax-pre-ltirr 7941  ax-pre-ltwlin 7942  ax-pre-lttrn 7943  ax-pre-ltadd 7945
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 4308  df-iord 4381  df-on 4383  df-ilim 4384  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-riota 5847  df-ov 5894  df-oprab 5895  df-mpo 5896  df-1st 6159  df-2nd 6160  df-recs 6324  df-frec 6410  df-er 6553  df-pm 6669  df-en 6759  df-pnf 8012  df-mnf 8013  df-xr 8014  df-ltxr 8015  df-le 8016  df-sub 8148  df-neg 8149  df-inn 8938  df-n0 9195  df-z 9272  df-uz 9547  df-fz 10027  df-seqfrec 10464
This theorem is referenced by:  ctinf  12449
  Copyright terms: Public domain W3C validator