Metamath Proof Explorer

Theorem ausgrumgri

Description: If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypothesis ausgr.1 
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
Assertion ausgrumgri 
|- ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ Fun ( iEdg ` H ) ) -> H e. UMGraph )

Proof

Step Hyp Ref Expression
1 ausgr.1 
 |-  G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
2 fvex 
 |-  ( Vtx ` H ) e. _V
3 fvex 
 |-  ( Edg ` H ) e. _V
4 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 } ) )
5 2 3 4 mp2an 
 |-  ( ( Vtx ` H ) G ( Edg ` H ) <-> ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
6 edgval 
 |-  ( Edg ` H ) = ran ( iEdg ` H )
7 6 a1i 
 |-  ( H e. W -> ( Edg ` H ) = ran ( iEdg ` H ) )
8 7 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 } ) )
9 funfn 
 |-  ( Fun ( iEdg ` H ) <-> ( iEdg ` H ) Fn dom ( iEdg ` H ) )
10 9 biimpi 
 |-  ( Fun ( iEdg ` H ) -> ( iEdg ` H ) Fn dom ( iEdg ` H ) )
11 10 3ad2ant3 
 |-  ( ( H e. W /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } /\ Fun ( iEdg ` H ) ) -> ( iEdg ` H ) Fn dom ( iEdg ` H ) )
12 simp2 
 |-  ( ( H e. W /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } /\ Fun ( iEdg ` H ) ) -> ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
13 df-f 
 |-  ( ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } <-> ( ( iEdg ` H ) Fn dom ( iEdg ` H ) /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
14 11 12 13 sylanbrc 
 |-  ( ( H e. W /\ ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } /\ Fun ( iEdg ` H ) ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
15 14 3exp 
 |-  ( H e. W -> ( ran ( iEdg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } -> ( Fun ( iEdg ` H ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) ) )
16 8 15 sylbid 
 |-  ( H e. W -> ( ( Edg ` H ) C_ { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } -> ( Fun ( iEdg ` H ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) ) )
17 5 16 syl5bi 
 |-  ( H e. W -> ( ( Vtx ` H ) G ( Edg ` H ) -> ( Fun ( iEdg ` H ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) ) )
18 17 3imp 
 |-  ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ Fun ( iEdg ` H ) ) -> ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } )
19 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
20 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
21 19 20 isumgrs 
 |-  ( H e. W -> ( H e. UMGraph <-> ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
22 21 3ad2ant1 
 |-  ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ Fun ( iEdg ` H ) ) -> ( H e. UMGraph <-> ( iEdg ` H ) : dom ( iEdg ` H ) --> { x e. ~P ( Vtx ` H ) | ( # ` x ) = 2 } ) )
23 18 22 mpbird 
 |-  ( ( H e. W /\ ( Vtx ` H ) G ( Edg ` H ) /\ Fun ( iEdg ` H ) ) -> H e. UMGraph )