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 ∈ V a ≠ 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 → ∃ a a ∈ V
10 9 ex ⊢ V ∈ W → 0 < V → ∃ a a ∈ V
11 8 10 syld ⊢ V ∈ W → 2 < V → ∃ a a ∈ V
12 11 imp ⊢ V ∈ W ∧ 2 < V → ∃ a a ∈ 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 ∖ a b ≠ c
47 13 45 46 syl2an2r ⊢ V ∈ W ∧ 2 < V → ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c
48 47 alrimiv ⊢ V ∈ W ∧ 2 < V → ∀ a ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c
49 19.29r ⊢ ∃ a a ∈ V ∧ ∀ a ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c → ∃ a a ∈ V ∧ ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c
50 12 48 49 syl2anc ⊢ V ∈ W ∧ 2 < V → ∃ a a ∈ V ∧ ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c
51 df-rex ⊢ ∃ a ∈ V ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c ↔ ∃ a a ∈ V ∧ ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ 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 → ∀ c a ≠ b
57 56 anim2i ⊢ b ∈ V ∧ a ≠ b → b ∈ V ∧ ∀ c a ≠ b
58 55 57 sylbi ⊢ b ∈ V ∖ a → b ∈ V ∧ ∀ c a ≠ b
59 3anass ⊢ c ∈ V ∧ a ≠ c ∧ b ≠ c ↔ c ∈ V ∧ a ≠ c ∧ b ≠ c
60 59 exbii ⊢ ∃ c c ∈ V ∧ a ≠ c ∧ b ≠ c ↔ ∃ c c ∈ V ∧ a ≠ c ∧ b ≠ c
61 df-rex ⊢ ∃ c ∈ V ∖ a b ≠ c ↔ ∃ c c ∈ 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 ⊢ ∃ c c ∈ V ∖ a ∧ b ≠ c ↔ ∃ c c ∈ V ∧ a ≠ c ∧ b ≠ c
70 61 69 bitri ⊢ ∃ c ∈ V ∖ a b ≠ c ↔ ∃ c c ∈ V ∧ a ≠ c ∧ b ≠ c
71 df-rex ⊢ ∃ c ∈ V a ≠ c ∧ b ≠ c ↔ ∃ c c ∈ V ∧ a ≠ c ∧ b ≠ c
72 60 70 71 3bitr4i ⊢ ∃ c ∈ V ∖ a b ≠ c ↔ ∃ c ∈ V a ≠ c ∧ b ≠ c
73 72 biimpi ⊢ ∃ c ∈ V ∖ a b ≠ c → ∃ c ∈ V a ≠ c ∧ b ≠ c
74 58 73 anim12i ⊢ b ∈ V ∖ a ∧ ∃ c ∈ V ∖ a b ≠ c → b ∈ V ∧ ∀ c a ≠ b ∧ ∃ c ∈ V a ≠ c ∧ b ≠ c
75 alral ⊢ ∀ c a ≠ b → ∀ c ∈ V a ≠ b
76 75 anim1i ⊢ ∀ c a ≠ b ∧ ∃ c ∈ V a ≠ c ∧ b ≠ c → ∀ c ∈ V a ≠ b ∧ ∃ c ∈ V a ≠ c ∧ b ≠ c
77 r19.29 ⊢ ∀ c ∈ V a ≠ b ∧ ∃ c ∈ V a ≠ c ∧ b ≠ c → ∃ c ∈ 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 ⊢ ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c → ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
81 76 77 80 3syl ⊢ ∀ c a ≠ b ∧ ∃ c ∈ V a ≠ c ∧ b ≠ c → ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
82 81 anim2i ⊢ b ∈ V ∧ ∀ c a ≠ b ∧ ∃ c ∈ V a ≠ c ∧ b ≠ c → b ∈ V ∧ ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
83 82 anassrs ⊢ b ∈ V ∧ ∀ c a ≠ b ∧ ∃ c ∈ V a ≠ c ∧ b ≠ c → b ∈ V ∧ ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
84 74 83 syl ⊢ b ∈ V ∖ a ∧ ∃ c ∈ V ∖ a b ≠ c → b ∈ V ∧ ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
85 84 reximi2 ⊢ ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c → ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
86 85 reximi ⊢ ∃ a ∈ V ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
87 51 86 sylbir ⊢ ∃ a a ∈ V ∧ ∃ b ∈ V ∖ a ∃ c ∈ V ∖ a b ≠ c → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c
88 50 87 syl ⊢ V ∈ W ∧ 2 < V → ∃ a ∈ V ∃ b ∈ V ∃ c ∈ V a ≠ b ∧ a ≠ c ∧ b ≠ c