Metamath Proof Explorer

Theorem usgrexmpledg

Description: The edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } of the graph G = <. V , E >. . (Contributed by AV, 12-Jan-2020) (Revised by AV, 21-Oct-2020)

Ref Expression
Hypotheses usgrexmpl.v ⊢ 𝑉 = ( 0 ... 4 )
usgrexmpl.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
usgrexmpl.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmpledg ( Edg ‘ 𝐺 ) = ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } )

Proof

Step Hyp Ref Expression
1 usgrexmpl.v ⊢ 𝑉 = ( 0 ... 4 )
2 usgrexmpl.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
3 usgrexmpl.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
5 1 2 3 usgrexmpllem ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 )
6 5 simpri ⊢ ( iEdg ‘ 𝐺 ) = 𝐸
7 6 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐸
8 prex ⊢ { 0 , 1 } ∈ V
9 prex ⊢ { 1 , 2 } ∈ V
10 8 9 pm3.2i ⊢ ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V )
11 prex ⊢ { 2 , 0 } ∈ V
12 prex ⊢ { 0 , 3 } ∈ V
13 11 12 pm3.2i ⊢ ( { 2 , 0 } ∈ V ∧ { 0 , 3 } ∈ V )
14 10 13 pm3.2i ⊢ ( ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ ( { 2 , 0 } ∈ V ∧ { 0 , 3 } ∈ V ) )
15 usgrexmpldifpr ⊢ ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } ) )
16 14 15 pm3.2i ⊢ ( ( ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ ( { 2 , 0 } ∈ V ∧ { 0 , 3 } ∈ V ) ) ∧ ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } ) ) )
17 16 2 pm3.2i ⊢ ( ( ( ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ ( { 2 , 0 } ∈ V ∧ { 0 , 3 } ∈ V ) ) ∧ ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } ) ) ) ∧ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ )
18 s4f1o ⊢ ( ( ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ ( { 2 , 0 } ∈ V ∧ { 0 , 3 } ∈ V ) ) → ( ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } ) ) → ( 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ → 𝐸 : dom 𝐸 –1-1-onto→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ) ) )
19 18 imp31 ⊢ ( ( ( ( ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V ) ∧ ( { 2 , 0 } ∈ V ∧ { 0 , 3 } ∈ V ) ) ∧ ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 0 } ∧ { 0 , 1 } ≠ { 0 , 3 } ) ∧ ( { 1 , 2 } ≠ { 2 , 0 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 2 , 0 } ≠ { 0 , 3 } ) ) ) ∧ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ ) → 𝐸 : dom 𝐸 –1-1-onto→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) )
20 dff1o5 ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ↔ ( 𝐸 : dom 𝐸 –1-1→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ∧ ran 𝐸 = ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ) )
21 20 simprbi ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) → ran 𝐸 = ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) )
22 17 19 21 mp2b ⊢ ran 𝐸 = ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } )
23 4 7 22 3eqtri ⊢ ( Edg ‘ 𝐺 ) = ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } )