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∈W∧2<V→∃a∈V∃b∈V∃c∈Va≠b∧a≠c∧b≠c

Proof

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