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 ⊢ 𝑉 = ( 0 ... 5 )
usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmpl2edg ( Edg ‘ 𝐺 ) = ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
3 usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
5 3 fveq2i ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
6 1 ovexi ⊢ 𝑉 ∈ V
7 s7cli ⊢ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩ ∈ Word V
8 2 7 eqeltri ⊢ 𝐸 ∈ Word V
9 opiedgfv ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ Word V ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
10 6 8 9 mp2an ⊢ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸
11 5 10 eqtri ⊢ ( iEdg ‘ 𝐺 ) = 𝐸
12 11 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐸
13 2 rneqi ⊢ ran 𝐸 = 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 𝐸 = ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )
62 4 12 61 3eqtri ⊢ ( Edg ‘ 𝐺 ) = ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )