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

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl1.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
3 usgrexmpl1.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
5 3 fveq2i ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
6 1 ovexi ⊢ 𝑉 ∈ V
7 s7cli ⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 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 } { 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 𝐸 = ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
35 4 12 34 3eqtri ⊢ ( Edg ‘ 𝐺 ) = ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )