Proof of Theorem hash1to3
Step | Hyp | Ref
| Expression |
1 | | hashcl 14069 |
. . 3
⊢ (𝑉 ∈ Fin →
(♯‘𝑉) ∈
ℕ0) |
2 | | nn01to3 12680 |
. . 3
⊢
(((♯‘𝑉)
∈ ℕ0 ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3) → ((♯‘𝑉) = 1 ∨ (♯‘𝑉) = 2 ∨ (♯‘𝑉) = 3)) |
3 | 1, 2 | syl3an1 1162 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 1 ≤
(♯‘𝑉) ∧
(♯‘𝑉) ≤ 3)
→ ((♯‘𝑉) =
1 ∨ (♯‘𝑉) =
2 ∨ (♯‘𝑉) =
3)) |
4 | | hash1snb 14132 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin →
((♯‘𝑉) = 1
↔ ∃𝑎 𝑉 = {𝑎})) |
5 | 4 | biimpa 477 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 1)
→ ∃𝑎 𝑉 = {𝑎}) |
6 | | 3mix1 1329 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑎} → (𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
7 | 6 | 2eximi 1842 |
. . . . . . . . . 10
⊢
(∃𝑏∃𝑐 𝑉 = {𝑎} → ∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
8 | 7 | 19.23bi 2188 |
. . . . . . . . 9
⊢
(∃𝑐 𝑉 = {𝑎} → ∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
9 | 8 | 19.23bi 2188 |
. . . . . . . 8
⊢ (𝑉 = {𝑎} → ∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
10 | 9 | eximi 1841 |
. . . . . . 7
⊢
(∃𝑎 𝑉 = {𝑎} → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
11 | 5, 10 | syl 17 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 1)
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
12 | 11 | expcom 414 |
. . . . 5
⊢
((♯‘𝑉) =
1 → (𝑉 ∈ Fin
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
13 | | hash2pr 14181 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ ∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏}) |
14 | | 3mix2 1330 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑎, 𝑏} → (𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
15 | 14 | eximi 1841 |
. . . . . . . . 9
⊢
(∃𝑐 𝑉 = {𝑎, 𝑏} → ∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
16 | 15 | 19.23bi 2188 |
. . . . . . . 8
⊢ (𝑉 = {𝑎, 𝑏} → ∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
17 | 16 | 2eximi 1842 |
. . . . . . 7
⊢
(∃𝑎∃𝑏 𝑉 = {𝑎, 𝑏} → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
18 | 13, 17 | syl 17 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 2)
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
19 | 18 | expcom 414 |
. . . . 5
⊢
((♯‘𝑉) =
2 → (𝑉 ∈ Fin
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
20 | | hash3tr 14202 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 3)
→ ∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐}) |
21 | | 3mix3 1331 |
. . . . . . . . 9
⊢ (𝑉 = {𝑎, 𝑏, 𝑐} → (𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
22 | 21 | eximi 1841 |
. . . . . . . 8
⊢
(∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐} → ∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
23 | 22 | 2eximi 1842 |
. . . . . . 7
⊢
(∃𝑎∃𝑏∃𝑐 𝑉 = {𝑎, 𝑏, 𝑐} → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
24 | 20, 23 | syl 17 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧
(♯‘𝑉) = 3)
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |
25 | 24 | expcom 414 |
. . . . 5
⊢
((♯‘𝑉) =
3 → (𝑉 ∈ Fin
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
26 | 12, 19, 25 | 3jaoi 1426 |
. . . 4
⊢
(((♯‘𝑉)
= 1 ∨ (♯‘𝑉)
= 2 ∨ (♯‘𝑉)
= 3) → (𝑉 ∈ Fin
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
27 | 26 | com12 32 |
. . 3
⊢ (𝑉 ∈ Fin →
(((♯‘𝑉) = 1
∨ (♯‘𝑉) = 2
∨ (♯‘𝑉) = 3)
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
28 | 27 | 3ad2ant1 1132 |
. 2
⊢ ((𝑉 ∈ Fin ∧ 1 ≤
(♯‘𝑉) ∧
(♯‘𝑉) ≤ 3)
→ (((♯‘𝑉)
= 1 ∨ (♯‘𝑉)
= 2 ∨ (♯‘𝑉)
= 3) → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}))) |
29 | 3, 28 | mpd 15 |
1
⊢ ((𝑉 ∈ Fin ∧ 1 ≤
(♯‘𝑉) ∧
(♯‘𝑉) ≤ 3)
→ ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) |