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 ( ( 𝑉 ∈ 𝑊 ∧ 2 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )

Proof

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