Metamath Proof Explorer

Theorem ausgrusgri

Description: The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 15-Oct-2020)

Ref Expression
Hypotheses ausgr.1 ⊢G=ve|e⊆x∈𝒫v|x=2
ausgrusgri.1 ⊢O=f|f:dom⁡f⟶1-1ran⁡f
Assertion ausgrusgri ⊢H∈W∧Vtx⁡HGEdg⁡H∧iEdg⁡H∈O→H∈USGraph

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢G=ve|e⊆x∈𝒫v|x=2
2 ausgrusgri.1 ⊢O=f|f:dom⁡f⟶1-1ran⁡f
3 fvex ⊢Vtx⁡H∈V
4 fvex ⊢Edg⁡H∈V
5 1 isausgr ⊢Vtx⁡H∈V∧Edg⁡H∈V→Vtx⁡HGEdg⁡H↔Edg⁡H⊆x∈𝒫Vtx⁡H|x=2
6 3 4 5 mp2an ⊢Vtx⁡HGEdg⁡H↔Edg⁡H⊆x∈𝒫Vtx⁡H|x=2
7 edgval ⊢Edg⁡H=ran⁡iEdg⁡H
8 7 a1i ⊢H∈W→Edg⁡H=ran⁡iEdg⁡H
9 8 sseq1d ⊢H∈W→Edg⁡H⊆x∈𝒫Vtx⁡H|x=2↔ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2
10 2 eleq2i ⊢iEdg⁡H∈O↔iEdg⁡H∈f|f:dom⁡f⟶1-1ran⁡f
11 fvex ⊢iEdg⁡H∈V
12 id ⊢f=iEdg⁡H→f=iEdg⁡H
13 dmeq ⊢f=iEdg⁡H→dom⁡f=dom⁡iEdg⁡H
14 rneq ⊢f=iEdg⁡H→ran⁡f=ran⁡iEdg⁡H
15 12 13 14 f1eq123d ⊢f=iEdg⁡H→f:dom⁡f⟶1-1ran⁡f↔iEdg⁡H:dom⁡iEdg⁡H⟶1-1ran⁡iEdg⁡H
16 11 15 elab ⊢iEdg⁡H∈f|f:dom⁡f⟶1-1ran⁡f↔iEdg⁡H:dom⁡iEdg⁡H⟶1-1ran⁡iEdg⁡H
17 10 16 sylbb ⊢iEdg⁡H∈O→iEdg⁡H:dom⁡iEdg⁡H⟶1-1ran⁡iEdg⁡H
18 17 3ad2ant3 ⊢H∈W∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2∧iEdg⁡H∈O→iEdg⁡H:dom⁡iEdg⁡H⟶1-1ran⁡iEdg⁡H
19 simp2 ⊢H∈W∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2∧iEdg⁡H∈O→ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2
20 f1ssr ⊢iEdg⁡H:dom⁡iEdg⁡H⟶1-1ran⁡iEdg⁡H∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2→iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
21 18 19 20 syl2anc ⊢H∈W∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2∧iEdg⁡H∈O→iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
22 21 3exp ⊢H∈W→ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2→iEdg⁡H∈O→iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
23 9 22 sylbid ⊢H∈W→Edg⁡H⊆x∈𝒫Vtx⁡H|x=2→iEdg⁡H∈O→iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
24 6 23 biimtrid ⊢H∈W→Vtx⁡HGEdg⁡H→iEdg⁡H∈O→iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
25 24 3imp ⊢H∈W∧Vtx⁡HGEdg⁡H∧iEdg⁡H∈O→iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
26 eqid ⊢Vtx⁡H=Vtx⁡H
27 eqid ⊢iEdg⁡H=iEdg⁡H
28 26 27 isusgrs ⊢H∈W→H∈USGraph↔iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
29 28 3ad2ant1 ⊢H∈W∧Vtx⁡HGEdg⁡H∧iEdg⁡H∈O→H∈USGraph↔iEdg⁡H:dom⁡iEdg⁡H⟶1-1x∈𝒫Vtx⁡H|x=2
30 25 29 mpbird ⊢H∈W∧Vtx⁡HGEdg⁡H∧iEdg⁡H∈O→H∈USGraph