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∃cV=a∨V=ab∨V=abc

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↔∃aV=a
5 4 biimpa ⊢V∈Fin∧V=1→∃aV=a
6 3mix1 ⊢V=a→V=a∨V=ab∨V=abc
7 6 2eximi ⊢∃b∃cV=a→∃b∃cV=a∨V=ab∨V=abc
8 7 19.23bi ⊢∃cV=a→∃b∃cV=a∨V=ab∨V=abc
9 8 19.23bi ⊢V=a→∃b∃cV=a∨V=ab∨V=abc
10 9 eximi ⊢∃aV=a→∃a∃b∃cV=a∨V=ab∨V=abc
11 5 10 syl ⊢V∈Fin∧V=1→∃a∃b∃cV=a∨V=ab∨V=abc
12 11 expcom ⊢V=1→V∈Fin→∃a∃b∃cV=a∨V=ab∨V=abc
13 hash2pr ⊢V∈Fin∧V=2→∃a∃bV=ab
14 3mix2 ⊢V=ab→V=a∨V=ab∨V=abc
15 14 eximi ⊢∃cV=ab→∃cV=a∨V=ab∨V=abc
16 15 19.23bi ⊢V=ab→∃cV=a∨V=ab∨V=abc
17 16 2eximi ⊢∃a∃bV=ab→∃a∃b∃cV=a∨V=ab∨V=abc
18 13 17 syl ⊢V∈Fin∧V=2→∃a∃b∃cV=a∨V=ab∨V=abc
19 18 expcom ⊢V=2→V∈Fin→∃a∃b∃cV=a∨V=ab∨V=abc
20 hash3tr ⊢V∈Fin∧V=3→∃a∃b∃cV=abc
21 3mix3 ⊢V=abc→V=a∨V=ab∨V=abc
22 21 eximi ⊢∃cV=abc→∃cV=a∨V=ab∨V=abc
23 22 2eximi ⊢∃a∃b∃cV=abc→∃a∃b∃cV=a∨V=ab∨V=abc
24 20 23 syl ⊢V∈Fin∧V=3→∃a∃b∃cV=a∨V=ab∨V=abc
25 24 expcom ⊢V=3→V∈Fin→∃a∃b∃cV=a∨V=ab∨V=abc
26 12 19 25 3jaoi ⊢V=1∨V=2∨V=3→V∈Fin→∃a∃b∃cV=a∨V=ab∨V=abc
27 26 com12 ⊢V∈Fin→V=1∨V=2∨V=3→∃a∃b∃cV=a∨V=ab∨V=abc
28 27 3ad2ant1 ⊢V∈Fin∧1≤V∧V≤3→V=1∨V=2∨V=3→∃a∃b∃cV=a∨V=ab∨V=abc
29 3 28 mpd ⊢V∈Fin∧1≤V∧V≤3→∃a∃b∃cV=a∨V=ab∨V=abc