Metamath Proof Explorer

Theorem usgrexmpl2edg

Description: The edges { 0 , 1 } , { 1 , 2 } , { 2 , 3 } , { 0 , 3 } , { 3 , 4 } , { 4 , 5 } , { 0 , 5 } of the graph G = <. V , E >. . (Contributed by AV, 3-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v ⊢ V = 0 … 5
usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
usgrexmpl2.g ⊢ G = V E
Assertion usgrexmpl2edg ⊢ Edg ⁡ G = 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ V = 0 … 5
2 usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
3 usgrexmpl2.g ⊢ G = V E
4 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
5 3 fveq2i ⊢ iEdg ⁡ G = iEdg ⁡ V E
6 1 ovexi ⊢ V ∈ V
7 s7cli ⊢ ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩ ∈ Word V
8 2 7 eqeltri ⊢ E ∈ Word V
9 opiedgfv ⊢ V ∈ V ∧ E ∈ Word V → iEdg ⁡ V E = E
10 6 8 9 mp2an ⊢ iEdg ⁡ V E = E
11 5 10 eqtri ⊢ iEdg ⁡ G = E
12 11 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ E
13 2 rneqi ⊢ ran ⁡ E = ran ⁡ ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
14 prex ⊢ 0 1 ∈ V
15 id ⊢ 0 1 ∈ V → 0 1 ∈ V
16 prex ⊢ 1 2 ∈ V
17 16 a1i ⊢ 0 1 ∈ V → 1 2 ∈ V
18 prex ⊢ 2 3 ∈ V
19 18 a1i ⊢ 0 1 ∈ V → 2 3 ∈ V
20 prex ⊢ 3 4 ∈ V
21 20 a1i ⊢ 0 1 ∈ V → 3 4 ∈ V
22 prex ⊢ 4 5 ∈ V
23 22 a1i ⊢ 0 1 ∈ V → 4 5 ∈ V
24 prex ⊢ 0 3 ∈ V
25 24 a1i ⊢ 0 1 ∈ V → 0 3 ∈ V
26 prex ⊢ 0 5 ∈ V
27 26 a1i ⊢ 0 1 ∈ V → 0 5 ∈ V
28 15 17 19 21 23 25 27 s7rn ⊢ 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 ⊢ 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 ⊢ 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 ⊢ 4 5 0 3 0 5 = 4 5 0 3 ∪ 0 5
32 df-pr ⊢ 4 5 0 3 = 4 5 ∪ 0 3
33 32 uneq1i ⊢ 4 5 0 3 ∪ 0 5 = 4 5 ∪ 0 3 ∪ 0 5
34 31 33 eqtri ⊢ 4 5 0 3 0 5 = 4 5 ∪ 0 3 ∪ 0 5
35 34 uneq2i ⊢ 3 4 ∪ 4 5 0 3 0 5 = 3 4 ∪ 4 5 ∪ 0 3 ∪ 0 5
36 unass ⊢ 4 5 ∪ 0 3 ∪ 0 5 = 4 5 ∪ 0 3 ∪ 0 5
37 uncom ⊢ 4 5 ∪ 0 3 ∪ 0 5 = 0 3 ∪ 0 5 ∪ 4 5
38 unass ⊢ 0 3 ∪ 0 5 ∪ 4 5 = 0 3 ∪ 0 5 ∪ 4 5
39 36 37 38 3eqtri ⊢ 4 5 ∪ 0 3 ∪ 0 5 = 0 3 ∪ 0 5 ∪ 4 5
40 39 uneq2i ⊢ 3 4 ∪ 4 5 ∪ 0 3 ∪ 0 5 = 3 4 ∪ 0 3 ∪ 0 5 ∪ 4 5
41 uncom ⊢ 3 4 ∪ 0 3 ∪ 0 5 ∪ 4 5 = 0 3 ∪ 0 5 ∪ 4 5 ∪ 3 4
42 unass ⊢ 0 3 ∪ 0 5 ∪ 4 5 ∪ 3 4 = 0 3 ∪ 0 5 ∪ 4 5 ∪ 3 4
43 40 41 42 3eqtri ⊢ 3 4 ∪ 4 5 ∪ 0 3 ∪ 0 5 = 0 3 ∪ 0 5 ∪ 4 5 ∪ 3 4
44 df-tp ⊢ 3 4 4 5 0 5 = 3 4 4 5 ∪ 0 5
45 uncom ⊢ 3 4 4 5 ∪ 0 5 = 0 5 ∪ 3 4 4 5
46 df-pr ⊢ 3 4 4 5 = 3 4 ∪ 4 5
47 46 equncomi ⊢ 3 4 4 5 = 4 5 ∪ 3 4
48 47 uneq2i ⊢ 0 5 ∪ 3 4 4 5 = 0 5 ∪ 4 5 ∪ 3 4
49 unass ⊢ 0 5 ∪ 4 5 ∪ 3 4 = 0 5 ∪ 4 5 ∪ 3 4
50 48 49 eqtr4i ⊢ 0 5 ∪ 3 4 4 5 = 0 5 ∪ 4 5 ∪ 3 4
51 44 45 50 3eqtrri ⊢ 0 5 ∪ 4 5 ∪ 3 4 = 3 4 4 5 0 5
52 51 uneq2i ⊢ 0 3 ∪ 0 5 ∪ 4 5 ∪ 3 4 = 0 3 ∪ 3 4 4 5 0 5
53 35 43 52 3eqtri ⊢ 3 4 ∪ 4 5 0 3 0 5 = 0 3 ∪ 3 4 4 5 0 5
54 53 uneq2i ⊢ 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 ⊢ 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 ⊢ 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 ⊢ 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 ⊢ 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 ⊢ 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 ⊢ 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 ⊢ ran ⁡ E = 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
62 4 12 61 3eqtri ⊢ Edg ⁡ G = 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5