Proof of Theorem hashgt23el
Step | Hyp | Ref
| Expression |
1 | | 2pos 12076 |
. . . . . 6
⊢ 0 <
2 |
2 | | 0xr 11022 |
. . . . . . 7
⊢ 0 ∈
ℝ* |
3 | | 2re 12047 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
4 | 3 | rexri 11033 |
. . . . . . 7
⊢ 2 ∈
ℝ* |
5 | | hashxrcl 14072 |
. . . . . . 7
⊢ (𝑉 ∈ 𝑊 → (♯‘𝑉) ∈
ℝ*) |
6 | | xrlttr 12874 |
. . . . . . 7
⊢ ((0
∈ ℝ* ∧ 2 ∈ ℝ* ∧
(♯‘𝑉) ∈
ℝ*) → ((0 < 2 ∧ 2 < (♯‘𝑉)) → 0 <
(♯‘𝑉))) |
7 | 2, 4, 5, 6 | mp3an12i 1464 |
. . . . . 6
⊢ (𝑉 ∈ 𝑊 → ((0 < 2 ∧ 2 <
(♯‘𝑉)) → 0
< (♯‘𝑉))) |
8 | 1, 7 | mpani 693 |
. . . . 5
⊢ (𝑉 ∈ 𝑊 → (2 < (♯‘𝑉) → 0 <
(♯‘𝑉))) |
9 | | hashgt0elex 14116 |
. . . . . 6
⊢ ((𝑉 ∈ 𝑊 ∧ 0 < (♯‘𝑉)) → ∃𝑎 𝑎 ∈ 𝑉) |
10 | 9 | ex 413 |
. . . . 5
⊢ (𝑉 ∈ 𝑊 → (0 < (♯‘𝑉) → ∃𝑎 𝑎 ∈ 𝑉)) |
11 | 8, 10 | syld 47 |
. . . 4
⊢ (𝑉 ∈ 𝑊 → (2 < (♯‘𝑉) → ∃𝑎 𝑎 ∈ 𝑉)) |
12 | 11 | imp 407 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 𝑎 ∈ 𝑉) |
13 | | difexg 5251 |
. . . . 5
⊢ (𝑉 ∈ 𝑊 → (𝑉 ∖ {𝑎}) ∈ V) |
14 | | difsnid 4743 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑉 → ((𝑉 ∖ {𝑎}) ∪ {𝑎}) = 𝑉) |
15 | 14 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ 𝑉 → (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) = (♯‘𝑉)) |
16 | 15 | breq2d 5086 |
. . . . . . . . . 10
⊢ (𝑎 ∈ 𝑉 → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) ↔ 2 < (♯‘𝑉))) |
17 | 16 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊) → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) ↔ 2 < (♯‘𝑉))) |
18 | | df-2 12036 |
. . . . . . . . . . . . 13
⊢ 2 = (1 +
1) |
19 | 18 | breq1i 5081 |
. . . . . . . . . . . 12
⊢ (2 <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎}))) |
20 | | neldifsn 4725 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑎 ∈ (𝑉 ∖ {𝑎}) |
21 | | 1nn0 12249 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
22 | | hashunsnggt 14109 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑉 ∖ {𝑎}) ∈ V ∧ 𝑎 ∈ 𝑉 ∧ 1 ∈ ℕ0) ∧
¬ 𝑎 ∈ (𝑉 ∖ {𝑎})) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) |
23 | 21, 22 | mp3anl3 1456 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑉 ∖ {𝑎}) ∈ V ∧ 𝑎 ∈ 𝑉) ∧ ¬ 𝑎 ∈ (𝑉 ∖ {𝑎})) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) |
24 | 13, 23 | sylanl1 677 |
. . . . . . . . . . . . . 14
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉) ∧ ¬ 𝑎 ∈ (𝑉 ∖ {𝑎})) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) |
25 | 20, 24 | mpan2 688 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉) → (1 < (♯‘(𝑉 ∖ {𝑎})) ↔ (1 + 1) <
(♯‘((𝑉 ∖
{𝑎}) ∪ {𝑎})))) |
26 | 25 | biimp3ar 1469 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉 ∧ (1 + 1) < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎}))) → 1 < (♯‘(𝑉 ∖ {𝑎}))) |
27 | 19, 26 | syl3an3b 1404 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉 ∧ 2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎}))) → 1 < (♯‘(𝑉 ∖ {𝑎}))) |
28 | 27 | 3expia 1120 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉) → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) → 1 < (♯‘(𝑉 ∖ {𝑎})))) |
29 | 28 | ancoms 459 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊) → (2 < (♯‘((𝑉 ∖ {𝑎}) ∪ {𝑎})) → 1 < (♯‘(𝑉 ∖ {𝑎})))) |
30 | 17, 29 | sylbird 259 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊) → (2 < (♯‘𝑉) → 1 <
(♯‘(𝑉 ∖
{𝑎})))) |
31 | 30 | 3impia 1116 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎}))) |
32 | 31 | 3expib 1121 |
. . . . . 6
⊢ (𝑎 ∈ 𝑉 → ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎})))) |
33 | | 1lt2 12144 |
. . . . . . . . . . 11
⊢ 1 <
2 |
34 | | 1xr 11034 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ* |
35 | | xrlttr 12874 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ* ∧ 2 ∈ ℝ* ∧
(♯‘𝑉) ∈
ℝ*) → ((1 < 2 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘𝑉))) |
36 | 34, 4, 5, 35 | mp3an12i 1464 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ 𝑊 → ((1 < 2 ∧ 2 <
(♯‘𝑉)) → 1
< (♯‘𝑉))) |
37 | 33, 36 | mpani 693 |
. . . . . . . . . 10
⊢ (𝑉 ∈ 𝑊 → (2 < (♯‘𝑉) → 1 <
(♯‘𝑉))) |
38 | 37 | imp 407 |
. . . . . . . . 9
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘𝑉)) |
39 | 38 | 3adant1 1129 |
. . . . . . . 8
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘𝑉)) |
40 | | difsn 4731 |
. . . . . . . . . 10
⊢ (¬
𝑎 ∈ 𝑉 → (𝑉 ∖ {𝑎}) = 𝑉) |
41 | 40 | 3ad2ant1 1132 |
. . . . . . . . 9
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → (𝑉 ∖ {𝑎}) = 𝑉) |
42 | 41 | fveq2d 6778 |
. . . . . . . 8
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → (♯‘(𝑉 ∖ {𝑎})) = (♯‘𝑉)) |
43 | 39, 42 | breqtrrd 5102 |
. . . . . . 7
⊢ ((¬
𝑎 ∈ 𝑉 ∧ 𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎}))) |
44 | 43 | 3expib 1121 |
. . . . . 6
⊢ (¬
𝑎 ∈ 𝑉 → ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎})))) |
45 | 32, 44 | pm2.61i 182 |
. . . . 5
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → 1 <
(♯‘(𝑉 ∖
{𝑎}))) |
46 | | hashgt12el 14137 |
. . . . 5
⊢ (((𝑉 ∖ {𝑎}) ∈ V ∧ 1 <
(♯‘(𝑉 ∖
{𝑎}))) → ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) |
47 | 13, 45, 46 | syl2an2r 682 |
. . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) |
48 | 47 | alrimiv 1930 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∀𝑎∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) |
49 | | 19.29r 1877 |
. . 3
⊢
((∃𝑎 𝑎 ∈ 𝑉 ∧ ∀𝑎∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → ∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐)) |
50 | 12, 48, 49 | syl2anc 584 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐)) |
51 | | df-rex 3070 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐)) |
52 | | eldifsn 4720 |
. . . . . . . . 9
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎)) |
53 | | necom 2997 |
. . . . . . . . . 10
⊢ (𝑏 ≠ 𝑎 ↔ 𝑎 ≠ 𝑏) |
54 | 53 | anbi2i 623 |
. . . . . . . . 9
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎) ↔ (𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) |
55 | 52, 54 | bitri 274 |
. . . . . . . 8
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏)) |
56 | | ax-5 1913 |
. . . . . . . . 9
⊢ (𝑎 ≠ 𝑏 → ∀𝑐 𝑎 ≠ 𝑏) |
57 | 56 | anim2i 617 |
. . . . . . . 8
⊢ ((𝑏 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏) → (𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏)) |
58 | 55, 57 | sylbi 216 |
. . . . . . 7
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → (𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏)) |
59 | | 3anass 1094 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑐 ∈ 𝑉 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
60 | 59 | exbii 1850 |
. . . . . . . . 9
⊢
(∃𝑐(𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
61 | | df-rex 3070 |
. . . . . . . . . 10
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑐(𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐)) |
62 | | eldifsn 4720 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑐 ∈ 𝑉 ∧ 𝑐 ≠ 𝑎)) |
63 | | necom 2997 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ≠ 𝑎 ↔ 𝑎 ≠ 𝑐) |
64 | 63 | anbi2i 623 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑐 ≠ 𝑎) ↔ (𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐)) |
65 | 62, 64 | bitri 274 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐)) |
66 | 65 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐) ↔ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐) ∧ 𝑏 ≠ 𝑐)) |
67 | | df-3an 1088 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ((𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐) ∧ 𝑏 ≠ 𝑐)) |
68 | 66, 67 | bitr4i 277 |
. . . . . . . . . . 11
⊢ ((𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐) ↔ (𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
69 | 68 | exbii 1850 |
. . . . . . . . . 10
⊢
(∃𝑐(𝑐 ∈ (𝑉 ∖ {𝑎}) ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
70 | 61, 69 | bitri 274 |
. . . . . . . . 9
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
71 | | df-rex 3070 |
. . . . . . . . 9
⊢
(∃𝑐 ∈
𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑐 ∈ 𝑉 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
72 | 60, 70, 71 | 3bitr4i 303 |
. . . . . . . 8
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 ↔ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
73 | 72 | biimpi 215 |
. . . . . . 7
⊢
(∃𝑐 ∈
(𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
74 | 58, 73 | anim12i 613 |
. . . . . 6
⊢ ((𝑏 ∈ (𝑉 ∖ {𝑎}) ∧ ∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → ((𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏) ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
75 | | alral 3080 |
. . . . . . . . . 10
⊢
(∀𝑐 𝑎 ≠ 𝑏 → ∀𝑐 ∈ 𝑉 𝑎 ≠ 𝑏) |
76 | 75 | anim1i 615 |
. . . . . . . . 9
⊢
((∀𝑐 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (∀𝑐 ∈ 𝑉 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
77 | | r19.29 3184 |
. . . . . . . . 9
⊢
((∀𝑐 ∈
𝑉 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
78 | | 3anass 1094 |
. . . . . . . . . . 11
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
79 | 78 | biimpri 227 |
. . . . . . . . . 10
⊢ ((𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
80 | 79 | reximi 3178 |
. . . . . . . . 9
⊢
(∃𝑐 ∈
𝑉 (𝑎 ≠ 𝑏 ∧ (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
81 | 76, 77, 80 | 3syl 18 |
. . . . . . . 8
⊢
((∀𝑐 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
82 | 81 | anim2i 617 |
. . . . . . 7
⊢ ((𝑏 ∈ 𝑉 ∧ (∀𝑐 𝑎 ≠ 𝑏 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) → (𝑏 ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
83 | 82 | anassrs 468 |
. . . . . 6
⊢ (((𝑏 ∈ 𝑉 ∧ ∀𝑐 𝑎 ≠ 𝑏) ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) → (𝑏 ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
84 | 74, 83 | syl 17 |
. . . . 5
⊢ ((𝑏 ∈ (𝑉 ∖ {𝑎}) ∧ ∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → (𝑏 ∈ 𝑉 ∧ ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))) |
85 | 84 | reximi2 3175 |
. . . 4
⊢
(∃𝑏 ∈
(𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
86 | 85 | reximi 3178 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐 → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
87 | 51, 86 | sylbir 234 |
. 2
⊢
(∃𝑎(𝑎 ∈ 𝑉 ∧ ∃𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑐 ∈ (𝑉 ∖ {𝑎})𝑏 ≠ 𝑐) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |
88 | 50, 87 | syl 17 |
1
⊢ ((𝑉 ∈ 𝑊 ∧ 2 < (♯‘𝑉)) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)) |