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