Step | Hyp | Ref
| Expression |
1 | | 1ex 11282 |
. . . . . 6
⊢ 1 ∈
V |
2 | 1 | tpid2 4795 |
. . . . 5
⊢ 1 ∈
{0, 1, 2} |
3 | 2 | orci 864 |
. . . 4
⊢ (1 ∈
{0, 1, 2} ∨ 1 ∈ {3, 4, 5}) |
4 | | elun 4170 |
. . . 4
⊢ (1 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (1 ∈ {0, 1, 2} ∨ 1 ∈ {3, 4,
5})) |
5 | 3, 4 | mpbir 231 |
. . 3
⊢ 1 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
6 | | usgrexmpl2.v |
. . . 4
⊢ 𝑉 = (0...5) |
7 | | usgrexmpl2.e |
. . . 4
⊢ 𝐸 = 〈“{0, 1} {1, 2}
{2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 |
8 | | usgrexmpl2.g |
. . . 4
⊢ 𝐺 = 〈𝑉, 𝐸〉 |
9 | 6, 7, 8 | usgrexmpl2nblem 47765 |
. . 3
⊢ (1 ∈
({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 1) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣
{1, 𝑛} ∈ ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))}) |
10 | 5, 9 | ax-mp 5 |
. 2
⊢ (𝐺 NeighbVtx 1) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {1, 𝑛} ∈
({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))} |
11 | | c0ex 11280 |
. . . . . 6
⊢ 0 ∈
V |
12 | 11 | tpid1 4793 |
. . . . 5
⊢ 0 ∈
{0, 1, 2} |
13 | 12 | orci 864 |
. . . 4
⊢ (0 ∈
{0, 1, 2} ∨ 0 ∈ {3, 4, 5}) |
14 | | elun 4170 |
. . . 4
⊢ (0 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (0 ∈ {0, 1, 2} ∨ 0 ∈ {3, 4,
5})) |
15 | 13, 14 | mpbir 231 |
. . 3
⊢ 0 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
16 | | 2ex 12366 |
. . . . . 6
⊢ 2 ∈
V |
17 | 16 | tpid3 4798 |
. . . . 5
⊢ 2 ∈
{0, 1, 2} |
18 | 17 | orci 864 |
. . . 4
⊢ (2 ∈
{0, 1, 2} ∨ 2 ∈ {3, 4, 5}) |
19 | | elun 4170 |
. . . 4
⊢ (2 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (2 ∈ {0, 1, 2} ∨ 2 ∈ {3, 4,
5})) |
20 | 18, 19 | mpbir 231 |
. . 3
⊢ 2 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
21 | | prssi 4846 |
. . . . 5
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
→ {0, 2} ⊆ ({0, 1, 2} ∪ {3, 4, 5})) |
22 | | 1re 11286 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
23 | | vex 3486 |
. . . . . . . . . . . . . 14
⊢ 𝑛 ∈ V |
24 | 22, 23 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ ∧ 𝑛 ∈
V) |
25 | | 3ex 12371 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
V |
26 | 16, 25 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (2 ∈
V ∧ 3 ∈ V) |
27 | 24, 26 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (2 ∈ V ∧ 3 ∈ V)) |
28 | | 1ne2 12497 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
2 |
29 | | 1lt3 12462 |
. . . . . . . . . . . . . . 15
⊢ 1 <
3 |
30 | 22, 29 | ltneii 11399 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
3 |
31 | 28, 30 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (1 ≠ 2
∧ 1 ≠ 3) |
32 | 31 | orci 864 |
. . . . . . . . . . . 12
⊢ ((1 ≠
2 ∧ 1 ≠ 3) ∨ (𝑛
≠ 2 ∧ 𝑛 ≠
3)) |
33 | | prneimg 4879 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (2 ∈ V ∧ 3 ∈ V)) → (((1 ≠ 2 ∧ 1 ≠
3) ∨ (𝑛 ≠ 2 ∧
𝑛 ≠ 3)) → {1, 𝑛} ≠ {2, 3})) |
34 | 27, 32, 33 | mp2 9 |
. . . . . . . . . . 11
⊢ {1, 𝑛} ≠ {2, 3} |
35 | 34 | neii 2944 |
. . . . . . . . . 10
⊢ ¬
{1, 𝑛} = {2,
3} |
36 | 35 | biorfri 938 |
. . . . . . . . 9
⊢ (({1,
𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2}) ↔ (({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2}) ∨ {1, 𝑛} = {2, 3})) |
37 | 23 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (0 ∈
V → 𝑛 ∈
V) |
38 | | elex 3504 |
. . . . . . . . . . . . 13
⊢ (0 ∈
V → 0 ∈ V) |
39 | 37, 38 | preq2b 4872 |
. . . . . . . . . . . 12
⊢ (0 ∈
V → ({1, 𝑛} = {1, 0}
↔ 𝑛 =
0)) |
40 | 11, 39 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ({1,
𝑛} = {1, 0} ↔ 𝑛 = 0) |
41 | | prcom 4757 |
. . . . . . . . . . . 12
⊢ {1, 0} =
{0, 1} |
42 | 41 | eqeq2i 2747 |
. . . . . . . . . . 11
⊢ ({1,
𝑛} = {1, 0} ↔ {1,
𝑛} = {0,
1}) |
43 | 40, 42 | bitr3i 277 |
. . . . . . . . . 10
⊢ (𝑛 = 0 ↔ {1, 𝑛} = {0, 1}) |
44 | 23 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (2 ∈
V → 𝑛 ∈
V) |
45 | | elex 3504 |
. . . . . . . . . . . . 13
⊢ (2 ∈
V → 2 ∈ V) |
46 | 44, 45 | preq2b 4872 |
. . . . . . . . . . . 12
⊢ (2 ∈
V → ({1, 𝑛} = {1, 2}
↔ 𝑛 =
2)) |
47 | 46 | bicomd 223 |
. . . . . . . . . . 11
⊢ (2 ∈
V → (𝑛 = 2 ↔ {1,
𝑛} = {1,
2})) |
48 | 16, 47 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑛 = 2 ↔ {1, 𝑛} = {1, 2}) |
49 | 43, 48 | orbi12i 913 |
. . . . . . . . 9
⊢ ((𝑛 = 0 ∨ 𝑛 = 2) ↔ ({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2})) |
50 | | df-3or 1088 |
. . . . . . . . 9
⊢ (({1,
𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ↔ (({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2}) ∨ {1, 𝑛} = {2, 3})) |
51 | 36, 49, 50 | 3bitr4i 303 |
. . . . . . . 8
⊢ ((𝑛 = 0 ∨ 𝑛 = 2) ↔ ({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3})) |
52 | | 4nn0 12568 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℕ0 |
53 | 25, 52 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (3 ∈
V ∧ 4 ∈ ℕ0) |
54 | 24, 53 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (3 ∈ V ∧ 4 ∈
ℕ0)) |
55 | | 1lt4 12465 |
. . . . . . . . . . . . . . 15
⊢ 1 <
4 |
56 | 22, 55 | ltneii 11399 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
4 |
57 | 30, 56 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (1 ≠ 3
∧ 1 ≠ 4) |
58 | 57 | orci 864 |
. . . . . . . . . . . 12
⊢ ((1 ≠
3 ∧ 1 ≠ 4) ∨ (𝑛
≠ 3 ∧ 𝑛 ≠
4)) |
59 | | prneimg 4879 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (3 ∈ V ∧ 4 ∈ ℕ0)) → (((1
≠ 3 ∧ 1 ≠ 4) ∨ (𝑛 ≠ 3 ∧ 𝑛 ≠ 4)) → {1, 𝑛} ≠ {3, 4})) |
60 | 54, 58, 59 | mp2 9 |
. . . . . . . . . . 11
⊢ {1, 𝑛} ≠ {3, 4} |
61 | 60 | neii 2944 |
. . . . . . . . . 10
⊢ ¬
{1, 𝑛} = {3,
4} |
62 | | 5nn0 12569 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ0 |
63 | 52, 62 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0) |
64 | 24, 63 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (4 ∈ ℕ0 ∧ 5 ∈
ℕ0)) |
65 | | 1lt5 12469 |
. . . . . . . . . . . . . . 15
⊢ 1 <
5 |
66 | 22, 65 | ltneii 11399 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
5 |
67 | 56, 66 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (1 ≠ 4
∧ 1 ≠ 5) |
68 | 67 | orci 864 |
. . . . . . . . . . . 12
⊢ ((1 ≠
4 ∧ 1 ≠ 5) ∨ (𝑛
≠ 4 ∧ 𝑛 ≠
5)) |
69 | | prneimg 4879 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (4 ∈ ℕ0 ∧ 5 ∈
ℕ0)) → (((1 ≠ 4 ∧ 1 ≠ 5) ∨ (𝑛 ≠ 4 ∧ 𝑛 ≠ 5)) → {1, 𝑛} ≠ {4, 5})) |
70 | 64, 68, 69 | mp2 9 |
. . . . . . . . . . 11
⊢ {1, 𝑛} ≠ {4, 5} |
71 | 70 | neii 2944 |
. . . . . . . . . 10
⊢ ¬
{1, 𝑛} = {4,
5} |
72 | 11, 62 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (0 ∈
V ∧ 5 ∈ ℕ0) |
73 | 24, 72 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ V ∧ 5 ∈
ℕ0)) |
74 | | ax-1ne0 11249 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
0 |
75 | 74, 66 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ (1 ≠ 0
∧ 1 ≠ 5) |
76 | 75 | orci 864 |
. . . . . . . . . . . 12
⊢ ((1 ≠
0 ∧ 1 ≠ 5) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠
5)) |
77 | | prneimg 4879 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ V ∧ 5 ∈ ℕ0)) → (((1
≠ 0 ∧ 1 ≠ 5) ∨ (𝑛 ≠ 0 ∧ 𝑛 ≠ 5)) → {1, 𝑛} ≠ {0, 5})) |
78 | 73, 76, 77 | mp2 9 |
. . . . . . . . . . 11
⊢ {1, 𝑛} ≠ {0, 5} |
79 | 78 | neii 2944 |
. . . . . . . . . 10
⊢ ¬
{1, 𝑛} = {0,
5} |
80 | 61, 71, 79 | 3pm3.2ni 1487 |
. . . . . . . . 9
⊢ ¬
({1, 𝑛} = {3, 4} ∨ {1,
𝑛} = {4, 5} ∨ {1, 𝑛} = {0, 5}) |
81 | 80 | biorfri 938 |
. . . . . . . 8
⊢ (({1,
𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ↔ (({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ∨ ({1, 𝑛} = {3, 4} ∨ {1, 𝑛} = {4, 5} ∨ {1, 𝑛} = {0, 5}))) |
82 | 11, 25 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (0 ∈
V ∧ 3 ∈ V) |
83 | 24, 82 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ V ∧ 3 ∈ V)) |
84 | 74, 30 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (1 ≠ 0
∧ 1 ≠ 3) |
85 | 84 | orci 864 |
. . . . . . . . . . 11
⊢ ((1 ≠
0 ∧ 1 ≠ 3) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠
3)) |
86 | | prneimg 4879 |
. . . . . . . . . . 11
⊢ (((1
∈ ℝ ∧ 𝑛
∈ V) ∧ (0 ∈ V ∧ 3 ∈ V)) → (((1 ≠ 0 ∧ 1 ≠
3) ∨ (𝑛 ≠ 0 ∧
𝑛 ≠ 3)) → {1, 𝑛} ≠ {0, 3})) |
87 | 83, 85, 86 | mp2 9 |
. . . . . . . . . 10
⊢ {1, 𝑛} ≠ {0, 3} |
88 | 87 | neii 2944 |
. . . . . . . . 9
⊢ ¬
{1, 𝑛} = {0,
3} |
89 | 88 | biorfi 937 |
. . . . . . . 8
⊢ ((({1,
𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ∨ ({1, 𝑛} = {3, 4} ∨ {1, 𝑛} = {4, 5} ∨ {1, 𝑛} = {0, 5})) ↔ ({1, 𝑛} = {0, 3} ∨ (({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ∨ ({1, 𝑛} = {3, 4} ∨ {1, 𝑛} = {4, 5} ∨ {1, 𝑛} = {0, 5})))) |
90 | 51, 81, 89 | 3bitri 297 |
. . . . . . 7
⊢ ((𝑛 = 0 ∨ 𝑛 = 2) ↔ ({1, 𝑛} = {0, 3} ∨ (({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ∨ ({1, 𝑛} = {3, 4} ∨ {1, 𝑛} = {4, 5} ∨ {1, 𝑛} = {0, 5})))) |
91 | 23 | elpr 4672 |
. . . . . . 7
⊢ (𝑛 ∈ {0, 2} ↔ (𝑛 = 0 ∨ 𝑛 = 2)) |
92 | | prex 5455 |
. . . . . . . 8
⊢ {1, 𝑛} ∈ V |
93 | | el7g 4713 |
. . . . . . . 8
⊢ ({1,
𝑛} ∈ V → ({1,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({1, 𝑛} = {0, 3} ∨ (({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ∨ ({1, 𝑛} = {3, 4} ∨ {1, 𝑛} = {4, 5} ∨ {1, 𝑛} = {0, 5}))))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . 7
⊢ ({1,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({1, 𝑛} = {0, 3} ∨ (({1, 𝑛} = {0, 1} ∨ {1, 𝑛} = {1, 2} ∨ {1, 𝑛} = {2, 3}) ∨ ({1, 𝑛} = {3, 4} ∨ {1, 𝑛} = {4, 5} ∨ {1, 𝑛} = {0, 5})))) |
95 | 90, 91, 94 | 3bitr4i 303 |
. . . . . 6
⊢ (𝑛 ∈ {0, 2} ↔ {1, 𝑛} ∈ ({{0, 3}} ∪ ({{0,
1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))) |
96 | 95 | a1i 11 |
. . . . 5
⊢ (((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
∧ 𝑛 ∈ ({0, 1, 2}
∪ {3, 4, 5})) → (𝑛
∈ {0, 2} ↔ {1, 𝑛}
∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})))) |
97 | 21, 96 | eqrrabd 4103 |
. . . 4
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
→ {0, 2} = {𝑛 ∈
({0, 1, 2} ∪ {3, 4, 5}) ∣ {1, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2},
{2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))}) |
98 | 97 | eqcomd 2740 |
. . 3
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2 ∈ ({0, 1, 2} ∪ {3, 4, 5}))
→ {𝑛 ∈ ({0, 1, 2}
∪ {3, 4, 5}) ∣ {1, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2},
{2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))} = {0, 2}) |
99 | 15, 20, 98 | mp2an 691 |
. 2
⊢ {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {1, 𝑛} ∈
({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))} =
{0, 2} |
100 | 10, 99 | eqtri 2762 |
1
⊢ (𝐺 NeighbVtx 1) = {0,
2} |