# 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}=\left(0\dots 4\right)$
usgrexmpl.e ${⊢}{E}=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$
usgrexmpl.g ${⊢}{G}=⟨{V},{E}⟩$
Assertion usgrexmpl ${⊢}{G}\in \mathrm{USGraph}$

### Proof

Step Hyp Ref Expression
1 usgrexmpl.v ${⊢}{V}=\left(0\dots 4\right)$
2 usgrexmpl.e ${⊢}{E}=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$
3 usgrexmpl.g ${⊢}{G}=⟨{V},{E}⟩$
4 1 2 usgrexmplef ${⊢}{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}$
5 opex ${⊢}⟨{V},{E}⟩\in \mathrm{V}$
6 3 5 eqeltri ${⊢}{G}\in \mathrm{V}$
7 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
8 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
9 7 8 isusgrs ${⊢}{G}\in \mathrm{V}\to \left({G}\in \mathrm{USGraph}↔\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{e}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{e}\right|=2\right\}\right)$
10 1 2 3 usgrexmpllem ${⊢}\left(\mathrm{Vtx}\left({G}\right)={V}\wedge \mathrm{iEdg}\left({G}\right)={E}\right)$
11 simpr ${⊢}\left(\mathrm{Vtx}\left({G}\right)={V}\wedge \mathrm{iEdg}\left({G}\right)={E}\right)\to \mathrm{iEdg}\left({G}\right)={E}$
12 11 dmeqd ${⊢}\left(\mathrm{Vtx}\left({G}\right)={V}\wedge \mathrm{iEdg}\left({G}\right)={E}\right)\to \mathrm{dom}\mathrm{iEdg}\left({G}\right)=\mathrm{dom}{E}$
13 pweq ${⊢}\mathrm{Vtx}\left({G}\right)={V}\to 𝒫\mathrm{Vtx}\left({G}\right)=𝒫{V}$
14 13 adantr ${⊢}\left(\mathrm{Vtx}\left({G}\right)={V}\wedge \mathrm{iEdg}\left({G}\right)={E}\right)\to 𝒫\mathrm{Vtx}\left({G}\right)=𝒫{V}$
15 14 rabeqdv ${⊢}\left(\mathrm{Vtx}\left({G}\right)={V}\wedge \mathrm{iEdg}\left({G}\right)={E}\right)\to \left\{{e}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{e}\right|=2\right\}=\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}$
16 11 12 15 f1eq123d ${⊢}\left(\mathrm{Vtx}\left({G}\right)={V}\wedge \mathrm{iEdg}\left({G}\right)={E}\right)\to \left(\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{e}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{e}\right|=2\right\}↔{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}\right)$
17 10 16 ax-mp ${⊢}\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{e}\in 𝒫\mathrm{Vtx}\left({G}\right)|\left|{e}\right|=2\right\}↔{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}$
18 9 17 syl6bb ${⊢}{G}\in \mathrm{V}\to \left({G}\in \mathrm{USGraph}↔{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}\right)$
19 6 18 ax-mp ${⊢}{G}\in \mathrm{USGraph}↔{E}:\mathrm{dom}{E}\underset{1-1}{⟶}\left\{{e}\in 𝒫{V}|\left|{e}\right|=2\right\}$
20 4 19 mpbir ${⊢}{G}\in \mathrm{USGraph}$