Metamath Proof Explorer

Theorem hash1to3

Description: If the size of a set is between 1 and 3 (inclusively), the set is a singleton or an unordered pair or an unordered triple. (Contributed by Alexander van der Vekens, 13-Sep-2018)

Ref Expression
Assertion hash1to3 ⊢ V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c

Proof

Step Hyp Ref Expression
1 hashcl ⊢ V ∈ Fin → V ∈ ℕ 0
2 nn01to3 ⊢ V ∈ ℕ 0 ∧ 1 ≤ V ∧ V ≤ 3 → V = 1 ∨ V = 2 ∨ V = 3
3 1 2 syl3an1 ⊢ V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3 → V = 1 ∨ V = 2 ∨ V = 3
4 hash1snb ⊢ V ∈ Fin → V = 1 ↔ ∃ a V = a
5 4 biimpa ⊢ V ∈ Fin ∧ V = 1 → ∃ a V = a
6 3mix1 ⊢ V = a → V = a ∨ V = a b ∨ V = a b c
7 6 2eximi ⊢ ∃ b ∃ c V = a → ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
8 7 19.23bi ⊢ ∃ c V = a → ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
9 8 19.23bi ⊢ V = a → ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
10 9 eximi ⊢ ∃ a V = a → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
11 5 10 syl ⊢ V ∈ Fin ∧ V = 1 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
12 11 expcom ⊢ V = 1 → V ∈ Fin → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
13 hash2pr ⊢ V ∈ Fin ∧ V = 2 → ∃ a ∃ b V = a b
14 3mix2 ⊢ V = a b → V = a ∨ V = a b ∨ V = a b c
15 14 eximi ⊢ ∃ c V = a b → ∃ c V = a ∨ V = a b ∨ V = a b c
16 15 19.23bi ⊢ V = a b → ∃ c V = a ∨ V = a b ∨ V = a b c
17 16 2eximi ⊢ ∃ a ∃ b V = a b → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
18 13 17 syl ⊢ V ∈ Fin ∧ V = 2 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
19 18 expcom ⊢ V = 2 → V ∈ Fin → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
20 hash3tr ⊢ V ∈ Fin ∧ V = 3 → ∃ a ∃ b ∃ c V = a b c
21 3mix3 ⊢ V = a b c → V = a ∨ V = a b ∨ V = a b c
22 21 eximi ⊢ ∃ c V = a b c → ∃ c V = a ∨ V = a b ∨ V = a b c
23 22 2eximi ⊢ ∃ a ∃ b ∃ c V = a b c → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
24 20 23 syl ⊢ V ∈ Fin ∧ V = 3 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
25 24 expcom ⊢ V = 3 → V ∈ Fin → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
26 12 19 25 3jaoi ⊢ V = 1 ∨ V = 2 ∨ V = 3 → V ∈ Fin → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
27 26 com12 ⊢ V ∈ Fin → V = 1 ∨ V = 2 ∨ V = 3 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
28 27 3ad2ant1 ⊢ V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3 → V = 1 ∨ V = 2 ∨ V = 3 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c
29 3 28 mpd ⊢ V ∈ Fin ∧ 1 ≤ V ∧ V ≤ 3 → ∃ a ∃ b ∃ c V = a ∨ V = a b ∨ V = a b c