Metamath Proof Explorer


Theorem umgracycusgr

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

Ref Expression
Assertion umgracycusgr G UMGraph G AcyclicGraph G USGraph

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 eqid iEdg G = iEdg G
3 1 2 umgrf G UMGraph iEdg G : dom iEdg G x 𝒫 Vtx G | x = 2
4 isacycgr G UMGraph G AcyclicGraph ¬ f p f Cycles G p f
5 4 biimpa G UMGraph G AcyclicGraph ¬ f p f Cycles G p f
6 2 umgr2cycl G UMGraph j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k f 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 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 f p f Cycles G p f = 2 f p f Cycles G p f
16 6 15 syl G UMGraph j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k f p f Cycles G p f
17 16 ex G UMGraph j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k f p f Cycles G p f
18 17 con3d G UMGraph ¬ f p f Cycles G p f ¬ j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k
19 18 adantr G UMGraph G AcyclicGraph ¬ f p f Cycles G p f ¬ j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k
20 5 19 mpd G UMGraph G AcyclicGraph ¬ j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k
21 dff15 iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2 iEdg G : dom iEdg G x 𝒫 Vtx G | x = 2 ¬ j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k
22 21 biimpri iEdg G : dom iEdg G x 𝒫 Vtx G | x = 2 ¬ j dom iEdg G k dom iEdg G iEdg G j = iEdg G k j k iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2
23 3 20 22 syl2an2r G UMGraph G AcyclicGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2
24 1 2 isusgrs G UMGraph G USGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2
25 24 biimprd G UMGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2 G USGraph
26 25 adantr G UMGraph G AcyclicGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x = 2 G USGraph
27 23 26 mpd G UMGraph G AcyclicGraph G USGraph