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=⟨“01122003”⟩
usgrexmpl.g ⊢G=VE
Assertion usgrexmpledg ⊢Edg⁡G=0112∪2003

Proof

Step Hyp Ref Expression
1 usgrexmpl.v ⊢V=0…4
2 usgrexmpl.e ⊢E=⟨“01122003”⟩
3 usgrexmpl.g ⊢G=VE
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 ⊢01∈V
9 prex ⊢12∈V
10 8 9 pm3.2i ⊢01∈V∧12∈V
11 prex ⊢20∈V
12 prex ⊢03∈V
13 11 12 pm3.2i ⊢20∈V∧03∈V
14 10 13 pm3.2i ⊢01∈V∧12∈V∧20∈V∧03∈V
15 usgrexmpldifpr ⊢01≠12∧01≠20∧01≠03∧12≠20∧12≠03∧20≠03
16 14 15 pm3.2i ⊢01∈V∧12∈V∧20∈V∧03∈V∧01≠12∧01≠20∧01≠03∧12≠20∧12≠03∧20≠03
17 16 2 pm3.2i ⊢01∈V∧12∈V∧20∈V∧03∈V∧01≠12∧01≠20∧01≠03∧12≠20∧12≠03∧20≠03∧E=⟨“01122003”⟩
18 s4f1o ⊢01∈V∧12∈V∧20∈V∧03∈V→01≠12∧01≠20∧01≠03∧12≠20∧12≠03∧20≠03→E=⟨“01122003”⟩→E:dom⁡E⟶1-1 onto0112∪2003
19 18 imp31 ⊢01∈V∧12∈V∧20∈V∧03∈V∧01≠12∧01≠20∧01≠03∧12≠20∧12≠03∧20≠03∧E=⟨“01122003”⟩→E:dom⁡E⟶1-1 onto0112∪2003
20 dff1o5 ⊢E:dom⁡E⟶1-1 onto0112∪2003↔E:dom⁡E⟶1-10112∪2003∧ran⁡E=0112∪2003
21 20 simprbi ⊢E:dom⁡E⟶1-1 onto0112∪2003→ran⁡E=0112∪2003
22 17 19 21 mp2b ⊢ran⁡E=0112∪2003
23 4 7 22 3eqtri ⊢Edg⁡G=0112∪2003