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 e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )

Proof

Step Hyp Ref Expression
1 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
2 nn01to3 
 |-  ( ( ( # ` V ) e. NN0 /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 2 \/ ( # ` V ) = 3 ) )
3 1 2 syl3an1 
 |-  ( ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 2 \/ ( # ` V ) = 3 ) )
4 hash1snb 
 |-  ( V e. Fin -> ( ( # ` V ) = 1 <-> E. a V = { a } ) )
5 4 biimpa 
 |-  ( ( V e. Fin /\ ( # ` V ) = 1 ) -> E. a V = { a } )
6 3mix1 
 |-  ( V = { a } -> ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
7 6 2eximi 
 |-  ( E. b E. c V = { a } -> E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
8 7 19.23bi 
 |-  ( E. c V = { a } -> E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
9 8 19.23bi 
 |-  ( V = { a } -> E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
10 9 eximi 
 |-  ( E. a V = { a } -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
11 5 10 syl 
 |-  ( ( V e. Fin /\ ( # ` V ) = 1 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
12 11 expcom 
 |-  ( ( # ` V ) = 1 -> ( V e. Fin -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) ) )
13 hash2pr 
 |-  ( ( V e. Fin /\ ( # ` V ) = 2 ) -> E. a E. b V = { a , b } )
14 3mix2 
 |-  ( V = { a , b } -> ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
15 14 eximi 
 |-  ( E. c V = { a , b } -> E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
16 15 19.23bi 
 |-  ( V = { a , b } -> E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
17 16 2eximi 
 |-  ( E. a E. b V = { a , b } -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
18 13 17 syl 
 |-  ( ( V e. Fin /\ ( # ` V ) = 2 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
19 18 expcom 
 |-  ( ( # ` V ) = 2 -> ( V e. Fin -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) ) )
20 hash3tr 
 |-  ( ( V e. Fin /\ ( # ` V ) = 3 ) -> E. a E. b E. c V = { a , b , c } )
21 3mix3 
 |-  ( V = { a , b , c } -> ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
22 21 eximi 
 |-  ( E. c V = { a , b , c } -> E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
23 22 2eximi 
 |-  ( E. a E. b E. c V = { a , b , c } -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
24 20 23 syl 
 |-  ( ( V e. Fin /\ ( # ` V ) = 3 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )
25 24 expcom 
 |-  ( ( # ` V ) = 3 -> ( V e. Fin -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) ) )
26 12 19 25 3jaoi 
 |-  ( ( ( # ` V ) = 1 \/ ( # ` V ) = 2 \/ ( # ` V ) = 3 ) -> ( V e. Fin -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) ) )
27 26 com12 
 |-  ( V e. Fin -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 2 \/ ( # ` V ) = 3 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) ) )
28 27 3ad2ant1 
 |-  ( ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 2 \/ ( # ` V ) = 3 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) ) )
29 3 28 mpd 
 |-  ( ( V e. Fin /\ 1 <_ ( # ` V ) /\ ( # ` V ) <_ 3 ) -> E. a E. b E. c ( V = { a } \/ V = { a , b } \/ V = { a , b , c } ) )