Proof of Theorem hash1to3
Step | Hyp | Ref
| Expression |
1 | | hashcl 13009 |
. . 3
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
2 | | nn01to3 11657 |
. . 3
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 1 ≤ (#‘𝑉) ∧ (#‘𝑉) ≤ 3) → ((#‘𝑉) = 1 ∨ (#‘𝑉) = 2 ∨ (#‘𝑉) = 3)) |
3 | 1, 2 | syl3an1 1351 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 1 ≤
(#‘𝑉) ∧
(#‘𝑉) ≤ 3) →
((#‘𝑉) = 1 ∨
(#‘𝑉) = 2 ∨
(#‘𝑉) =
3)) |
4 | | hash1snb 13068 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 1 ↔
∃𝑎 𝑉 = {𝑎})) |
5 | 4 | biimpa 500 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 1) → ∃𝑎 𝑉 = {𝑎}) |
6 | | 3mix1 1223 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑎} → (𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
7 | 6 | 2eximi 1753 |
. . . . . . . . . 10
⊢
(∃𝑏∃𝑐 𝑉 = {𝑎} → ∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
8 | 7 | 19.23bi 2049 |
. . . . . . . . 9
⊢
(∃𝑐 𝑉 = {𝑎} → ∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
9 | 8 | 19.23bi 2049 |
. . . . . . . 8
⊢ (𝑉 = {𝑎} → ∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
10 | 9 | eximi 1752 |
. . . . . . 7
⊢
(∃𝑎 𝑉 = {𝑎} → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
11 | 5, 10 | syl 17 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 1) → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
12 | 11 | expcom 450 |
. . . . 5
⊢
((#‘𝑉) = 1
→ (𝑉 ∈ Fin →
∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
13 | | hash2pr 13108 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏}) |
14 | | 3mix2 1224 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑎, 𝑏} → (𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
15 | 14 | eximi 1752 |
. . . . . . . . 9
⊢
(∃𝑐 𝑉 = {𝑎, 𝑏} → ∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
16 | 15 | 19.23bi 2049 |
. . . . . . . 8
⊢ (𝑉 = {𝑎, 𝑏} → ∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
17 | 16 | 2eximi 1753 |
. . . . . . 7
⊢
(∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏} → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
18 | 13, 17 | syl 17 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 2) → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
19 | 18 | expcom 450 |
. . . . 5
⊢
((#‘𝑉) = 2
→ (𝑉 ∈ Fin →
∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
20 | | hash3tr 13127 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐}) |
21 | | 3mix3 1225 |
. . . . . . . . 9
⊢ (𝑉 = {𝑎, 𝑏, 𝑐} → (𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
22 | 21 | eximi 1752 |
. . . . . . . 8
⊢
(∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐} → ∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
23 | 22 | 2eximi 1753 |
. . . . . . 7
⊢
(∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐} → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
24 | 20, 23 | syl 17 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ (#‘𝑉) = 3) → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
25 | 24 | expcom 450 |
. . . . 5
⊢
((#‘𝑉) = 3
→ (𝑉 ∈ Fin →
∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
26 | 12, 19, 25 | 3jaoi 1383 |
. . . 4
⊢
(((#‘𝑉) = 1
∨ (#‘𝑉) = 2 ∨
(#‘𝑉) = 3) →
(𝑉 ∈ Fin →
∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
27 | 26 | com12 32 |
. . 3
⊢ (𝑉 ∈ Fin →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 2 ∨
(#‘𝑉) = 3) →
∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
28 | 27 | 3ad2ant1 1075 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 1 ≤
(#‘𝑉) ∧
(#‘𝑉) ≤ 3) →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 2 ∨
(#‘𝑉) = 3) →
∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
29 | 3, 28 | mpd 15 |
1
⊢ ((𝑉 ∈ Fin ∧ 1 ≤
(#‘𝑉) ∧
(#‘𝑉) ≤ 3) →
∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |