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