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 ( ( 𝑉 ∈ Fin ∧ 1 ≤ ( ♯ ‘ 𝑉 ) ∧ ( ♯ ‘ 𝑉 ) ≤ 3 ) → ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑉 = { 𝑎 } ∨ 𝑉 = { 𝑎 , 𝑏 } ∨ 𝑉 = { 𝑎 , 𝑏 , 𝑐 } ) )

Proof

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