Step | Hyp | Ref
| Expression |
1 | | 5re 12376 |
. . . . . . 7
⊢ 5 ∈
ℝ |
2 | 1 | elexi 3506 |
. . . . . 6
⊢ 5 ∈
V |
3 | 2 | tpid3 4798 |
. . . . 5
⊢ 5 ∈
{3, 4, 5} |
4 | 3 | olci 865 |
. . . 4
⊢ (5 ∈
{0, 1, 2} ∨ 5 ∈ {3, 4, 5}) |
5 | | elun 4170 |
. . . 4
⊢ (5 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (5 ∈ {0, 1, 2} ∨ 5 ∈ {3, 4,
5})) |
6 | 4, 5 | mpbir 231 |
. . 3
⊢ 5 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
7 | | usgrexmpl2.v |
. . . 4
⊢ 𝑉 = (0...5) |
8 | | usgrexmpl2.e |
. . . 4
⊢ 𝐸 = 〈“{0, 1} {1, 2}
{2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 |
9 | | usgrexmpl2.g |
. . . 4
⊢ 𝐺 = 〈𝑉, 𝐸〉 |
10 | 7, 8, 9 | usgrexmpl2nblem 47765 |
. . 3
⊢ (5 ∈
({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 5) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣
{5, 𝑛} ∈ ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))}) |
11 | 6, 10 | ax-mp 5 |
. 2
⊢ (𝐺 NeighbVtx 5) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {5, 𝑛} ∈
({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))} |
12 | | c0ex 11280 |
. . . . . 6
⊢ 0 ∈
V |
13 | 12 | tpid1 4793 |
. . . . 5
⊢ 0 ∈
{0, 1, 2} |
14 | 13 | orci 864 |
. . . 4
⊢ (0 ∈
{0, 1, 2} ∨ 0 ∈ {3, 4, 5}) |
15 | | elun 4170 |
. . . 4
⊢ (0 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (0 ∈ {0, 1, 2} ∨ 0 ∈ {3, 4,
5})) |
16 | 14, 15 | mpbir 231 |
. . 3
⊢ 0 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
17 | | 4re 12373 |
. . . . . . 7
⊢ 4 ∈
ℝ |
18 | 17 | elexi 3506 |
. . . . . 6
⊢ 4 ∈
V |
19 | 18 | tpid2 4795 |
. . . . 5
⊢ 4 ∈
{3, 4, 5} |
20 | 19 | olci 865 |
. . . 4
⊢ (4 ∈
{0, 1, 2} ∨ 4 ∈ {3, 4, 5}) |
21 | | elun 4170 |
. . . 4
⊢ (4 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (4 ∈ {0, 1, 2} ∨ 4 ∈ {3, 4,
5})) |
22 | 20, 21 | mpbir 231 |
. . 3
⊢ 4 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
23 | | prssi 4846 |
. . . . 5
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 4 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
→ {0, 4} ⊆ ({0, 1, 2} ∪ {3, 4, 5})) |
24 | | vex 3486 |
. . . . . . . . . . . . . . 15
⊢ 𝑛 ∈ V |
25 | 1, 24 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (5 ∈
ℝ ∧ 𝑛 ∈
V) |
26 | | 3re 12369 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ |
27 | 26, 17 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℝ ∧ 4 ∈ ℝ) |
28 | 25, 27 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ ((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (3 ∈ ℝ ∧ 4 ∈ ℝ)) |
29 | | 3lt5 12467 |
. . . . . . . . . . . . . . . 16
⊢ 3 <
5 |
30 | 26, 29 | gtneii 11398 |
. . . . . . . . . . . . . . 15
⊢ 5 ≠
3 |
31 | | 4lt5 12466 |
. . . . . . . . . . . . . . . 16
⊢ 4 <
5 |
32 | 17, 31 | gtneii 11398 |
. . . . . . . . . . . . . . 15
⊢ 5 ≠
4 |
33 | 30, 32 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (5 ≠ 3
∧ 5 ≠ 4) |
34 | 33 | orci 864 |
. . . . . . . . . . . . 13
⊢ ((5 ≠
3 ∧ 5 ≠ 4) ∨ (𝑛
≠ 3 ∧ 𝑛 ≠
4)) |
35 | | prneimg 4879 |
. . . . . . . . . . . . 13
⊢ (((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (3 ∈ ℝ ∧ 4 ∈ ℝ)) → (((5 ≠ 3
∧ 5 ≠ 4) ∨ (𝑛
≠ 3 ∧ 𝑛 ≠ 4))
→ {5, 𝑛} ≠ {3,
4})) |
36 | 28, 34, 35 | mp2 9 |
. . . . . . . . . . . 12
⊢ {5, 𝑛} ≠ {3, 4} |
37 | 36 | neii 2944 |
. . . . . . . . . . 11
⊢ ¬
{5, 𝑛} = {3,
4} |
38 | 37 | biorfi 937 |
. . . . . . . . . 10
⊢ (({5,
𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}) ↔ ({5, 𝑛} = {3, 4} ∨ ({5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}))) |
39 | | orcom 869 |
. . . . . . . . . . 11
⊢ ((𝑛 = 0 ∨ 𝑛 = 4) ↔ (𝑛 = 4 ∨ 𝑛 = 0)) |
40 | | prcom 4757 |
. . . . . . . . . . . . . 14
⊢ {4, 5} =
{5, 4} |
41 | 40 | eqeq2i 2747 |
. . . . . . . . . . . . 13
⊢ ({5,
𝑛} = {4, 5} ↔ {5,
𝑛} = {5,
4}) |
42 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (4 ∈
ℝ → 𝑛 ∈
V) |
43 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (4 ∈
ℝ → 4 ∈ ℝ) |
44 | 42, 43 | preq2b 4872 |
. . . . . . . . . . . . . 14
⊢ (4 ∈
ℝ → ({5, 𝑛} =
{5, 4} ↔ 𝑛 =
4)) |
45 | 17, 44 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ({5,
𝑛} = {5, 4} ↔ 𝑛 = 4) |
46 | 41, 45 | bitr2i 276 |
. . . . . . . . . . . 12
⊢ (𝑛 = 4 ↔ {5, 𝑛} = {4, 5}) |
47 | | prcom 4757 |
. . . . . . . . . . . . . 14
⊢ {0, 5} =
{5, 0} |
48 | 47 | eqeq2i 2747 |
. . . . . . . . . . . . 13
⊢ ({5,
𝑛} = {0, 5} ↔ {5,
𝑛} = {5,
0}) |
49 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → 𝑛 ∈
V) |
50 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V → 0 ∈ V) |
51 | 49, 50 | preq2b 4872 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
V → ({5, 𝑛} = {5, 0}
↔ 𝑛 =
0)) |
52 | 12, 51 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ({5,
𝑛} = {5, 0} ↔ 𝑛 = 0) |
53 | 48, 52 | bitr2i 276 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 ↔ {5, 𝑛} = {0, 5}) |
54 | 46, 53 | orbi12i 913 |
. . . . . . . . . . 11
⊢ ((𝑛 = 4 ∨ 𝑛 = 0) ↔ ({5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5})) |
55 | 39, 54 | bitri 275 |
. . . . . . . . . 10
⊢ ((𝑛 = 0 ∨ 𝑛 = 4) ↔ ({5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5})) |
56 | | 3orass 1090 |
. . . . . . . . . 10
⊢ (({5,
𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}) ↔ ({5, 𝑛} = {3, 4} ∨ ({5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}))) |
57 | 38, 55, 56 | 3bitr4i 303 |
. . . . . . . . 9
⊢ ((𝑛 = 0 ∨ 𝑛 = 4) ↔ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5})) |
58 | | 0re 11288 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
59 | | 1re 11286 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
60 | 58, 59 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
ℝ ∧ 1 ∈ ℝ) |
61 | 25, 60 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ ((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ ℝ ∧ 1 ∈ ℝ)) |
62 | | 5pos 12398 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
5 |
63 | 58, 62 | gtneii 11398 |
. . . . . . . . . . . . . . 15
⊢ 5 ≠
0 |
64 | | 1lt5 12469 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
5 |
65 | 59, 64 | gtneii 11398 |
. . . . . . . . . . . . . . 15
⊢ 5 ≠
1 |
66 | 63, 65 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (5 ≠ 0
∧ 5 ≠ 1) |
67 | 66 | orci 864 |
. . . . . . . . . . . . 13
⊢ ((5 ≠
0 ∧ 5 ≠ 1) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠
1)) |
68 | | prneimg 4879 |
. . . . . . . . . . . . 13
⊢ (((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ ℝ ∧ 1 ∈ ℝ)) → (((5 ≠ 0
∧ 5 ≠ 1) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠ 1))
→ {5, 𝑛} ≠ {0,
1})) |
69 | 61, 67, 68 | mp2 9 |
. . . . . . . . . . . 12
⊢ {5, 𝑛} ≠ {0, 1} |
70 | 69 | neii 2944 |
. . . . . . . . . . 11
⊢ ¬
{5, 𝑛} = {0,
1} |
71 | | 2re 12363 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
72 | 59, 71 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℝ ∧ 2 ∈ ℝ) |
73 | 25, 72 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ ((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (1 ∈ ℝ ∧ 2 ∈ ℝ)) |
74 | | 2lt5 12468 |
. . . . . . . . . . . . . . . 16
⊢ 2 <
5 |
75 | 71, 74 | gtneii 11398 |
. . . . . . . . . . . . . . 15
⊢ 5 ≠
2 |
76 | 65, 75 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (5 ≠ 1
∧ 5 ≠ 2) |
77 | 76 | orci 864 |
. . . . . . . . . . . . 13
⊢ ((5 ≠
1 ∧ 5 ≠ 2) ∨ (𝑛
≠ 1 ∧ 𝑛 ≠
2)) |
78 | | prneimg 4879 |
. . . . . . . . . . . . 13
⊢ (((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (1 ∈ ℝ ∧ 2 ∈ ℝ)) → (((5 ≠ 1
∧ 5 ≠ 2) ∨ (𝑛
≠ 1 ∧ 𝑛 ≠ 2))
→ {5, 𝑛} ≠ {1,
2})) |
79 | 73, 77, 78 | mp2 9 |
. . . . . . . . . . . 12
⊢ {5, 𝑛} ≠ {1, 2} |
80 | 79 | neii 2944 |
. . . . . . . . . . 11
⊢ ¬
{5, 𝑛} = {1,
2} |
81 | 71, 26 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ ∧ 3 ∈ ℝ) |
82 | 25, 81 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ ((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (2 ∈ ℝ ∧ 3 ∈ ℝ)) |
83 | 75, 30 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (5 ≠ 2
∧ 5 ≠ 3) |
84 | 83 | orci 864 |
. . . . . . . . . . . . 13
⊢ ((5 ≠
2 ∧ 5 ≠ 3) ∨ (𝑛
≠ 2 ∧ 𝑛 ≠
3)) |
85 | | prneimg 4879 |
. . . . . . . . . . . . 13
⊢ (((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (2 ∈ ℝ ∧ 3 ∈ ℝ)) → (((5 ≠ 2
∧ 5 ≠ 3) ∨ (𝑛
≠ 2 ∧ 𝑛 ≠ 3))
→ {5, 𝑛} ≠ {2,
3})) |
86 | 82, 84, 85 | mp2 9 |
. . . . . . . . . . . 12
⊢ {5, 𝑛} ≠ {2, 3} |
87 | 86 | neii 2944 |
. . . . . . . . . . 11
⊢ ¬
{5, 𝑛} = {2,
3} |
88 | 70, 80, 87 | 3pm3.2ni 1487 |
. . . . . . . . . 10
⊢ ¬
({5, 𝑛} = {0, 1} ∨ {5,
𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) |
89 | 88 | biorfi 937 |
. . . . . . . . 9
⊢ (({5,
𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}) ↔ (({5, 𝑛} = {0, 1} ∨ {5, 𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) ∨ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}))) |
90 | 57, 89 | bitri 275 |
. . . . . . . 8
⊢ ((𝑛 = 0 ∨ 𝑛 = 4) ↔ (({5, 𝑛} = {0, 1} ∨ {5, 𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) ∨ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}))) |
91 | 58, 26 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℝ ∧ 3 ∈ ℝ) |
92 | 25, 91 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ ((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ ℝ ∧ 3 ∈ ℝ)) |
93 | 63, 30 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (5 ≠ 0
∧ 5 ≠ 3) |
94 | 93 | orci 864 |
. . . . . . . . . . 11
⊢ ((5 ≠
0 ∧ 5 ≠ 3) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠
3)) |
95 | | prneimg 4879 |
. . . . . . . . . . 11
⊢ (((5
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ ℝ ∧ 3 ∈ ℝ)) → (((5 ≠ 0
∧ 5 ≠ 3) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠ 3))
→ {5, 𝑛} ≠ {0,
3})) |
96 | 92, 94, 95 | mp2 9 |
. . . . . . . . . 10
⊢ {5, 𝑛} ≠ {0, 3} |
97 | 96 | neii 2944 |
. . . . . . . . 9
⊢ ¬
{5, 𝑛} = {0,
3} |
98 | 97 | biorfi 937 |
. . . . . . . 8
⊢ ((({5,
𝑛} = {0, 1} ∨ {5, 𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) ∨ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5})) ↔ ({5, 𝑛} = {0, 3} ∨ (({5, 𝑛} = {0, 1} ∨ {5, 𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) ∨ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5})))) |
99 | 90, 98 | bitri 275 |
. . . . . . 7
⊢ ((𝑛 = 0 ∨ 𝑛 = 4) ↔ ({5, 𝑛} = {0, 3} ∨ (({5, 𝑛} = {0, 1} ∨ {5, 𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) ∨ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5})))) |
100 | 24 | elpr 4672 |
. . . . . . 7
⊢ (𝑛 ∈ {0, 4} ↔ (𝑛 = 0 ∨ 𝑛 = 4)) |
101 | | prex 5455 |
. . . . . . . 8
⊢ {5, 𝑛} ∈ V |
102 | | el7g 4713 |
. . . . . . . 8
⊢ ({5,
𝑛} ∈ V → ({5,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({5, 𝑛} = {0, 3} ∨ (({5, 𝑛} = {0, 1} ∨ {5, 𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) ∨ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5}))))) |
103 | 101, 102 | ax-mp 5 |
. . . . . . 7
⊢ ({5,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({5, 𝑛} = {0, 3} ∨ (({5, 𝑛} = {0, 1} ∨ {5, 𝑛} = {1, 2} ∨ {5, 𝑛} = {2, 3}) ∨ ({5, 𝑛} = {3, 4} ∨ {5, 𝑛} = {4, 5} ∨ {5, 𝑛} = {0, 5})))) |
104 | 99, 100, 103 | 3bitr4i 303 |
. . . . . 6
⊢ (𝑛 ∈ {0, 4} ↔ {5, 𝑛} ∈ ({{0, 3}} ∪ ({{0,
1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))) |
105 | 104 | a1i 11 |
. . . . 5
⊢ (((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 4 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
∧ 𝑛 ∈ ({0, 1, 2}
∪ {3, 4, 5})) → (𝑛
∈ {0, 4} ↔ {5, 𝑛}
∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})))) |
106 | 23, 105 | eqrrabd 4103 |
. . . 4
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 4 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
→ {0, 4} = {𝑛 ∈
({0, 1, 2} ∪ {3, 4, 5}) ∣ {5, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2},
{2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))}) |
107 | 106 | eqcomd 2740 |
. . 3
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 4 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
→ {𝑛 ∈ ({0, 1, 2}
∪ {3, 4, 5}) ∣ {5, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2},
{2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))} = {0, 4}) |
108 | 16, 22, 107 | mp2an 691 |
. 2
⊢ {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {5, 𝑛} ∈
({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))} =
{0, 4} |
109 | 11, 108 | eqtri 2762 |
1
⊢ (𝐺 NeighbVtx 5) = {0,
4} |