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 e. AcyclicGraph /\ G e. UHGraph ) -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )

Proof

Step Hyp Ref Expression
1 acycgrislfgr.1 
 |-  V = ( Vtx ` G )
2 acycgrislfgr.2 
 |-  I = ( iEdg ` G )
3 isacycgr 
 |-  ( G e. UHGraph -> ( G e. AcyclicGraph <-> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
4 3 biimpac 
 |-  ( ( G e. AcyclicGraph /\ G e. UHGraph ) -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
5 loop1cycl 
 |-  ( G e. UHGraph -> ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = a ) <-> { a } e. ( Edg ` G ) ) )
6 3simpa 
 |-  ( ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = a ) -> ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) )
7 6 2eximi 
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 /\ ( p ` 0 ) = a ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) )
8 5 7 syl6bir 
 |-  ( G e. UHGraph -> ( { a } e. ( Edg ` G ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) ) )
9 8 exlimdv 
 |-  ( G e. UHGraph -> ( E. a { a } e. ( Edg ` G ) -> E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) ) )
10 vex 
 |-  f e. _V
11 hash1n0 
 |-  ( ( f e. _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 
 |-  ( E. f E. p ( f ( Cycles ` G ) p /\ ( # ` f ) = 1 ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) )
15 9 14 syl6 
 |-  ( G e. UHGraph -> ( E. a { a } e. ( Edg ` G ) -> E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) )
16 15 con3d 
 |-  ( G e. UHGraph -> ( -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. E. a { a } e. ( Edg ` G ) ) )
17 16 adantl 
 |-  ( ( G e. AcyclicGraph /\ G e. UHGraph ) -> ( -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) -> -. E. a { a } e. ( Edg ` G ) ) )
18 4 17 mpd 
 |-  ( ( G e. AcyclicGraph /\ G e. UHGraph ) -> -. E. a { a } e. ( Edg ` G ) )
19 1 2 lfuhgr3 
 |-  ( G e. UHGraph -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> -. E. a { a } e. ( Edg ` G ) ) )
20 19 adantl 
 |-  ( ( G e. AcyclicGraph /\ G e. UHGraph ) -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> -. E. a { a } e. ( Edg ` G ) ) )
21 18 20 mpbird 
 |-  ( ( G e. AcyclicGraph /\ G e. UHGraph ) -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )