Metamath Proof Explorer

Theorem lfuhgr

Description: A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Hypotheses lfuhgr.1 
|- V = ( Vtx ` G )
lfuhgr.2 
|- I = ( iEdg ` G )
Assertion lfuhgr 
|- ( G e. UHGraph -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )

Proof

Step Hyp Ref Expression
1 lfuhgr.1 
 |-  V = ( Vtx ` G )
2 lfuhgr.2 
 |-  I = ( iEdg ` G )
3 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
4 2 rneqi 
 |-  ran I = ran ( iEdg ` G )
5 3 4 eqtr4i 
 |-  ( Edg ` G ) = ran I
6 5 sseq1i 
 |-  ( ( Edg ` G ) C_ { x e. ~P V | 2 <_ ( # ` x ) } <-> ran I C_ { x e. ~P V | 2 <_ ( # ` x ) } )
7 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
8 fdmrn 
 |-  ( Fun I <-> I : dom I --> ran I )
9 fss 
 |-  ( ( I : dom I --> ran I /\ ran I C_ { x e. ~P V | 2 <_ ( # ` x ) } ) -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )
10 9 ex 
 |-  ( I : dom I --> ran I -> ( ran I C_ { x e. ~P V | 2 <_ ( # ` x ) } -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
11 8 10 sylbi 
 |-  ( Fun I -> ( ran I C_ { x e. ~P V | 2 <_ ( # ` x ) } -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
12 7 11 syl 
 |-  ( G e. UHGraph -> ( ran I C_ { x e. ~P V | 2 <_ ( # ` x ) } -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
13 frn 
 |-  ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ran I C_ { x e. ~P V | 2 <_ ( # ` x ) } )
14 12 13 impbid1 
 |-  ( G e. UHGraph -> ( ran I C_ { x e. ~P V | 2 <_ ( # ` x ) } <-> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
15 6 14 syl5bb 
 |-  ( G e. UHGraph -> ( ( Edg ` G ) C_ { x e. ~P V | 2 <_ ( # ` x ) } <-> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
16 uhgredgss 
 |-  ( G e. UHGraph -> ( Edg ` G ) C_ ( ~P ( Vtx ` G ) \ { (/) } ) )
17 16 difss2d 
 |-  ( G e. UHGraph -> ( Edg ` G ) C_ ~P ( Vtx ` G ) )
18 1 pweqi 
 |-  ~P V = ~P ( Vtx ` G )
19 17 18 sseqtrrdi 
 |-  ( G e. UHGraph -> ( Edg ` G ) C_ ~P V )
20 ssrab 
 |-  ( ( Edg ` G ) C_ { x e. ~P V | 2 <_ ( # ` x ) } <-> ( ( Edg ` G ) C_ ~P V /\ A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )
21 20 baib 
 |-  ( ( Edg ` G ) C_ ~P V -> ( ( Edg ` G ) C_ { x e. ~P V | 2 <_ ( # ` x ) } <-> A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )
22 19 21 syl 
 |-  ( G e. UHGraph -> ( ( Edg ` G ) C_ { x e. ~P V | 2 <_ ( # ` x ) } <-> A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )
23 15 22 bitr3d 
 |-  ( G e. UHGraph -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )