This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashgt23el

Description: A set with more than two elements has at least three different elements. (Contributed by BTernaryTau, 21-Sep-2023)

Ref Expression
Assertion hashgt23el 
|- ( ( V e. W /\ 2 < ( # ` V ) ) -> E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )

Proof

Step Hyp Ref Expression
1 2pos 
 |-  0 < 2
2 0xr 
 |-  0 e. RR*
3 2re 
 |-  2 e. RR
4 3 rexri 
 |-  2 e. RR*
5 hashxrcl 
 |-  ( V e. W -> ( # ` V ) e. RR* )
6 xrlttr 
 |-  ( ( 0 e. RR* /\ 2 e. RR* /\ ( # ` V ) e. RR* ) -> ( ( 0 < 2 /\ 2 < ( # ` V ) ) -> 0 < ( # ` V ) ) )
7 2 4 5 6 mp3an12i 
 |-  ( V e. W -> ( ( 0 < 2 /\ 2 < ( # ` V ) ) -> 0 < ( # ` V ) ) )
8 1 7 mpani 
 |-  ( V e. W -> ( 2 < ( # ` V ) -> 0 < ( # ` V ) ) )
9 hashgt0elex 
 |-  ( ( V e. W /\ 0 < ( # ` V ) ) -> E. a a e. V )
10 9 ex 
 |-  ( V e. W -> ( 0 < ( # ` V ) -> E. a a e. V ) )
11 8 10 syld 
 |-  ( V e. W -> ( 2 < ( # ` V ) -> E. a a e. V ) )
12 11 imp 
 |-  ( ( V e. W /\ 2 < ( # ` V ) ) -> E. a a e. V )
13 difexg 
 |-  ( V e. W -> ( V \ { a } ) e. _V )
14 difsnid 
 |-  ( a e. V -> ( ( V \ { a } ) u. { a } ) = V )
15 14 fveq2d 
 |-  ( a e. V -> ( # ` ( ( V \ { a } ) u. { a } ) ) = ( # ` V ) )
16 15 breq2d 
 |-  ( a e. V -> ( 2 < ( # ` ( ( V \ { a } ) u. { a } ) ) <-> 2 < ( # ` V ) ) )
17 16 adantr 
 |-  ( ( a e. V /\ V e. W ) -> ( 2 < ( # ` ( ( V \ { a } ) u. { a } ) ) <-> 2 < ( # ` V ) ) )
18 df-2 
 |-  2 = ( 1 + 1 )
19 18 breq1i 
 |-  ( 2 < ( # ` ( ( V \ { a } ) u. { a } ) ) <-> ( 1 + 1 ) < ( # ` ( ( V \ { a } ) u. { a } ) ) )
20 neldifsn 
 |-  -. a e. ( V \ { a } )
21 1nn0 
 |-  1 e. NN0
22 hashunsnggt 
 |-  ( ( ( ( V \ { a } ) e. _V /\ a e. V /\ 1 e. NN0 ) /\ -. a e. ( V \ { a } ) ) -> ( 1 < ( # ` ( V \ { a } ) ) <-> ( 1 + 1 ) < ( # ` ( ( V \ { a } ) u. { a } ) ) ) )
23 21 22 mp3anl3 
 |-  ( ( ( ( V \ { a } ) e. _V /\ a e. V ) /\ -. a e. ( V \ { a } ) ) -> ( 1 < ( # ` ( V \ { a } ) ) <-> ( 1 + 1 ) < ( # ` ( ( V \ { a } ) u. { a } ) ) ) )
24 13 23 sylanl1 
 |-  ( ( ( V e. W /\ a e. V ) /\ -. a e. ( V \ { a } ) ) -> ( 1 < ( # ` ( V \ { a } ) ) <-> ( 1 + 1 ) < ( # ` ( ( V \ { a } ) u. { a } ) ) ) )
25 20 24 mpan2 
 |-  ( ( V e. W /\ a e. V ) -> ( 1 < ( # ` ( V \ { a } ) ) <-> ( 1 + 1 ) < ( # ` ( ( V \ { a } ) u. { a } ) ) ) )
26 25 biimp3ar 
 |-  ( ( V e. W /\ a e. V /\ ( 1 + 1 ) < ( # ` ( ( V \ { a } ) u. { a } ) ) ) -> 1 < ( # ` ( V \ { a } ) ) )
27 19 26 syl3an3b 
 |-  ( ( V e. W /\ a e. V /\ 2 < ( # ` ( ( V \ { a } ) u. { a } ) ) ) -> 1 < ( # ` ( V \ { a } ) ) )
28 27 3expia 
 |-  ( ( V e. W /\ a e. V ) -> ( 2 < ( # ` ( ( V \ { a } ) u. { a } ) ) -> 1 < ( # ` ( V \ { a } ) ) ) )
29 28 ancoms 
 |-  ( ( a e. V /\ V e. W ) -> ( 2 < ( # ` ( ( V \ { a } ) u. { a } ) ) -> 1 < ( # ` ( V \ { a } ) ) ) )
30 17 29 sylbird 
 |-  ( ( a e. V /\ V e. W ) -> ( 2 < ( # ` V ) -> 1 < ( # ` ( V \ { a } ) ) ) )
31 30 3impia 
 |-  ( ( a e. V /\ V e. W /\ 2 < ( # ` V ) ) -> 1 < ( # ` ( V \ { a } ) ) )
32 31 3expib 
 |-  ( a e. V -> ( ( V e. W /\ 2 < ( # ` V ) ) -> 1 < ( # ` ( V \ { a } ) ) ) )
33 1lt2 
 |-  1 < 2
34 1xr 
 |-  1 e. RR*
35 xrlttr 
 |-  ( ( 1 e. RR* /\ 2 e. RR* /\ ( # ` V ) e. RR* ) -> ( ( 1 < 2 /\ 2 < ( # ` V ) ) -> 1 < ( # ` V ) ) )
36 34 4 5 35 mp3an12i 
 |-  ( V e. W -> ( ( 1 < 2 /\ 2 < ( # ` V ) ) -> 1 < ( # ` V ) ) )
37 33 36 mpani 
 |-  ( V e. W -> ( 2 < ( # ` V ) -> 1 < ( # ` V ) ) )
38 37 imp 
 |-  ( ( V e. W /\ 2 < ( # ` V ) ) -> 1 < ( # ` V ) )
39 38 3adant1 
 |-  ( ( -. a e. V /\ V e. W /\ 2 < ( # ` V ) ) -> 1 < ( # ` V ) )
40 difsn 
 |-  ( -. a e. V -> ( V \ { a } ) = V )
41 40 3ad2ant1 
 |-  ( ( -. a e. V /\ V e. W /\ 2 < ( # ` V ) ) -> ( V \ { a } ) = V )
42 41 fveq2d 
 |-  ( ( -. a e. V /\ V e. W /\ 2 < ( # ` V ) ) -> ( # ` ( V \ { a } ) ) = ( # ` V ) )
43 39 42 breqtrrd 
 |-  ( ( -. a e. V /\ V e. W /\ 2 < ( # ` V ) ) -> 1 < ( # ` ( V \ { a } ) ) )
44 43 3expib 
 |-  ( -. a e. V -> ( ( V e. W /\ 2 < ( # ` V ) ) -> 1 < ( # ` ( V \ { a } ) ) ) )
45 32 44 pm2.61i 
 |-  ( ( V e. W /\ 2 < ( # ` V ) ) -> 1 < ( # ` ( V \ { a } ) ) )
46 hashgt12el 
 |-  ( ( ( V \ { a } ) e. _V /\ 1 < ( # ` ( V \ { a } ) ) ) -> E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c )
47 13 45 46 syl2an2r 
 |-  ( ( V e. W /\ 2 < ( # ` V ) ) -> E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c )
48 47 alrimiv 
 |-  ( ( V e. W /\ 2 < ( # ` V ) ) -> A. a E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c )
49 19.29r 
 |-  ( ( E. a a e. V /\ A. a E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c ) -> E. a ( a e. V /\ E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c ) )
50 12 48 49 syl2anc 
 |-  ( ( V e. W /\ 2 < ( # ` V ) ) -> E. a ( a e. V /\ E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c ) )
51 df-rex 
 |-  ( E. a e. V E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c <-> E. a ( a e. V /\ E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c ) )
52 eldifsn 
 |-  ( b e. ( V \ { a } ) <-> ( b e. V /\ b =/= a ) )
53 necom 
 |-  ( b =/= a <-> a =/= b )
54 53 anbi2i 
 |-  ( ( b e. V /\ b =/= a ) <-> ( b e. V /\ a =/= b ) )
55 52 54 bitri 
 |-  ( b e. ( V \ { a } ) <-> ( b e. V /\ a =/= b ) )
56 ax-5 
 |-  ( a =/= b -> A. c a =/= b )
57 56 anim2i 
 |-  ( ( b e. V /\ a =/= b ) -> ( b e. V /\ A. c a =/= b ) )
58 55 57 sylbi 
 |-  ( b e. ( V \ { a } ) -> ( b e. V /\ A. c a =/= b ) )
59 3anass 
 |-  ( ( c e. V /\ a =/= c /\ b =/= c ) <-> ( c e. V /\ ( a =/= c /\ b =/= c ) ) )
60 59 exbii 
 |-  ( E. c ( c e. V /\ a =/= c /\ b =/= c ) <-> E. c ( c e. V /\ ( a =/= c /\ b =/= c ) ) )
61 df-rex 
 |-  ( E. c e. ( V \ { a } ) b =/= c <-> E. c ( c e. ( V \ { a } ) /\ b =/= c ) )
62 eldifsn 
 |-  ( c e. ( V \ { a } ) <-> ( c e. V /\ c =/= a ) )
63 necom 
 |-  ( c =/= a <-> a =/= c )
64 63 anbi2i 
 |-  ( ( c e. V /\ c =/= a ) <-> ( c e. V /\ a =/= c ) )
65 62 64 bitri 
 |-  ( c e. ( V \ { a } ) <-> ( c e. V /\ a =/= c ) )
66 65 anbi1i 
 |-  ( ( c e. ( V \ { a } ) /\ b =/= c ) <-> ( ( c e. V /\ a =/= c ) /\ b =/= c ) )
67 df-3an 
 |-  ( ( c e. V /\ a =/= c /\ b =/= c ) <-> ( ( c e. V /\ a =/= c ) /\ b =/= c ) )
68 66 67 bitr4i 
 |-  ( ( c e. ( V \ { a } ) /\ b =/= c ) <-> ( c e. V /\ a =/= c /\ b =/= c ) )
69 68 exbii 
 |-  ( E. c ( c e. ( V \ { a } ) /\ b =/= c ) <-> E. c ( c e. V /\ a =/= c /\ b =/= c ) )
70 61 69 bitri 
 |-  ( E. c e. ( V \ { a } ) b =/= c <-> E. c ( c e. V /\ a =/= c /\ b =/= c ) )
71 df-rex 
 |-  ( E. c e. V ( a =/= c /\ b =/= c ) <-> E. c ( c e. V /\ ( a =/= c /\ b =/= c ) ) )
72 60 70 71 3bitr4i 
 |-  ( E. c e. ( V \ { a } ) b =/= c <-> E. c e. V ( a =/= c /\ b =/= c ) )
73 72 biimpi 
 |-  ( E. c e. ( V \ { a } ) b =/= c -> E. c e. V ( a =/= c /\ b =/= c ) )
74 58 73 anim12i 
 |-  ( ( b e. ( V \ { a } ) /\ E. c e. ( V \ { a } ) b =/= c ) -> ( ( b e. V /\ A. c a =/= b ) /\ E. c e. V ( a =/= c /\ b =/= c ) ) )
75 alral 
 |-  ( A. c a =/= b -> A. c e. V a =/= b )
76 75 anim1i 
 |-  ( ( A. c a =/= b /\ E. c e. V ( a =/= c /\ b =/= c ) ) -> ( A. c e. V a =/= b /\ E. c e. V ( a =/= c /\ b =/= c ) ) )
77 r19.29 
 |-  ( ( A. c e. V a =/= b /\ E. c e. V ( a =/= c /\ b =/= c ) ) -> E. c e. V ( a =/= b /\ ( a =/= c /\ b =/= c ) ) )
78 3anass 
 |-  ( ( a =/= b /\ a =/= c /\ b =/= c ) <-> ( a =/= b /\ ( a =/= c /\ b =/= c ) ) )
79 78 biimpri 
 |-  ( ( a =/= b /\ ( a =/= c /\ b =/= c ) ) -> ( a =/= b /\ a =/= c /\ b =/= c ) )
80 79 reximi 
 |-  ( E. c e. V ( a =/= b /\ ( a =/= c /\ b =/= c ) ) -> E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )
81 76 77 80 3syl 
 |-  ( ( A. c a =/= b /\ E. c e. V ( a =/= c /\ b =/= c ) ) -> E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )
82 81 anim2i 
 |-  ( ( b e. V /\ ( A. c a =/= b /\ E. c e. V ( a =/= c /\ b =/= c ) ) ) -> ( b e. V /\ E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) ) )
83 82 anassrs 
 |-  ( ( ( b e. V /\ A. c a =/= b ) /\ E. c e. V ( a =/= c /\ b =/= c ) ) -> ( b e. V /\ E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) ) )
84 74 83 syl 
 |-  ( ( b e. ( V \ { a } ) /\ E. c e. ( V \ { a } ) b =/= c ) -> ( b e. V /\ E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) ) )
85 84 reximi2 
 |-  ( E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c -> E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )
86 85 reximi 
 |-  ( E. a e. V E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c -> E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )
87 51 86 sylbir 
 |-  ( E. a ( a e. V /\ E. b e. ( V \ { a } ) E. c e. ( V \ { a } ) b =/= c ) -> E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )
88 50 87 syl 
 |-  ( ( V e. W /\ 2 < ( # ` V ) ) -> E. a e. V E. b e. V E. c e. V ( a =/= b /\ a =/= c /\ b =/= c ) )