Step | Hyp | Ref
| Expression |
1 | | 3ex 12371 |
. . . . . 6
⊢ 3 ∈
V |
2 | 1 | tpid1 4793 |
. . . . 5
⊢ 3 ∈
{3, 4, 5} |
3 | 2 | olci 865 |
. . . 4
⊢ (3 ∈
{0, 1, 2} ∨ 3 ∈ {3, 4, 5}) |
4 | | elun 4170 |
. . . 4
⊢ (3 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (3 ∈ {0, 1, 2} ∨ 3 ∈ {3, 4,
5})) |
5 | 3, 4 | mpbir 231 |
. . 3
⊢ 3 ∈
({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
⊢ (3 ∈
({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 3) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣
{3, 𝑛} ∈ ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))}) |
10 | 5, 9 | ax-mp 5 |
. 2
⊢ (𝐺 NeighbVtx 3) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {3, 𝑛} ∈
({{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 | | 4nn0 12568 |
. . . . . . 7
⊢ 4 ∈
ℕ0 |
22 | 21 | elexi 3506 |
. . . . . 6
⊢ 4 ∈
V |
23 | 22 | tpid2 4795 |
. . . . 5
⊢ 4 ∈
{3, 4, 5} |
24 | 23 | olci 865 |
. . . 4
⊢ (4 ∈
{0, 1, 2} ∨ 4 ∈ {3, 4, 5}) |
25 | | elun 4170 |
. . . 4
⊢ (4 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (4 ∈ {0, 1, 2} ∨ 4 ∈ {3, 4,
5})) |
26 | 24, 25 | mpbir 231 |
. . 3
⊢ 4 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
27 | | tpssi 4863 |
. . . 4
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2 ∈ ({0, 1, 2} ∪ {3, 4, 5})
∧ 4 ∈ ({0, 1, 2} ∪ {3, 4, 5})) → {0, 2, 4} ⊆ ({0, 1, 2}
∪ {3, 4, 5})) |
28 | | 3orass 1090 |
. . . . . 6
⊢ ((𝑛 = 0 ∨ 𝑛 = 2 ∨ 𝑛 = 4) ↔ (𝑛 = 0 ∨ (𝑛 = 2 ∨ 𝑛 = 4))) |
29 | | vex 3486 |
. . . . . . 7
⊢ 𝑛 ∈ V |
30 | 29 | eltp 4712 |
. . . . . 6
⊢ (𝑛 ∈ {0, 2, 4} ↔ (𝑛 = 0 ∨ 𝑛 = 2 ∨ 𝑛 = 4)) |
31 | | prex 5455 |
. . . . . . . 8
⊢ {3, 𝑛} ∈ V |
32 | | el7g 4713 |
. . . . . . . 8
⊢ ({3,
𝑛} ∈ V → ({3,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({3, 𝑛} = {0, 3} ∨ (({3, 𝑛} = {0, 1} ∨ {3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3}) ∨ ({3, 𝑛} = {3, 4} ∨ {3, 𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5}))))) |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
⊢ ({3,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({3, 𝑛} = {0, 3} ∨ (({3, 𝑛} = {0, 1} ∨ {3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3}) ∨ ({3, 𝑛} = {3, 4} ∨ {3, 𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5})))) |
34 | | prcom 4757 |
. . . . . . . . . 10
⊢ {0, 3} =
{3, 0} |
35 | 34 | eqeq2i 2747 |
. . . . . . . . 9
⊢ ({3,
𝑛} = {0, 3} ↔ {3,
𝑛} = {3,
0}) |
36 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ (0 ∈
V → 𝑛 ∈
V) |
37 | | elex 3504 |
. . . . . . . . . . 11
⊢ (0 ∈
V → 0 ∈ V) |
38 | 36, 37 | preq2b 4872 |
. . . . . . . . . 10
⊢ (0 ∈
V → ({3, 𝑛} = {3, 0}
↔ 𝑛 =
0)) |
39 | 11, 38 | ax-mp 5 |
. . . . . . . . 9
⊢ ({3,
𝑛} = {3, 0} ↔ 𝑛 = 0) |
40 | 35, 39 | bitri 275 |
. . . . . . . 8
⊢ ({3,
𝑛} = {0, 3} ↔ 𝑛 = 0) |
41 | | 3orrot 1092 |
. . . . . . . . . 10
⊢ (({3,
𝑛} = {0, 1} ∨ {3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3}) ↔ ({3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3} ∨ {3, 𝑛} = {0, 1})) |
42 | 1, 29 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (3 ∈
V ∧ 𝑛 ∈
V) |
43 | | 1re 11286 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
44 | 43, 16 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ ∧ 2 ∈ V) |
45 | 42, 44 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ V ∧ 𝑛 ∈ V)
∧ (1 ∈ ℝ ∧ 2 ∈ V)) |
46 | | 1lt3 12462 |
. . . . . . . . . . . . . . . . 17
⊢ 1 <
3 |
47 | 43, 46 | gtneii 11398 |
. . . . . . . . . . . . . . . 16
⊢ 3 ≠
1 |
48 | | 2re 12363 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
49 | | 2lt3 12461 |
. . . . . . . . . . . . . . . . 17
⊢ 2 <
3 |
50 | 48, 49 | gtneii 11398 |
. . . . . . . . . . . . . . . 16
⊢ 3 ≠
2 |
51 | 47, 50 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (3 ≠ 1
∧ 3 ≠ 2) |
52 | 51 | orci 864 |
. . . . . . . . . . . . . 14
⊢ ((3 ≠
1 ∧ 3 ≠ 2) ∨ (𝑛
≠ 1 ∧ 𝑛 ≠
2)) |
53 | | prneimg 4879 |
. . . . . . . . . . . . . 14
⊢ (((3
∈ V ∧ 𝑛 ∈ V)
∧ (1 ∈ ℝ ∧ 2 ∈ V)) → (((3 ≠ 1 ∧ 3 ≠ 2)
∨ (𝑛 ≠ 1 ∧ 𝑛 ≠ 2)) → {3, 𝑛} ≠ {1, 2})) |
54 | 45, 52, 53 | mp2 9 |
. . . . . . . . . . . . 13
⊢ {3, 𝑛} ≠ {1, 2} |
55 | 54 | neii 2944 |
. . . . . . . . . . . 12
⊢ ¬
{3, 𝑛} = {1,
2} |
56 | | id 22 |
. . . . . . . . . . . . 13
⊢ (¬
{3, 𝑛} = {1, 2} →
¬ {3, 𝑛} = {1,
2}) |
57 | 11, 43 | pm3.2i 470 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
V ∧ 1 ∈ ℝ) |
58 | 42, 57 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ V ∧ 𝑛 ∈ V)
∧ (0 ∈ V ∧ 1 ∈ ℝ)) |
59 | | 3ne0 12395 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ≠
0 |
60 | 59, 47 | pm3.2i 470 |
. . . . . . . . . . . . . . . . 17
⊢ (3 ≠ 0
∧ 3 ≠ 1) |
61 | 60 | orci 864 |
. . . . . . . . . . . . . . . 16
⊢ ((3 ≠
0 ∧ 3 ≠ 1) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠
1)) |
62 | | prneimg 4879 |
. . . . . . . . . . . . . . . 16
⊢ (((3
∈ V ∧ 𝑛 ∈ V)
∧ (0 ∈ V ∧ 1 ∈ ℝ)) → (((3 ≠ 0 ∧ 3 ≠ 1)
∨ (𝑛 ≠ 0 ∧ 𝑛 ≠ 1)) → {3, 𝑛} ≠ {0, 1})) |
63 | 58, 61, 62 | mp2 9 |
. . . . . . . . . . . . . . 15
⊢ {3, 𝑛} ≠ {0, 1} |
64 | 63 | neii 2944 |
. . . . . . . . . . . . . 14
⊢ ¬
{3, 𝑛} = {0,
1} |
65 | 64 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
{3, 𝑛} = {1, 2} →
¬ {3, 𝑛} = {0,
1}) |
66 | 56, 65 | 3bior2fd 1477 |
. . . . . . . . . . . 12
⊢ (¬
{3, 𝑛} = {1, 2} → ({3,
𝑛} = {2, 3} ↔ ({3,
𝑛} = {1, 2} ∨ {3, 𝑛} = {0, 1} ∨ {3, 𝑛} = {2, 3}))) |
67 | 55, 66 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ({3,
𝑛} = {2, 3} ↔ ({3,
𝑛} = {1, 2} ∨ {3, 𝑛} = {0, 1} ∨ {3, 𝑛} = {2, 3})) |
68 | | 3orcomb 1094 |
. . . . . . . . . . 11
⊢ (({3,
𝑛} = {1, 2} ∨ {3, 𝑛} = {0, 1} ∨ {3, 𝑛} = {2, 3}) ↔ ({3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3} ∨ {3, 𝑛} = {0, 1})) |
69 | 67, 68 | bitri 275 |
. . . . . . . . . 10
⊢ ({3,
𝑛} = {2, 3} ↔ ({3,
𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3} ∨ {3, 𝑛} = {0, 1})) |
70 | | prcom 4757 |
. . . . . . . . . . . 12
⊢ {2, 3} =
{3, 2} |
71 | 70 | eqeq2i 2747 |
. . . . . . . . . . 11
⊢ ({3,
𝑛} = {2, 3} ↔ {3,
𝑛} = {3,
2}) |
72 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (2 ∈
V → 𝑛 ∈
V) |
73 | | elex 3504 |
. . . . . . . . . . . . 13
⊢ (2 ∈
V → 2 ∈ V) |
74 | 72, 73 | preq2b 4872 |
. . . . . . . . . . . 12
⊢ (2 ∈
V → ({3, 𝑛} = {3, 2}
↔ 𝑛 =
2)) |
75 | 16, 74 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ({3,
𝑛} = {3, 2} ↔ 𝑛 = 2) |
76 | 71, 75 | bitri 275 |
. . . . . . . . . 10
⊢ ({3,
𝑛} = {2, 3} ↔ 𝑛 = 2) |
77 | 41, 69, 76 | 3bitr2i 299 |
. . . . . . . . 9
⊢ (({3,
𝑛} = {0, 1} ∨ {3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3}) ↔ 𝑛 = 2) |
78 | | 3orrot 1092 |
. . . . . . . . . 10
⊢ (({3,
𝑛} = {3, 4} ∨ {3, 𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5}) ↔ ({3, 𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5} ∨ {3, 𝑛} = {3, 4})) |
79 | | 5nn0 12569 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℕ0 |
80 | 21, 79 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0) |
81 | 42, 80 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ ((3
∈ V ∧ 𝑛 ∈ V)
∧ (4 ∈ ℕ0 ∧ 5 ∈
ℕ0)) |
82 | | 3re 12369 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
83 | | 3lt4 12463 |
. . . . . . . . . . . . . . . 16
⊢ 3 <
4 |
84 | 82, 83 | ltneii 11399 |
. . . . . . . . . . . . . . 15
⊢ 3 ≠
4 |
85 | | 3lt5 12467 |
. . . . . . . . . . . . . . . 16
⊢ 3 <
5 |
86 | 82, 85 | ltneii 11399 |
. . . . . . . . . . . . . . 15
⊢ 3 ≠
5 |
87 | 84, 86 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (3 ≠ 4
∧ 3 ≠ 5) |
88 | 87 | orci 864 |
. . . . . . . . . . . . 13
⊢ ((3 ≠
4 ∧ 3 ≠ 5) ∨ (𝑛
≠ 4 ∧ 𝑛 ≠
5)) |
89 | | prneimg 4879 |
. . . . . . . . . . . . 13
⊢ (((3
∈ V ∧ 𝑛 ∈ V)
∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)) →
(((3 ≠ 4 ∧ 3 ≠ 5) ∨ (𝑛 ≠ 4 ∧ 𝑛 ≠ 5)) → {3, 𝑛} ≠ {4, 5})) |
90 | 81, 88, 89 | mp2 9 |
. . . . . . . . . . . 12
⊢ {3, 𝑛} ≠ {4, 5} |
91 | 90 | neii 2944 |
. . . . . . . . . . 11
⊢ ¬
{3, 𝑛} = {4,
5} |
92 | | id 22 |
. . . . . . . . . . . 12
⊢ (¬
{3, 𝑛} = {4, 5} →
¬ {3, 𝑛} = {4,
5}) |
93 | 11, 79 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
V ∧ 5 ∈ ℕ0) |
94 | 42, 93 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ V ∧ 𝑛 ∈ V)
∧ (0 ∈ V ∧ 5 ∈ ℕ0)) |
95 | 59, 86 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (3 ≠ 0
∧ 3 ≠ 5) |
96 | 95 | orci 864 |
. . . . . . . . . . . . . . 15
⊢ ((3 ≠
0 ∧ 3 ≠ 5) ∨ (𝑛
≠ 0 ∧ 𝑛 ≠
5)) |
97 | | prneimg 4879 |
. . . . . . . . . . . . . . 15
⊢ (((3
∈ V ∧ 𝑛 ∈ V)
∧ (0 ∈ V ∧ 5 ∈ ℕ0)) → (((3 ≠ 0 ∧
3 ≠ 5) ∨ (𝑛 ≠ 0
∧ 𝑛 ≠ 5)) → {3,
𝑛} ≠ {0,
5})) |
98 | 94, 96, 97 | mp2 9 |
. . . . . . . . . . . . . 14
⊢ {3, 𝑛} ≠ {0, 5} |
99 | 98 | neii 2944 |
. . . . . . . . . . . . 13
⊢ ¬
{3, 𝑛} = {0,
5} |
100 | 99 | a1i 11 |
. . . . . . . . . . . 12
⊢ (¬
{3, 𝑛} = {4, 5} →
¬ {3, 𝑛} = {0,
5}) |
101 | 92, 100 | 3bior2fd 1477 |
. . . . . . . . . . 11
⊢ (¬
{3, 𝑛} = {4, 5} → ({3,
𝑛} = {3, 4} ↔ ({3,
𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5} ∨ {3, 𝑛} = {3, 4}))) |
102 | 91, 101 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({3,
𝑛} = {3, 4} ↔ ({3,
𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5} ∨ {3, 𝑛} = {3, 4})) |
103 | 29 | a1i 11 |
. . . . . . . . . . . 12
⊢ (4 ∈
ℕ0 → 𝑛 ∈ V) |
104 | | elex 3504 |
. . . . . . . . . . . 12
⊢ (4 ∈
ℕ0 → 4 ∈ V) |
105 | 103, 104 | preq2b 4872 |
. . . . . . . . . . 11
⊢ (4 ∈
ℕ0 → ({3, 𝑛} = {3, 4} ↔ 𝑛 = 4)) |
106 | 21, 105 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({3,
𝑛} = {3, 4} ↔ 𝑛 = 4) |
107 | 78, 102, 106 | 3bitr2i 299 |
. . . . . . . . 9
⊢ (({3,
𝑛} = {3, 4} ∨ {3, 𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5}) ↔ 𝑛 = 4) |
108 | 77, 107 | orbi12i 913 |
. . . . . . . 8
⊢ ((({3,
𝑛} = {0, 1} ∨ {3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3}) ∨ ({3, 𝑛} = {3, 4} ∨ {3, 𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5})) ↔ (𝑛 = 2 ∨ 𝑛 = 4)) |
109 | 40, 108 | orbi12i 913 |
. . . . . . 7
⊢ (({3,
𝑛} = {0, 3} ∨ (({3,
𝑛} = {0, 1} ∨ {3, 𝑛} = {1, 2} ∨ {3, 𝑛} = {2, 3}) ∨ ({3, 𝑛} = {3, 4} ∨ {3, 𝑛} = {4, 5} ∨ {3, 𝑛} = {0, 5}))) ↔ (𝑛 = 0 ∨ (𝑛 = 2 ∨ 𝑛 = 4))) |
110 | 33, 109 | bitri 275 |
. . . . . 6
⊢ ({3,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ (𝑛 = 0 ∨ (𝑛 = 2 ∨ 𝑛 = 4))) |
111 | 28, 30, 110 | 3bitr4i 303 |
. . . . 5
⊢ (𝑛 ∈ {0, 2, 4} ↔ {3,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))) |
112 | 111 | a1i 11 |
. . . 4
⊢ (((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2 ∈ ({0, 1, 2} ∪ {3, 4, 5})
∧ 4 ∈ ({0, 1, 2} ∪ {3, 4, 5})) ∧ 𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5})) →
(𝑛 ∈ {0, 2, 4} ↔
{3, 𝑛} ∈ ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})))) |
113 | 27, 112 | eqrrabd 4103 |
. . 3
⊢ ((0
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2 ∈ ({0, 1, 2} ∪ {3, 4, 5})
∧ 4 ∈ ({0, 1, 2} ∪ {3, 4, 5})) → {0, 2, 4} = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {3, 𝑛} ∈
({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))}) |
114 | 15, 20, 26, 113 | mp3an 1461 |
. 2
⊢ {0, 2, 4}
= {𝑛 ∈ ({0, 1, 2}
∪ {3, 4, 5}) ∣ {3, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2},
{2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))} |
115 | 10, 114 | eqtr4i 2765 |
1
⊢ (𝐺 NeighbVtx 3) = {0, 2,
4} |