Metamath Proof Explorer


Theorem usgrexmpl

Description: G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4 , with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } . (Contributed by Alexander van der Vekens, 15-Aug-2017) (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 usgrexmpl G USGraph

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 1 2 usgrexmplef E : dom E 1-1 e 𝒫 V | e = 2
5 opex V E V
6 3 5 eqeltri G V
7 eqid Vtx G = Vtx G
8 eqid iEdg G = iEdg G
9 7 8 isusgrs G V G USGraph iEdg G : dom iEdg G 1-1 e 𝒫 Vtx G | e = 2
10 1 2 3 usgrexmpllem Vtx G = V iEdg G = E
11 simpr Vtx G = V iEdg G = E iEdg G = E
12 11 dmeqd Vtx G = V iEdg G = E dom iEdg G = dom E
13 pweq Vtx G = V 𝒫 Vtx G = 𝒫 V
14 13 adantr Vtx G = V iEdg G = E 𝒫 Vtx G = 𝒫 V
15 14 rabeqdv Vtx G = V iEdg G = E e 𝒫 Vtx G | e = 2 = e 𝒫 V | e = 2
16 11 12 15 f1eq123d Vtx G = V iEdg G = E iEdg G : dom iEdg G 1-1 e 𝒫 Vtx G | e = 2 E : dom E 1-1 e 𝒫 V | e = 2
17 10 16 ax-mp iEdg G : dom iEdg G 1-1 e 𝒫 Vtx G | e = 2 E : dom E 1-1 e 𝒫 V | e = 2
18 9 17 bitrdi G V G USGraph E : dom E 1-1 e 𝒫 V | e = 2
19 6 18 ax-mp G USGraph E : dom E 1-1 e 𝒫 V | e = 2
20 4 19 mpbir G USGraph