Metamath Proof Explorer

Theorem usgrexmpl1edg

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

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

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v ⊢ V = 0 … 5
2 usgrexmpl1.e ⊢ E = ⟨“ 0 1 0 2 1 2 0 3 3 4 3 5 4 5 ”⟩
3 usgrexmpl1.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 0 2 1 2 0 3 3 4 3 5 4 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 0 2 1 2 0 3 3 4 3 5 4 5 ”⟩
14 prex ⊢ 0 1 ∈ V
15 id ⊢ 0 1 ∈ V → 0 1 ∈ V
16 prex ⊢ 0 2 ∈ V
17 16 a1i ⊢ 0 1 ∈ V → 0 2 ∈ V
18 prex ⊢ 1 2 ∈ V
19 18 a1i ⊢ 0 1 ∈ V → 1 2 ∈ V
20 prex ⊢ 0 3 ∈ V
21 20 a1i ⊢ 0 1 ∈ V → 0 3 ∈ V
22 prex ⊢ 3 4 ∈ V
23 22 a1i ⊢ 0 1 ∈ V → 3 4 ∈ V
24 prex ⊢ 3 5 ∈ V
25 24 a1i ⊢ 0 1 ∈ V → 3 5 ∈ V
26 prex ⊢ 4 5 ∈ V
27 26 a1i ⊢ 0 1 ∈ V → 4 5 ∈ V
28 15 17 19 21 23 25 27 s7rn ⊢ 0 1 ∈ V → ran ⁡ ⟨“ 0 1 0 2 1 2 0 3 3 4 3 5 4 5 ”⟩ = 0 1 0 2 1 2 ∪ 0 3 ∪ 3 4 3 5 4 5
29 14 28 ax-mp ⊢ ran ⁡ ⟨“ 0 1 0 2 1 2 0 3 3 4 3 5 4 5 ”⟩ = 0 1 0 2 1 2 ∪ 0 3 ∪ 3 4 3 5 4 5
30 uncom ⊢ 0 1 0 2 1 2 ∪ 0 3 = 0 3 ∪ 0 1 0 2 1 2
31 30 uneq1i ⊢ 0 1 0 2 1 2 ∪ 0 3 ∪ 3 4 3 5 4 5 = 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
32 unass ⊢ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 = 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
33 31 32 eqtri ⊢ 0 1 0 2 1 2 ∪ 0 3 ∪ 3 4 3 5 4 5 = 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
34 13 29 33 3eqtri ⊢ ran ⁡ E = 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
35 4 12 34 3eqtri ⊢ Edg ⁡ G = 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5