Definition df-ihash 10769

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 8552). 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 10768	. 2 class ♯
2		vx	. . . . . 6 setvar 𝑥
3		cz 9266	. . . . . 6 class ℤ
4	2	cv 1362	. . . . . . 7 class 𝑥
5		c1 7825	. . . . . . 7 class 1
6		caddc 7827	. . . . . . 7 class +
7	4, 5, 6	co 5888	. . . . . 6 class (𝑥 + 1)
8	2, 3, 7	cmpt 4076	. . . . 5 class (𝑥 ∈ ℤ ↦ (𝑥 + 1))
9		cc0 7824	. . . . 5 class 0
10	8, 9	cfrec 6404	. . . 4 class frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
11		com 4601	. . . . . 6 class ω
12		cpnf 8002	. . . . . 6 class +∞
13	11, 12	cop 3607	. . . . 5 class ⟨ω, +∞⟩
14	13	csn 3604	. . . 4 class {⟨ω, +∞⟩}
15	10, 14	cun 3139	. . 3 class (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})
16		cvv 2749	. . . 4 class V
17		vy	. . . . . . . 8 setvar 𝑦
18	17	cv 1362	. . . . . . 7 class 𝑦
19		cdom 6752	. . . . . . 7 class ≼
20	18, 4, 19	wbr 4015	. . . . . 6 wff 𝑦 ≼ 𝑥
21	11	csn 3604	. . . . . . 7 class {ω}
22	11, 21	cun 3139	. . . . . 6 class (ω ∪ {ω})
23	20, 17, 22	crab 2469	. . . . 5 class {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
24	23	cuni 3821	. . . 4 class ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
25	2, 16, 24	cmpt 4076	. . 3 class (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥})
26	15, 25	ccom 4642	. 2 class ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))
27	1, 26	wceq 1363	1 wff ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))

This definition is referenced by:  hashinfom  10771  hashennn  10773