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 = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
ausgrusgri.1 
|- O = { f | f : dom f -1-1-> ran f }
Assertion ausgrusgri 
|- ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ ( iEdg ` H ) e. O ) -> H e. USGraph )

Proof

Step Hyp Ref Expression
1 ausgr.1 
 |-  G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
2 ausgrusgri.1 
 |-  O = { f | f : dom f -1-1-> ran f }
3 fvex 
 |-  ( Vtx ` H ) e. _V
4 fvex 
 |-  ( Edg ` H ) e. _V
5 1 isausgr 
 |-  ( ( ( Vtx ` H ) e. _V /\ ( Edg ` H ) e. _V ) -> ( ( Vtx ` H ) G ( Edg ` H ) <-> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
6 3 4 5 mp2an 
 |-  ( ( Vtx ` H ) G ( Edg ` H ) <-> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
7 edgval 
 |-  ( Edg ` H ) = ran ( iEdg ` H )
8 7 a1i 
 |-  ( H e. W -> ( Edg ` H ) = ran ( iEdg ` H ) )
9 8 sseq1d 
 |-  ( H e. W -> ( ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } <-> ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
10 2 eleq2i 
 |-  ( ( iEdg ` H ) e. O <-> ( iEdg ` H ) e. { f | f : dom f -1-1-> ran f } )
11 fvex 
 |-  ( iEdg ` H ) e. _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-1-> ran f <-> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> ran ( iEdg ` H ) ) )
16 11 15 elab 
 |-  ( ( iEdg ` H ) e. { f | f : dom f -1-1-> ran f } <-> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> ran ( iEdg ` H ) )
17 10 16 sylbb 
 |-  ( ( iEdg ` H ) e. O -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> ran ( iEdg ` H ) )
18 17 3ad2ant3 
 |-  ( ( H e. W /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } /\ ( iEdg ` H ) e. O ) -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> ran ( iEdg ` H ) )
19 simp2 
 |-  ( ( H e. W /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } /\ ( iEdg ` H ) e. O ) -> ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
20 f1ssr 
 |-  ( ( ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> ran ( iEdg ` H ) /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
21 18 19 20 syl2anc 
 |-  ( ( H e. W /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } /\ ( iEdg ` H ) e. O ) -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
22 21 3exp 
 |-  ( H e. W -> ( ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } -> ( ( iEdg ` H ) e. O -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) ) )
23 9 22 sylbid 
 |-  ( H e. W -> ( ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } -> ( ( iEdg ` H ) e. O -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) ) )
24 6 23 syl5bi 
 |-  ( H e. W -> ( ( Vtx ` H ) G ( Edg ` H ) -> ( ( iEdg ` H ) e. O -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) ) )
25 24 3imp 
 |-  ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ ( iEdg ` H ) e. O ) -> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
26 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
27 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
28 26 27 isusgrs 
 |-  ( H e. W -> ( H e. USGraph <-> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
29 28 3ad2ant1 
 |-  ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ ( iEdg ` H ) e. O ) -> ( H e. USGraph <-> ( iEdg ` H ) : dom ( iEdg ` H ) -1-1-> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
30 25 29 mpbird 
 |-  ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ ( iEdg ` H ) e. O ) -> H e. USGraph )