Definition df-ihash 11026

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.

Since we don't know that an arbitrary set is either finite or infinite (by inffiexmid 7089), the behavior beyond finite sets is not as useful as it might appear. For example, we wouldn't expect to be able to define this function in a meaningful way on 𝒫 1_o, which cannot be shown to be finite (per pw1fin 7093).

Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8750). 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 11025	. 2 class ♯
2		vx	. . . . . 6 setvar 𝑥
3		cz 9467	. . . . . 6 class ℤ
4	2	cv 1394	. . . . . . 7 class 𝑥
5		c1 8021	. . . . . . 7 class 1
6		caddc 8023	. . . . . . 7 class +
7	4, 5, 6	co 6011	. . . . . 6 class (𝑥 + 1)
8	2, 3, 7	cmpt 4146	. . . . 5 class (𝑥 ∈ ℤ ↦ (𝑥 + 1))
9		cc0 8020	. . . . 5 class 0
10	8, 9	cfrec 6549	. . . 4 class frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
11		com 4684	. . . . . 6 class ω
12		cpnf 8199	. . . . . 6 class +∞
13	11, 12	cop 3670	. . . . 5 class ⟨ω, +∞⟩
14	13	csn 3667	. . . 4 class {⟨ω, +∞⟩}
15	10, 14	cun 3196	. . 3 class (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})
16		cvv 2800	. . . 4 class V
17		vy	. . . . . . . 8 setvar 𝑦
18	17	cv 1394	. . . . . . 7 class 𝑦
19		cdom 6901	. . . . . . 7 class ≼
20	18, 4, 19	wbr 4084	. . . . . 6 wff 𝑦 ≼ 𝑥
21	11	csn 3667	. . . . . . 7 class {ω}
22	11, 21	cun 3196	. . . . . 6 class (ω ∪ {ω})
23	20, 17, 22	crab 2512	. . . . 5 class {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
24	23	cuni 3889	. . . 4 class ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}
25	2, 16, 24	cmpt 4146	. . 3 class (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥})
26	15, 25	ccom 4725	. 2 class ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))
27	1, 26	wceq 1395	1 wff ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))

This definition is referenced by:  hashinfom  11028  hashennn  11030