Definition df-ihash 10774

Description: Define the set size function ♯, which gives the cardinality of a finite set as a member of ℕ₀, 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 8557). 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

Step	Hyp	Ref	Expression
1		chash 10773	. 2 class ♯
2		vx	. . . . . 6 setvar 𝑥
3		cz 9271	. . . . . 6 class ℤ
4	2	cv 1363	. . . . . . 7 class 𝑥
5		c1 7830	. . . . . . 7 class 1
6		caddc 7832	. . . . . . 7 class +
7	4, 5, 6	co 5891	. . . . . 6 class (𝑥 + 1)
8	2, 3, 7	cmpt 4079	. . . . 5 class (𝑥 ∈ ℤ ↦ (𝑥 + 1))
9		cc0 7829	. . . . 5 class 0
10	8, 9	cfrec 6409	. . . 4 class frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
11		com 4604	. . . . . 6 class ω
12		cpnf 8007	. . . . . 6 class +∞
13	11, 12	cop 3610	. . . . 5 class ⟨ω, +∞⟩
14	13	csn 3607	. . . 4 class {⟨ω, +∞⟩}
15	10, 14	cun 3142	. . 3 class (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})
16		cvv 2752	. . . 4 class V
17		vy	. . . . . . . 8 setvar 𝑦
18	17	cv 1363	. . . . . . 7 class 𝑦
19		cdom 6757	. . . . . . 7 class ≼
20	18, 4, 19	wbr 4018	. . . . . 6 wff 𝑦 ≼ 𝑥
21	11	csn 3607	. . . . . . 7 class {ω}
22	11, 21	cun 3142	. . . . . 6 class (ω ∪ {ω})
23	20, 17, 22	crab 2472	. . . . 5 class {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
24	23	cuni 3824	. . . 4 class ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
25	2, 16, 24	cmpt 4079	. . 3 class (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥})
26	15, 25	ccom 4645	. 2 class ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))
27	1, 26	wceq 1364	1 wff ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))

This definition is referenced by:  hashinfom  10776  hashennn  10778