Proof of Theorem usgrexmpl2edg
Step | Hyp | Ref
| Expression |
1 | | edgval 29075 |
. 2
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
2 | | usgrexmpl2.g |
. . . . 5
⊢ 𝐺 = 〈𝑉, 𝐸〉 |
3 | 2 | fveq2i 6922 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘〈𝑉, 𝐸〉) |
4 | | usgrexmpl2.v |
. . . . . 6
⊢ 𝑉 = (0...5) |
5 | 4 | ovexi 7479 |
. . . . 5
⊢ 𝑉 ∈ V |
6 | | usgrexmpl2.e |
. . . . . 6
⊢ 𝐸 = 〈“{0, 1} {1, 2}
{2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 |
7 | | s7cli 14930 |
. . . . . 6
⊢
〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0,
5}”〉 ∈ Word V |
8 | 6, 7 | eqeltri 2834 |
. . . . 5
⊢ 𝐸 ∈ Word V |
9 | | opiedgfv 29033 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ Word V) →
(iEdg‘〈𝑉, 𝐸〉) = 𝐸) |
10 | 5, 8, 9 | mp2an 691 |
. . . 4
⊢
(iEdg‘〈𝑉,
𝐸〉) = 𝐸 |
11 | 3, 10 | eqtri 2762 |
. . 3
⊢
(iEdg‘𝐺) =
𝐸 |
12 | 11 | rneqi 5961 |
. 2
⊢ ran
(iEdg‘𝐺) = ran 𝐸 |
13 | 6 | rneqi 5961 |
. . 3
⊢ ran 𝐸 = ran 〈“{0, 1} {1,
2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 |
14 | | prex 5455 |
. . . 4
⊢ {0, 1}
∈ V |
15 | | id 22 |
. . . . 5
⊢ ({0, 1}
∈ V → {0, 1} ∈ V) |
16 | | prex 5455 |
. . . . . 6
⊢ {1, 2}
∈ V |
17 | 16 | a1i 11 |
. . . . 5
⊢ ({0, 1}
∈ V → {1, 2} ∈ V) |
18 | | prex 5455 |
. . . . . 6
⊢ {2, 3}
∈ V |
19 | 18 | a1i 11 |
. . . . 5
⊢ ({0, 1}
∈ V → {2, 3} ∈ V) |
20 | | prex 5455 |
. . . . . 6
⊢ {3, 4}
∈ V |
21 | 20 | a1i 11 |
. . . . 5
⊢ ({0, 1}
∈ V → {3, 4} ∈ V) |
22 | | prex 5455 |
. . . . . 6
⊢ {4, 5}
∈ V |
23 | 22 | a1i 11 |
. . . . 5
⊢ ({0, 1}
∈ V → {4, 5} ∈ V) |
24 | | prex 5455 |
. . . . . 6
⊢ {0, 3}
∈ V |
25 | 24 | a1i 11 |
. . . . 5
⊢ ({0, 1}
∈ V → {0, 3} ∈ V) |
26 | | prex 5455 |
. . . . . 6
⊢ {0, 5}
∈ V |
27 | 26 | a1i 11 |
. . . . 5
⊢ ({0, 1}
∈ V → {0, 5} ∈ V) |
28 | 15, 17, 19, 21, 23, 25, 27 | s7rn 15010 |
. . . 4
⊢ ({0, 1}
∈ V → ran 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0,
5}”〉 = (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0,
3}, {0, 5}})) |
29 | 14, 28 | ax-mp 5 |
. . 3
⊢ ran
〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 =
(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0,
5}}) |
30 | | unass 4189 |
. . . 4
⊢ (({{0,
1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) = ({{0, 1},
{1, 2}, {2, 3}} ∪ ({{3, 4}} ∪ {{4, 5}, {0, 3}, {0,
5}})) |
31 | | df-tp 4653 |
. . . . . . . . 9
⊢ {{4, 5},
{0, 3}, {0, 5}} = ({{4, 5}, {0, 3}} ∪ {{0, 5}}) |
32 | | df-pr 4651 |
. . . . . . . . . 10
⊢ {{4, 5},
{0, 3}} = ({{4, 5}} ∪ {{0, 3}}) |
33 | 32 | uneq1i 4181 |
. . . . . . . . 9
⊢ ({{4, 5},
{0, 3}} ∪ {{0, 5}}) = (({{4, 5}} ∪ {{0, 3}}) ∪ {{0,
5}}) |
34 | 31, 33 | eqtri 2762 |
. . . . . . . 8
⊢ {{4, 5},
{0, 3}, {0, 5}} = (({{4, 5}} ∪ {{0, 3}}) ∪ {{0, 5}}) |
35 | 34 | uneq2i 4182 |
. . . . . . 7
⊢ ({{3, 4}}
∪ {{4, 5}, {0, 3}, {0, 5}}) = ({{3, 4}} ∪ (({{4, 5}} ∪ {{0, 3}})
∪ {{0, 5}})) |
36 | | unass 4189 |
. . . . . . . . . 10
⊢ (({{4,
5}} ∪ {{0, 3}}) ∪ {{0, 5}}) = ({{4, 5}} ∪ ({{0, 3}} ∪ {{0,
5}})) |
37 | | uncom 4175 |
. . . . . . . . . 10
⊢ ({{4, 5}}
∪ ({{0, 3}} ∪ {{0, 5}})) = (({{0, 3}} ∪ {{0, 5}}) ∪ {{4,
5}}) |
38 | | unass 4189 |
. . . . . . . . . 10
⊢ (({{0,
3}} ∪ {{0, 5}}) ∪ {{4, 5}}) = ({{0, 3}} ∪ ({{0, 5}} ∪ {{4,
5}})) |
39 | 36, 37, 38 | 3eqtri 2766 |
. . . . . . . . 9
⊢ (({{4,
5}} ∪ {{0, 3}}) ∪ {{0, 5}}) = ({{0, 3}} ∪ ({{0, 5}} ∪ {{4,
5}})) |
40 | 39 | uneq2i 4182 |
. . . . . . . 8
⊢ ({{3, 4}}
∪ (({{4, 5}} ∪ {{0, 3}}) ∪ {{0, 5}})) = ({{3, 4}} ∪ ({{0, 3}}
∪ ({{0, 5}} ∪ {{4, 5}}))) |
41 | | uncom 4175 |
. . . . . . . 8
⊢ ({{3, 4}}
∪ ({{0, 3}} ∪ ({{0, 5}} ∪ {{4, 5}}))) = (({{0, 3}} ∪ ({{0, 5}}
∪ {{4, 5}})) ∪ {{3, 4}}) |
42 | | unass 4189 |
. . . . . . . 8
⊢ (({{0,
3}} ∪ ({{0, 5}} ∪ {{4, 5}})) ∪ {{3, 4}}) = ({{0, 3}} ∪ (({{0,
5}} ∪ {{4, 5}}) ∪ {{3, 4}})) |
43 | 40, 41, 42 | 3eqtri 2766 |
. . . . . . 7
⊢ ({{3, 4}}
∪ (({{4, 5}} ∪ {{0, 3}}) ∪ {{0, 5}})) = ({{0, 3}} ∪ (({{0, 5}}
∪ {{4, 5}}) ∪ {{3, 4}})) |
44 | | df-tp 4653 |
. . . . . . . . 9
⊢ {{3, 4},
{4, 5}, {0, 5}} = ({{3, 4}, {4, 5}} ∪ {{0, 5}}) |
45 | | uncom 4175 |
. . . . . . . . 9
⊢ ({{3, 4},
{4, 5}} ∪ {{0, 5}}) = ({{0, 5}} ∪ {{3, 4}, {4, 5}}) |
46 | | df-pr 4651 |
. . . . . . . . . . . 12
⊢ {{3, 4},
{4, 5}} = ({{3, 4}} ∪ {{4, 5}}) |
47 | 46 | equncomi 4177 |
. . . . . . . . . . 11
⊢ {{3, 4},
{4, 5}} = ({{4, 5}} ∪ {{3, 4}}) |
48 | 47 | uneq2i 4182 |
. . . . . . . . . 10
⊢ ({{0, 5}}
∪ {{3, 4}, {4, 5}}) = ({{0, 5}} ∪ ({{4, 5}} ∪ {{3,
4}})) |
49 | | unass 4189 |
. . . . . . . . . 10
⊢ (({{0,
5}} ∪ {{4, 5}}) ∪ {{3, 4}}) = ({{0, 5}} ∪ ({{4, 5}} ∪ {{3,
4}})) |
50 | 48, 49 | eqtr4i 2765 |
. . . . . . . . 9
⊢ ({{0, 5}}
∪ {{3, 4}, {4, 5}}) = (({{0, 5}} ∪ {{4, 5}}) ∪ {{3,
4}}) |
51 | 44, 45, 50 | 3eqtrri 2767 |
. . . . . . . 8
⊢ (({{0,
5}} ∪ {{4, 5}}) ∪ {{3, 4}}) = {{3, 4}, {4, 5}, {0, 5}} |
52 | 51 | uneq2i 4182 |
. . . . . . 7
⊢ ({{0, 3}}
∪ (({{0, 5}} ∪ {{4, 5}}) ∪ {{3, 4}})) = ({{0, 3}} ∪ {{3, 4},
{4, 5}, {0, 5}}) |
53 | 35, 43, 52 | 3eqtri 2766 |
. . . . . 6
⊢ ({{3, 4}}
∪ {{4, 5}, {0, 3}, {0, 5}}) = ({{0, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}}) |
54 | 53 | uneq2i 4182 |
. . . . 5
⊢ ({{0, 1},
{1, 2}, {2, 3}} ∪ ({{3, 4}} ∪ {{4, 5}, {0, 3}, {0, 5}})) = ({{0, 1},
{1, 2}, {2, 3}} ∪ ({{0, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})) |
55 | 54 | equncomi 4177 |
. . . 4
⊢ ({{0, 1},
{1, 2}, {2, 3}} ∪ ({{3, 4}} ∪ {{4, 5}, {0, 3}, {0, 5}})) = (({{0, 3}}
∪ {{3, 4}, {4, 5}, {0, 5}}) ∪ {{0, 1}, {1, 2}, {2,
3}}) |
56 | | unass 4189 |
. . . . 5
⊢ (({{0,
3}} ∪ {{3, 4}, {4, 5}, {0, 5}}) ∪ {{0, 1}, {1, 2}, {2, 3}}) = ({{0, 3}}
∪ ({{3, 4}, {4, 5}, {0, 5}} ∪ {{0, 1}, {1, 2}, {2,
3}})) |
57 | | uncom 4175 |
. . . . . 6
⊢ ({{0, 1},
{1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}) = ({{3, 4}, {4, 5}, {0, 5}}
∪ {{0, 1}, {1, 2}, {2, 3}}) |
58 | 57 | uneq2i 4182 |
. . . . 5
⊢ ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) = ({{0, 3}}
∪ ({{3, 4}, {4, 5}, {0, 5}} ∪ {{0, 1}, {1, 2}, {2,
3}})) |
59 | 56, 58 | eqtr4i 2765 |
. . . 4
⊢ (({{0,
3}} ∪ {{3, 4}, {4, 5}, {0, 5}}) ∪ {{0, 1}, {1, 2}, {2, 3}}) = ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})) |
60 | 30, 55, 59 | 3eqtri 2766 |
. . 3
⊢ (({{0,
1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) = ({{0, 3}}
∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})) |
61 | 13, 29, 60 | 3eqtri 2766 |
. 2
⊢ ran 𝐸 = ({{0, 3}} ∪ ({{0, 1}, {1,
2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) |
62 | 1, 12, 61 | 3eqtri 2766 |
1
⊢
(Edg‘𝐺) =
({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0,
5}})) |