Proof of Theorem hashgt23el
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2pos 12370 | . . . . . 6
⊢ 0 <
2 | 
| 2 |  | 0xr 11309 | . . . . . . 7
⊢ 0 ∈
ℝ* | 
| 3 |  | 2re 12341 | . . . . . . . 8
⊢ 2 ∈
ℝ | 
| 4 | 3 | rexri 11320 | . . . . . . 7
⊢ 2 ∈
ℝ* | 
| 5 |  | hashxrcl 14397 | . . . . . . 7
⊢ (𝑉 ∈ 𝑊 → (♯‘𝑉) ∈
ℝ*) | 
| 6 |  | xrlttr 13183 | . . . . . . 7
⊢ ((0
∈ ℝ* ∧ 2 ∈ ℝ* ∧
(♯‘𝑉) ∈
ℝ*) → ((0 < 2 ∧ 2 < (♯‘𝑉)) → 0 <
(♯‘𝑉))) | 
| 7 | 2, 4, 5, 6 | mp3an12i 1466 | . . . . . 6
⊢ (𝑉 ∈ 𝑊 → ((0 < 2 ∧ 2 <
(♯‘𝑉)) → 0
< (♯‘𝑉))) | 
| 8 | 1, 7 | mpani 696 | . . . . 5
⊢ (𝑉 ∈ 𝑊 → (2 < (♯‘𝑉) → 0 <
(♯‘𝑉))) | 
| 9 |  | hashgt0elex 14441 | . . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 0 < (♯‘𝑉)) → ∃𝑎 𝑎 ∈ 𝑉) | 
| 10 | 9 | ex 412 | . . . . 5
⊢ (𝑉 ∈ 𝑊 → (0 < (♯‘𝑉) → ∃𝑎 𝑎 ∈ 𝑉)) | 
| 11 | 8, 10 | syld 47 | . . . 4
⊢ (𝑉 ∈ 𝑊 → (2 < (♯‘𝑉) → ∃𝑎 𝑎 ∈ 𝑉)) | 
| 12 | 11 | imp 406 | . . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 𝑎 ∈ 𝑉) | 
| 13 |  | difexg 5328 | . . . . 5
⊢ (𝑉 ∈ 𝑊 → (𝑉 ∖ {𝑎}) ∈ V) | 
| 14 |  | difsnid 4809 | . . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑉 → ((𝑉 ∖ {𝑎}) ∪ {𝑎}) = 𝑉) | 
| 15 | 14 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑎 ∈ 𝑉 → (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) = (♯‘𝑉)) | 
| 16 | 15 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝑎 ∈ 𝑉 → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) ↔ 2 < (♯‘𝑉))) | 
| 17 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊) → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) ↔ 2 < (♯‘𝑉))) | 
| 18 |  | df-2 12330 | . . . . . . . . . . . . 13
⊢ 2 = (1 +
1) | 
| 19 | 18 | breq1i 5149 | . . . . . . . . . . . 12
⊢ (2 <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎}))) | 
| 20 |  | neldifsn 4791 | . . . . . . . . . . . . . 14
⊢  ¬
𝑎 ∈ (𝑉 ∖ {𝑎}) | 
| 21 |  | 1nn0 12544 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 | 
| 22 |  | hashunsnggt 14434 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑉 ∖ {𝑎}) ∈ V ∧ 𝑎 ∈ 𝑉 ∧ 1 ∈ ℕ0) ∧
¬ 𝑎 ∈ (𝑉 ∖ {𝑎})) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) | 
| 23 | 21, 22 | mp3anl3 1458 | . . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∖ {𝑎}) ∈ V ∧ 𝑎 ∈ 𝑉) ∧ ¬ 𝑎 ∈ (𝑉 ∖ {𝑎})) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) | 
| 24 | 13, 23 | sylanl1 680 | . . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉) ∧ ¬ 𝑎 ∈ (𝑉 ∖ {𝑎})) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) | 
| 25 | 20, 24 | mpan2 691 | . . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) | 
| 26 | 25 | biimp3ar 1471 | . . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉 ∧ (1 + 1) < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎}))) → 1 < (♯‘(𝑉 ∖ {𝑎}))) | 
| 27 | 19, 26 | syl3an3b 1406 | . . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉 ∧ 2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎}))) → 1 < (♯‘(𝑉 ∖ {𝑎}))) | 
| 28 | 27 | 3expia 1121 | . . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉) → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) → 1 < (♯‘(𝑉 ∖ {𝑎})))) | 
| 29 | 28 | ancoms 458 | . . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊) → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) → 1 < (♯‘(𝑉 ∖ {𝑎})))) | 
| 30 | 17, 29 | sylbird 260 | . . . . . . . 8
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊) → (2 < (♯‘𝑉) → 1 <
(♯‘(𝑉 ∖
{𝑎})))) | 
| 31 | 30 | 3impia 1117 | . . . . . . 7
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎}))) | 
| 32 | 31 | 3expib 1122 | . . . . . 6
⊢ (𝑎 ∈ 𝑉 → ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎})))) | 
| 33 |  | 1lt2 12438 | . . . . . . . . . . 11
⊢ 1 <
2 | 
| 34 |  | 1xr 11321 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ* | 
| 35 |  | xrlttr 13183 | . . . . . . . . . . . 12
⊢ ((1
∈ ℝ* ∧ 2 ∈ ℝ* ∧
(♯‘𝑉) ∈
ℝ*) → ((1 < 2 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘𝑉))) | 
| 36 | 34, 4, 5, 35 | mp3an12i 1466 | . . . . . . . . . . 11
⊢ (𝑉 ∈ 𝑊 → ((1 < 2 ∧ 2 <
(♯‘𝑉)) → 1
< (♯‘𝑉))) | 
| 37 | 33, 36 | mpani 696 | . . . . . . . . . 10
⊢ (𝑉 ∈ 𝑊 → (2 < (♯‘𝑉) → 1 <
(♯‘𝑉))) | 
| 38 | 37 | imp 406 | . . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘𝑉)) | 
| 39 | 38 | 3adant1 1130 | . . . . . . . 8
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘𝑉)) | 
| 40 |  | difsn 4797 | . . . . . . . . . 10
⊢ (¬
𝑎 ∈ 𝑉 → (𝑉 ∖ {𝑎}) = 𝑉) | 
| 41 | 40 | 3ad2ant1 1133 | . . . . . . . . 9
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → (𝑉 ∖ {𝑎}) = 𝑉) | 
| 42 | 41 | fveq2d 6909 | . . . . . . . 8
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → (♯‘(𝑉 ∖ {𝑎})) = (♯‘𝑉)) | 
| 43 | 39, 42 | breqtrrd 5170 | . . . . . . 7
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎}))) | 
| 44 | 43 | 3expib 1122 | . . . . . 6
⊢ (¬
𝑎 ∈ 𝑉 → ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎})))) | 
| 45 | 32, 44 | pm2.61i 182 | . . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎}))) | 
| 46 |  | hashgt12el 14462 | . . . . 5
⊢ (((𝑉 ∖ {𝑎}) ∈ V ∧ 1 <
(♯‘(𝑉 ∖
{𝑎}))) → ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) | 
| 47 | 13, 45, 46 | syl2an2r 685 | . . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) | 
| 48 | 47 | alrimiv 1926 | . . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∀𝑎∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) | 
| 49 |  | 19.29r 1873 | . . 3
⊢
((∃𝑎 𝑎 ∈ 𝑉 ∧ ∀𝑎∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → ∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐)) | 
| 50 | 12, 48, 49 | syl2anc 584 | . 2
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐)) | 
| 51 |  | df-rex 3070 | . . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐)) | 
| 52 |  | eldifsn 4785 | . . . . . . . . 9
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎)) | 
| 53 |  | necom 2993 | . . . . . . . . . 10
⊢ (𝑏 ≠ 𝑎 ↔ 𝑎 ≠ 𝑏) | 
| 54 | 53 | anbi2i 623 | . . . . . . . . 9
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎) ↔ (𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) | 
| 55 | 52, 54 | bitri 275 | . . . . . . . 8
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) | 
| 56 |  | ax-5 1909 | . . . . . . . . 9
⊢ (𝑎 ≠ 𝑏 → ∀𝑐 𝑎 ≠ 𝑏) | 
| 57 | 56 | anim2i 617 | . . . . . . . 8
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏) → (𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏)) | 
| 58 | 55, 57 | sylbi 217 | . . . . . . 7
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → (𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏)) | 
| 59 |  | 3anass 1094 | . . . . . . . . . 10
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑐 ∈ 𝑉 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 60 | 59 | exbii 1847 | . . . . . . . . 9
⊢
(∃𝑐(𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 61 |  | df-rex 3070 | . . . . . . . . . 10
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑐(𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐)) | 
| 62 |  | eldifsn 4785 | . . . . . . . . . . . . . 14
⊢ (𝑐 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑐 ∈ 𝑉 ∧ 𝑐 ≠ 𝑎)) | 
| 63 |  | necom 2993 | . . . . . . . . . . . . . . 15
⊢ (𝑐 ≠ 𝑎 ↔ 𝑎 ≠ 𝑐) | 
| 64 | 63 | anbi2i 623 | . . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑐 ≠ 𝑎) ↔ (𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐)) | 
| 65 | 62, 64 | bitri 275 | . . . . . . . . . . . . 13
⊢ (𝑐 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐)) | 
| 66 | 65 | anbi1i 624 | . . . . . . . . . . . 12
⊢ ((𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐) ↔ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐) ∧ 𝑏 ≠ 𝑐)) | 
| 67 |  | df-3an 1088 | . . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐) ∧ 𝑏 ≠ 𝑐)) | 
| 68 | 66, 67 | bitr4i 278 | . . . . . . . . . . 11
⊢ ((𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐) ↔ (𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 69 | 68 | exbii 1847 | . . . . . . . . . 10
⊢
(∃𝑐(𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 70 | 61, 69 | bitri 275 | . . . . . . . . 9
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 71 |  | df-rex 3070 | . . . . . . . . 9
⊢
(∃𝑐 ∈
𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 72 | 60, 70, 71 | 3bitr4i 303 | . . . . . . . 8
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 73 | 72 | biimpi 216 | . . . . . . 7
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 74 | 58, 73 | anim12i 613 | . . . . . 6
⊢ ((𝑏 ∈ (𝑉 ∖ {𝑎}) ∧ ∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → ((𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏) ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 75 |  | alral 3074 | . . . . . . . . . 10
⊢
(∀𝑐 𝑎 ≠ 𝑏 → ∀𝑐 ∈ 𝑉 𝑎 ≠ 𝑏) | 
| 76 | 75 | anim1i 615 | . . . . . . . . 9
⊢
((∀𝑐 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (∀𝑐 ∈ 𝑉 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 77 |  | r19.29 3113 | . . . . . . . . 9
⊢
((∀𝑐 ∈
𝑉 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 78 |  | 3anass 1094 | . . . . . . . . . . 11
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 79 | 78 | biimpri 228 | . . . . . . . . . 10
⊢ ((𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 80 | 79 | reximi 3083 | . . . . . . . . 9
⊢
(∃𝑐 ∈
𝑉 (𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 81 | 76, 77, 80 | 3syl 18 | . . . . . . . 8
⊢
((∀𝑐 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 82 | 81 | anim2i 617 | . . . . . . 7
⊢ ((𝑏 ∈ 𝑉 ∧ (∀𝑐 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) → (𝑏 ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 83 | 82 | anassrs 467 | . . . . . 6
⊢ (((𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏) ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (𝑏 ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 84 | 74, 83 | syl 17 | . . . . 5
⊢ ((𝑏 ∈ (𝑉 ∖ {𝑎}) ∧ ∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → (𝑏 ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) | 
| 85 | 84 | reximi2 3078 | . . . 4
⊢
(∃𝑏 ∈
(𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 86 | 85 | reximi 3083 | . . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 87 | 51, 86 | sylbir 235 | . 2
⊢
(∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) | 
| 88 | 50, 87 | syl 17 | 1
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |