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

Definition df-ihash 10299
 Description: Define the set size function ♯, which gives the cardinality of a finite set as a member of ℕ0, and assigns all infinite sets the value +∞. For example, (♯‘{0, 1, 2}) = 3. Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8156). We adopt the former notation from Corollary 8.2.4 of [AczelRathjen], p. 80 (although that work only defines it for finite sets). This definition (in terms of ∪ and ≼) is not taken directly from the literature, but for finite sets should be equivalent to the conventional definition that the size of a finite set is the unique natural number which is equinumerous to the given set. (Contributed by Jim Kingdon, 19-Feb-2022.)
Assertion
Ref Expression
df-ihash ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-ihash
StepHypRef Expression
1 chash 10298 . 2 class
2 vx . . . . . 6 setvar 𝑥
3 cz 8848 . . . . . 6 class
42cv 1295 . . . . . . 7 class 𝑥
5 c1 7448 . . . . . . 7 class 1
6 caddc 7450 . . . . . . 7 class +
74, 5, 6co 5690 . . . . . 6 class (𝑥 + 1)
82, 3, 7cmpt 3921 . . . . 5 class (𝑥 ∈ ℤ ↦ (𝑥 + 1))
9 cc0 7447 . . . . 5 class 0
108, 9cfrec 6193 . . . 4 class frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
11 com 4433 . . . . . 6 class ω
12 cpnf 7616 . . . . . 6 class +∞
1311, 12cop 3469 . . . . 5 class ⟨ω, +∞⟩
1413csn 3466 . . . 4 class {⟨ω, +∞⟩}
1510, 14cun 3011 . . 3 class (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})
16 cvv 2633 . . . 4 class V
17 vy . . . . . . . 8 setvar 𝑦
1817cv 1295 . . . . . . 7 class 𝑦
19 cdom 6536 . . . . . . 7 class
2018, 4, 19wbr 3867 . . . . . 6 wff 𝑦𝑥
2111csn 3466 . . . . . . 7 class {ω}
2211, 21cun 3011 . . . . . 6 class (ω ∪ {ω})
2320, 17, 22crab 2374 . . . . 5 class {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}
2423cuni 3675 . . . 4 class {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}
252, 16, 24cmpt 3921 . . 3 class (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})
2615, 25ccom 4471 . 2 class ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
271, 26wceq 1296 1 wff ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
 Colors of variables: wff set class This definition is referenced by:  hashinfom  10301  hashennn  10303
 Copyright terms: Public domain W3C validator