Metamath Proof Explorer

Theorem umgracycusgr

Description: An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023)

Ref Expression
Assertion umgracycusgr 
|- ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> G e. USGraph )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 umgrf 
 |-  ( G e. UMGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
4 isacycgr 
 |-  ( G e. UMGraph -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
5 4 biimpa 
 |-  ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
6 2 umgr2cycl 
 |-  ( ( G e. UMGraph /\ E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) )
7 2ne0 
 |-  2 =/= 0
8 neeq1 
 |-  ( ( # ` f ) = 2 -> ( ( # ` f ) =/= 0 <-> 2 =/= 0 ) )
9 7 8 mpbiri 
 |-  ( ( # ` f ) = 2 -> ( # ` f ) =/= 0 )
10 hasheq0 
 |-  ( f e. _V -> ( ( # ` f ) = 0 <-> f = (/) ) )
11 10 elv 
 |-  ( ( # ` f ) = 0 <-> f = (/) )
12 11 necon3bii 
 |-  ( ( # ` f ) =/= 0 <-> f =/= (/) )
13 9 12 sylib 
 |-  ( ( # ` f ) = 2 -> f =/= (/) )
14 13 anim2i 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) -> ( f ( Cycles ` G ) p /\ f =/= (/) ) )
15 14 2eximi 
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 2 ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
16 6 15 syl 
 |-  ( ( G e. UMGraph /\ E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
17 16 ex 
 |-  ( G e. UMGraph -> ( E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
18 17 con3d 
 |-  ( G e. UMGraph -> ( -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) ) )
19 18 adantr 
 |-  ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> ( -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) ) )
20 5 19 mpd 
 |-  ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> -. E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) )
21 dff15 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } <-> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } /\ -. E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) ) )
22 21 biimpri 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } /\ -. E. j e. dom ( iEdg ` G ) E. k e. dom ( iEdg ` G ) ( ( ( iEdg ` G ) ` j ) = ( ( iEdg ` G ) ` k ) /\ j =/= k ) ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
23 3 20 22 syl2an2r 
 |-  ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
24 1 2 isusgrs 
 |-  ( G e. UMGraph -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
25 24 biimprd 
 |-  ( G e. UMGraph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } -> G e. USGraph ) )
26 25 adantr 
 |-  ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } -> G e. USGraph ) )
27 23 26 mpd 
 |-  ( ( G e. UMGraph /\ G e. AcyclicGraph ) -> G e. USGraph )