![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ihash | GIF version |
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.) |
Ref | Expression |
---|---|
df-ihash | ⊢ ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {〈ω, +∞〉}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥})) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chash 10298 | . 2 class ♯ | |
2 | vx | . . . . . 6 setvar 𝑥 | |
3 | cz 8848 | . . . . . 6 class ℤ | |
4 | 2 | cv 1295 | . . . . . . 7 class 𝑥 |
5 | c1 7448 | . . . . . . 7 class 1 | |
6 | caddc 7450 | . . . . . . 7 class + | |
7 | 4, 5, 6 | co 5690 | . . . . . 6 class (𝑥 + 1) |
8 | 2, 3, 7 | cmpt 3921 | . . . . 5 class (𝑥 ∈ ℤ ↦ (𝑥 + 1)) |
9 | cc0 7447 | . . . . 5 class 0 | |
10 | 8, 9 | cfrec 6193 | . . . 4 class frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
11 | com 4433 | . . . . . 6 class ω | |
12 | cpnf 7616 | . . . . . 6 class +∞ | |
13 | 11, 12 | cop 3469 | . . . . 5 class 〈ω, +∞〉 |
14 | 13 | csn 3466 | . . . 4 class {〈ω, +∞〉} |
15 | 10, 14 | cun 3011 | . . 3 class (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {〈ω, +∞〉}) |
16 | cvv 2633 | . . . 4 class V | |
17 | vy | . . . . . . . 8 setvar 𝑦 | |
18 | 17 | cv 1295 | . . . . . . 7 class 𝑦 |
19 | cdom 6536 | . . . . . . 7 class ≼ | |
20 | 18, 4, 19 | wbr 3867 | . . . . . 6 wff 𝑦 ≼ 𝑥 |
21 | 11 | csn 3466 | . . . . . . 7 class {ω} |
22 | 11, 21 | cun 3011 | . . . . . 6 class (ω ∪ {ω}) |
23 | 20, 17, 22 | crab 2374 | . . . . 5 class {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥} |
24 | 23 | cuni 3675 | . . . 4 class ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥} |
25 | 2, 16, 24 | cmpt 3921 | . . 3 class (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}) |
26 | 15, 25 | ccom 4471 | . 2 class ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {〈ω, +∞〉}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥})) |
27 | 1, 26 | wceq 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 |