Definition df-ihash 10515

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 8337). 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 10514	. 2 class ♯
2		vx	. . . . . 6 setvar 𝑥
3		cz 9047	. . . . . 6 class ℤ
4	2	cv 1330	. . . . . . 7 class 𝑥
5		c1 7614	. . . . . . 7 class 1
6		caddc 7616	. . . . . . 7 class +
7	4, 5, 6	co 5767	. . . . . 6 class (𝑥 + 1)
8	2, 3, 7	cmpt 3984	. . . . 5 class (𝑥 ∈ ℤ ↦ (𝑥 + 1))
9		cc0 7613	. . . . 5 class 0
10	8, 9	cfrec 6280	. . . 4 class frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
11		com 4499	. . . . . 6 class ω
12		cpnf 7790	. . . . . 6 class +∞
13	11, 12	cop 3525	. . . . 5 class ⟨ω, +∞⟩
14	13	csn 3522	. . . 4 class {⟨ω, +∞⟩}
15	10, 14	cun 3064	. . 3 class (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})
16		cvv 2681	. . . 4 class V
17		vy	. . . . . . . 8 setvar 𝑦
18	17	cv 1330	. . . . . . 7 class 𝑦
19		cdom 6626	. . . . . . 7 class ≼
20	18, 4, 19	wbr 3924	. . . . . 6 wff 𝑦 ≼ 𝑥
21	11	csn 3522	. . . . . . 7 class {ω}
22	11, 21	cun 3064	. . . . . 6 class (ω ∪ {ω})
23	20, 17, 22	crab 2418	. . . . 5 class {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
24	23	cuni 3731	. . . 4 class ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
25	2, 16, 24	cmpt 3984	. . 3 class (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥})
26	15, 25	ccom 4538	. 2 class ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))
27	1, 26	wceq 1331	1 wff ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))

This definition is referenced by:  hashinfom  10517  hashennn  10519