Step | Hyp | Ref
| Expression |
1 | | c0ex 11280 |
. . . . . 6
⊢ 0 ∈
V |
2 | 1 | tpid1 4793 |
. . . . 5
⊢ 0 ∈
{0, 1, 2} |
3 | 2 | orci 864 |
. . . 4
⊢ (0 ∈
{0, 1, 2} ∨ 0 ∈ {3, 4, 5}) |
4 | | elun 4170 |
. . . 4
⊢ (0 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (0 ∈ {0, 1, 2} ∨ 0 ∈ {3, 4,
5})) |
5 | 3, 4 | mpbir 231 |
. . 3
⊢ 0 ∈
({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
⊢ (0 ∈
({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 0) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣
{0, 𝑛} ∈ ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))}) |
10 | 5, 9 | ax-mp 5 |
. 2
⊢ (𝐺 NeighbVtx 0) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {0, 𝑛} ∈
({{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 | | 5nn0 12569 |
. . . . . . 7
⊢ 5 ∈
ℕ0 |
22 | 21 | elexi 3506 |
. . . . . 6
⊢ 5 ∈
V |
23 | 22 | tpid3 4798 |
. . . . 5
⊢ 5 ∈
{3, 4, 5} |
24 | 23 | olci 865 |
. . . 4
⊢ (5 ∈
{0, 1, 2} ∨ 5 ∈ {3, 4, 5}) |
25 | | elun 4170 |
. . . 4
⊢ (5 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (5 ∈ {0, 1, 2} ∨ 5 ∈ {3, 4,
5})) |
26 | 24, 25 | mpbir 231 |
. . 3
⊢ 5 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
27 | | tpssi 4863 |
. . . 4
⊢ ((1
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 3 ∈ ({0, 1, 2} ∪ {3, 4, 5})
∧ 5 ∈ ({0, 1, 2} ∪ {3, 4, 5})) → {1, 3, 5} ⊆ ({0, 1, 2}
∪ {3, 4, 5})) |
28 | | 3orcoma 1093 |
. . . . . . 7
⊢ ((𝑛 = 3 ∨ 𝑛 = 1 ∨ 𝑛 = 5) ↔ (𝑛 = 1 ∨ 𝑛 = 3 ∨ 𝑛 = 5)) |
29 | | 3orass 1090 |
. . . . . . 7
⊢ ((𝑛 = 3 ∨ 𝑛 = 1 ∨ 𝑛 = 5) ↔ (𝑛 = 3 ∨ (𝑛 = 1 ∨ 𝑛 = 5))) |
30 | 28, 29 | bitr3i 277 |
. . . . . 6
⊢ ((𝑛 = 1 ∨ 𝑛 = 3 ∨ 𝑛 = 5) ↔ (𝑛 = 3 ∨ (𝑛 = 1 ∨ 𝑛 = 5))) |
31 | | vex 3486 |
. . . . . . 7
⊢ 𝑛 ∈ V |
32 | 31 | eltp 4712 |
. . . . . 6
⊢ (𝑛 ∈ {1, 3, 5} ↔ (𝑛 = 1 ∨ 𝑛 = 3 ∨ 𝑛 = 5)) |
33 | | prex 5455 |
. . . . . . . 8
⊢ {0, 𝑛} ∈ V |
34 | | el7g 4713 |
. . . . . . . 8
⊢ ({0,
𝑛} ∈ V → ({0,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({0, 𝑛} = {0, 3} ∨ (({0, 𝑛} = {0, 1} ∨ {0, 𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3}) ∨ ({0, 𝑛} = {3, 4} ∨ {0, 𝑛} = {4, 5} ∨ {0, 𝑛} = {0, 5}))))) |
35 | 33, 34 | ax-mp 5 |
. . . . . . 7
⊢ ({0,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ ({0, 𝑛} = {0, 3} ∨ (({0, 𝑛} = {0, 1} ∨ {0, 𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3}) ∨ ({0, 𝑛} = {3, 4} ∨ {0, 𝑛} = {4, 5} ∨ {0, 𝑛} = {0, 5})))) |
36 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ (3 ∈
V → 𝑛 ∈
V) |
37 | | elex 3504 |
. . . . . . . . . 10
⊢ (3 ∈
V → 3 ∈ V) |
38 | 36, 37 | preq2b 4872 |
. . . . . . . . 9
⊢ (3 ∈
V → ({0, 𝑛} = {0, 3}
↔ 𝑛 =
3)) |
39 | 16, 38 | ax-mp 5 |
. . . . . . . 8
⊢ ({0,
𝑛} = {0, 3} ↔ 𝑛 = 3) |
40 | | 3orrot 1092 |
. . . . . . . . . 10
⊢ (({0,
𝑛} = {0, 1} ∨ {0, 𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3}) ↔ ({0, 𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3} ∨ {0, 𝑛} = {0, 1})) |
41 | 1, 31 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
V ∧ 𝑛 ∈
V) |
42 | | 2ex 12366 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
V |
43 | 11, 42 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
V ∧ 2 ∈ V) |
44 | 41, 43 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ V ∧ 𝑛 ∈ V)
∧ (1 ∈ V ∧ 2 ∈ V)) |
45 | | 0ne1 12360 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≠
1 |
46 | | 0ne2 12496 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≠
2 |
47 | 45, 46 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (0 ≠ 1
∧ 0 ≠ 2) |
48 | 47 | orci 864 |
. . . . . . . . . . . . . 14
⊢ ((0 ≠
1 ∧ 0 ≠ 2) ∨ (𝑛
≠ 1 ∧ 𝑛 ≠
2)) |
49 | | prneimg 4879 |
. . . . . . . . . . . . . 14
⊢ (((0
∈ V ∧ 𝑛 ∈ V)
∧ (1 ∈ V ∧ 2 ∈ V)) → (((0 ≠ 1 ∧ 0 ≠ 2) ∨
(𝑛 ≠ 1 ∧ 𝑛 ≠ 2)) → {0, 𝑛} ≠ {1, 2})) |
50 | 44, 48, 49 | mp2 9 |
. . . . . . . . . . . . 13
⊢ {0, 𝑛} ≠ {1, 2} |
51 | 50 | neii 2944 |
. . . . . . . . . . . 12
⊢ ¬
{0, 𝑛} = {1,
2} |
52 | | id 22 |
. . . . . . . . . . . . 13
⊢ (¬
{0, 𝑛} = {1, 2} →
¬ {0, 𝑛} = {1,
2}) |
53 | 42, 16 | pm3.2i 470 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
V ∧ 3 ∈ V) |
54 | 41, 53 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ V ∧ 𝑛 ∈ V)
∧ (2 ∈ V ∧ 3 ∈ V)) |
55 | | 0re 11288 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
56 | | 3pos 12394 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 <
3 |
57 | 55, 56 | ltneii 11399 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≠
3 |
58 | 46, 57 | pm3.2i 470 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ≠ 2
∧ 0 ≠ 3) |
59 | 58 | orci 864 |
. . . . . . . . . . . . . . . 16
⊢ ((0 ≠
2 ∧ 0 ≠ 3) ∨ (𝑛
≠ 2 ∧ 𝑛 ≠
3)) |
60 | | prneimg 4879 |
. . . . . . . . . . . . . . . 16
⊢ (((0
∈ V ∧ 𝑛 ∈ V)
∧ (2 ∈ V ∧ 3 ∈ V)) → (((0 ≠ 2 ∧ 0 ≠ 3) ∨
(𝑛 ≠ 2 ∧ 𝑛 ≠ 3)) → {0, 𝑛} ≠ {2, 3})) |
61 | 54, 59, 60 | mp2 9 |
. . . . . . . . . . . . . . 15
⊢ {0, 𝑛} ≠ {2, 3} |
62 | 61 | neii 2944 |
. . . . . . . . . . . . . 14
⊢ ¬
{0, 𝑛} = {2,
3} |
63 | 62 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (¬
{0, 𝑛} = {1, 2} →
¬ {0, 𝑛} = {2,
3}) |
64 | 52, 63 | 3bior2fd 1477 |
. . . . . . . . . . . 12
⊢ (¬
{0, 𝑛} = {1, 2} → ({0,
𝑛} = {0, 1} ↔ ({0,
𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3} ∨ {0, 𝑛} = {0, 1}))) |
65 | 51, 64 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ({0,
𝑛} = {0, 1} ↔ ({0,
𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3} ∨ {0, 𝑛} = {0, 1})) |
66 | 31 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (1 ∈
V → 𝑛 ∈
V) |
67 | | elex 3504 |
. . . . . . . . . . . . 13
⊢ (1 ∈
V → 1 ∈ V) |
68 | 66, 67 | preq2b 4872 |
. . . . . . . . . . . 12
⊢ (1 ∈
V → ({0, 𝑛} = {0, 1}
↔ 𝑛 =
1)) |
69 | 11, 68 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ({0,
𝑛} = {0, 1} ↔ 𝑛 = 1) |
70 | 65, 69 | bitr3i 277 |
. . . . . . . . . 10
⊢ (({0,
𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3} ∨ {0, 𝑛} = {0, 1}) ↔ 𝑛 = 1) |
71 | 40, 70 | bitri 275 |
. . . . . . . . 9
⊢ (({0,
𝑛} = {0, 1} ∨ {0, 𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3}) ↔ 𝑛 = 1) |
72 | | 4nn0 12568 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℕ0 |
73 | 16, 72 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
V ∧ 4 ∈ ℕ0) |
74 | 41, 73 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢ ((0
∈ V ∧ 𝑛 ∈ V)
∧ (3 ∈ V ∧ 4 ∈ ℕ0)) |
75 | | 4pos 12396 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
4 |
76 | 55, 75 | ltneii 11399 |
. . . . . . . . . . . . . . 15
⊢ 0 ≠
4 |
77 | 57, 76 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (0 ≠ 3
∧ 0 ≠ 4) |
78 | 77 | orci 864 |
. . . . . . . . . . . . 13
⊢ ((0 ≠
3 ∧ 0 ≠ 4) ∨ (𝑛
≠ 3 ∧ 𝑛 ≠
4)) |
79 | | prneimg 4879 |
. . . . . . . . . . . . 13
⊢ (((0
∈ V ∧ 𝑛 ∈ V)
∧ (3 ∈ V ∧ 4 ∈ ℕ0)) → (((0 ≠ 3 ∧
0 ≠ 4) ∨ (𝑛 ≠ 3
∧ 𝑛 ≠ 4)) → {0,
𝑛} ≠ {3,
4})) |
80 | 74, 78, 79 | mp2 9 |
. . . . . . . . . . . 12
⊢ {0, 𝑛} ≠ {3, 4} |
81 | 80 | neii 2944 |
. . . . . . . . . . 11
⊢ ¬
{0, 𝑛} = {3,
4} |
82 | | id 22 |
. . . . . . . . . . . 12
⊢ (¬
{0, 𝑛} = {3, 4} →
¬ {0, 𝑛} = {3,
4}) |
83 | 72, 21 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0) |
84 | 41, 83 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ V ∧ 𝑛 ∈ V)
∧ (4 ∈ ℕ0 ∧ 5 ∈
ℕ0)) |
85 | | 5pos 12398 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
5 |
86 | 55, 85 | ltneii 11399 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ≠
5 |
87 | 76, 86 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (0 ≠ 4
∧ 0 ≠ 5) |
88 | 87 | orci 864 |
. . . . . . . . . . . . . . 15
⊢ ((0 ≠
4 ∧ 0 ≠ 5) ∨ (𝑛
≠ 4 ∧ 𝑛 ≠
5)) |
89 | | prneimg 4879 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ V ∧ 𝑛 ∈ V)
∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)) →
(((0 ≠ 4 ∧ 0 ≠ 5) ∨ (𝑛 ≠ 4 ∧ 𝑛 ≠ 5)) → {0, 𝑛} ≠ {4, 5})) |
90 | 84, 88, 89 | mp2 9 |
. . . . . . . . . . . . . 14
⊢ {0, 𝑛} ≠ {4, 5} |
91 | 90 | neii 2944 |
. . . . . . . . . . . . 13
⊢ ¬
{0, 𝑛} = {4,
5} |
92 | 91 | a1i 11 |
. . . . . . . . . . . 12
⊢ (¬
{0, 𝑛} = {3, 4} →
¬ {0, 𝑛} = {4,
5}) |
93 | 82, 92 | 3bior2fd 1477 |
. . . . . . . . . . 11
⊢ (¬
{0, 𝑛} = {3, 4} → ({0,
𝑛} = {0, 5} ↔ ({0,
𝑛} = {3, 4} ∨ {0, 𝑛} = {4, 5} ∨ {0, 𝑛} = {0, 5}))) |
94 | 81, 93 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({0,
𝑛} = {0, 5} ↔ ({0,
𝑛} = {3, 4} ∨ {0, 𝑛} = {4, 5} ∨ {0, 𝑛} = {0, 5})) |
95 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ (5 ∈
ℕ0 → 𝑛 ∈ V) |
96 | | elex 3504 |
. . . . . . . . . . . 12
⊢ (5 ∈
ℕ0 → 5 ∈ V) |
97 | 95, 96 | preq2b 4872 |
. . . . . . . . . . 11
⊢ (5 ∈
ℕ0 → ({0, 𝑛} = {0, 5} ↔ 𝑛 = 5)) |
98 | 21, 97 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({0,
𝑛} = {0, 5} ↔ 𝑛 = 5) |
99 | 94, 98 | bitr3i 277 |
. . . . . . . . 9
⊢ (({0,
𝑛} = {3, 4} ∨ {0, 𝑛} = {4, 5} ∨ {0, 𝑛} = {0, 5}) ↔ 𝑛 = 5) |
100 | 71, 99 | orbi12i 913 |
. . . . . . . 8
⊢ ((({0,
𝑛} = {0, 1} ∨ {0, 𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3}) ∨ ({0, 𝑛} = {3, 4} ∨ {0, 𝑛} = {4, 5} ∨ {0, 𝑛} = {0, 5})) ↔ (𝑛 = 1 ∨ 𝑛 = 5)) |
101 | 39, 100 | orbi12i 913 |
. . . . . . 7
⊢ (({0,
𝑛} = {0, 3} ∨ (({0,
𝑛} = {0, 1} ∨ {0, 𝑛} = {1, 2} ∨ {0, 𝑛} = {2, 3}) ∨ ({0, 𝑛} = {3, 4} ∨ {0, 𝑛} = {4, 5} ∨ {0, 𝑛} = {0, 5}))) ↔ (𝑛 = 3 ∨ (𝑛 = 1 ∨ 𝑛 = 5))) |
102 | 35, 101 | bitri 275 |
. . . . . 6
⊢ ({0,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) ↔ (𝑛 = 3 ∨ (𝑛 = 1 ∨ 𝑛 = 5))) |
103 | 30, 32, 102 | 3bitr4i 303 |
. . . . 5
⊢ (𝑛 ∈ {1, 3, 5} ↔ {0,
𝑛} ∈ ({{0, 3}} ∪
({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))) |
104 | 103 | a1i 11 |
. . . 4
⊢ (((1
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 3 ∈ ({0, 1, 2} ∪ {3, 4, 5})
∧ 5 ∈ ({0, 1, 2} ∪ {3, 4, 5})) ∧ 𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5})) →
(𝑛 ∈ {1, 3, 5} ↔
{0, 𝑛} ∈ ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})))) |
105 | 27, 104 | eqrrabd 4103 |
. . 3
⊢ ((1
∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 3 ∈ ({0, 1, 2} ∪ {3, 4, 5})
∧ 5 ∈ ({0, 1, 2} ∪ {3, 4, 5})) → {1, 3, 5} = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4,
5}) ∣ {0, 𝑛} ∈
({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}))}) |
106 | 15, 20, 26, 105 | mp3an 1461 |
. 2
⊢ {1, 3, 5}
= {𝑛 ∈ ({0, 1, 2}
∪ {3, 4, 5}) ∣ {0, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2},
{2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))} |
107 | 10, 106 | eqtr4i 2765 |
1
⊢ (𝐺 NeighbVtx 0) = {1, 3,
5} |