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 ⊢ V = 0 … 4
usgrexmpl.e ⊢ E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
usgrexmpl.g ⊢ G = V E
Assertion usgrexmpledg ⊢ Edg ⁡ G = 0 1 1 2 ∪ 2 0 0 3

Proof

Step Hyp Ref Expression
1 usgrexmpl.v ⊢ V = 0 … 4
2 usgrexmpl.e ⊢ E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
3 usgrexmpl.g ⊢ G = V E
4 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
5 1 2 3 usgrexmpllem ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E
6 5 simpri ⊢ iEdg ⁡ G = E
7 6 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ E
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 ∧ E = ⟨“ 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 → E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩ → E : dom ⁡ E ⟶ 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 ∧ E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩ → E : dom ⁡ E ⟶ 1-1 onto 0 1 1 2 ∪ 2 0 0 3
20 dff1o5 ⊢ E : dom ⁡ E ⟶ 1-1 onto 0 1 1 2 ∪ 2 0 0 3 ↔ E : dom ⁡ E ⟶ 1-1 0 1 1 2 ∪ 2 0 0 3 ∧ ran ⁡ E = 0 1 1 2 ∪ 2 0 0 3
21 20 simprbi ⊢ E : dom ⁡ E ⟶ 1-1 onto 0 1 1 2 ∪ 2 0 0 3 → ran ⁡ E = 0 1 1 2 ∪ 2 0 0 3
22 17 19 21 mp2b ⊢ ran ⁡ E = 0 1 1 2 ∪ 2 0 0 3
23 4 7 22 3eqtri ⊢ Edg ⁡ G = 0 1 1 2 ∪ 2 0 0 3