Metamath Proof Explorer


Theorem acycgrislfgr

Description: An acyclic hypergraph is a loop-free hypergraph. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Hypotheses acycgrislfgr.1 V = Vtx G
acycgrislfgr.2 I = iEdg G
Assertion acycgrislfgr G AcyclicGraph G UHGraph I : dom I x 𝒫 V | 2 x

Proof

Step Hyp Ref Expression
1 acycgrislfgr.1 V = Vtx G
2 acycgrislfgr.2 I = iEdg G
3 isacycgr G UHGraph G AcyclicGraph ¬ f p f Cycles G p f
4 3 biimpac G AcyclicGraph G UHGraph ¬ f p f Cycles G p f
5 loop1cycl G UHGraph f p f Cycles G p f = 1 p 0 = a a Edg G
6 3simpa f Cycles G p f = 1 p 0 = a f Cycles G p f = 1
7 6 2eximi f p f Cycles G p f = 1 p 0 = a f p f Cycles G p f = 1
8 5 7 syl6bir G UHGraph a Edg G f p f Cycles G p f = 1
9 8 exlimdv G UHGraph a a Edg G f p f Cycles G p f = 1
10 vex f V
11 hash1n0 f V f = 1 f
12 10 11 mpan f = 1 f
13 12 anim2i f Cycles G p f = 1 f Cycles G p f
14 13 2eximi f p f Cycles G p f = 1 f p f Cycles G p f
15 9 14 syl6 G UHGraph a a Edg G f p f Cycles G p f
16 15 con3d G UHGraph ¬ f p f Cycles G p f ¬ a a Edg G
17 16 adantl G AcyclicGraph G UHGraph ¬ f p f Cycles G p f ¬ a a Edg G
18 4 17 mpd G AcyclicGraph G UHGraph ¬ a a Edg G
19 1 2 lfuhgr3 G UHGraph I : dom I x 𝒫 V | 2 x ¬ a a Edg G
20 19 adantl G AcyclicGraph G UHGraph I : dom I x 𝒫 V | 2 x ¬ a a Edg G
21 18 20 mpbird G AcyclicGraph G UHGraph I : dom I x 𝒫 V | 2 x