Metamath Proof Explorer

Theorem lfuhgr2

Description: A hypergraph is loop-free if and only if every edge is not a loop. (Contributed by BTernaryTau, 15-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 lfuhgr.1 
 |-  V = ( Vtx ` G )
2 lfuhgr.2 
 |-  I = ( iEdg ` G )
3 1 2 lfuhgr 
 |-  ( G e. UHGraph -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )
4 uhgredgn0 
 |-  ( ( G e. UHGraph /\ x e. ( Edg ` G ) ) -> x e. ( ~P ( Vtx ` G ) \ { (/) } ) )
5 eldifsni 
 |-  ( x e. ( ~P ( Vtx ` G ) \ { (/) } ) -> x =/= (/) )
6 4 5 syl 
 |-  ( ( G e. UHGraph /\ x e. ( Edg ` G ) ) -> x =/= (/) )
7 hashneq0 
 |-  ( x e. _V -> ( 0 < ( # ` x ) <-> x =/= (/) ) )
8 7 elv 
 |-  ( 0 < ( # ` x ) <-> x =/= (/) )
9 6 8 sylibr 
 |-  ( ( G e. UHGraph /\ x e. ( Edg ` G ) ) -> 0 < ( # ` x ) )
10 9 gt0ne0d 
 |-  ( ( G e. UHGraph /\ x e. ( Edg ` G ) ) -> ( # ` x ) =/= 0 )
11 hashxnn0 
 |-  ( x e. _V -> ( # ` x ) e. NN0* )
12 11 elv 
 |-  ( # ` x ) e. NN0*
13 xnn0n0n1ge2b 
 |-  ( ( # ` x ) e. NN0* -> ( ( ( # ` x ) =/= 0 /\ ( # ` x ) =/= 1 ) <-> 2 <_ ( # ` x ) ) )
14 12 13 ax-mp 
 |-  ( ( ( # ` x ) =/= 0 /\ ( # ` x ) =/= 1 ) <-> 2 <_ ( # ` x ) )
15 14 biimpi 
 |-  ( ( ( # ` x ) =/= 0 /\ ( # ` x ) =/= 1 ) -> 2 <_ ( # ` x ) )
16 10 15 stoic3 
 |-  ( ( G e. UHGraph /\ x e. ( Edg ` G ) /\ ( # ` x ) =/= 1 ) -> 2 <_ ( # ` x ) )
17 16 3exp 
 |-  ( G e. UHGraph -> ( x e. ( Edg ` G ) -> ( ( # ` x ) =/= 1 -> 2 <_ ( # ` x ) ) ) )
18 17 a2d 
 |-  ( G e. UHGraph -> ( ( x e. ( Edg ` G ) -> ( # ` x ) =/= 1 ) -> ( x e. ( Edg ` G ) -> 2 <_ ( # ` x ) ) ) )
19 18 ralimdv2 
 |-  ( G e. UHGraph -> ( A. x e. ( Edg ` G ) ( # ` x ) =/= 1 -> A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )
20 1xr 
 |-  1 e. RR*
21 hashxrcl 
 |-  ( x e. _V -> ( # ` x ) e. RR* )
22 21 elv 
 |-  ( # ` x ) e. RR*
23 1lt2 
 |-  1 < 2
24 2re 
 |-  2 e. RR
25 24 rexri 
 |-  2 e. RR*
26 xrltletr 
 |-  ( ( 1 e. RR* /\ 2 e. RR* /\ ( # ` x ) e. RR* ) -> ( ( 1 < 2 /\ 2 <_ ( # ` x ) ) -> 1 < ( # ` x ) ) )
27 20 25 22 26 mp3an 
 |-  ( ( 1 < 2 /\ 2 <_ ( # ` x ) ) -> 1 < ( # ` x ) )
28 23 27 mpan 
 |-  ( 2 <_ ( # ` x ) -> 1 < ( # ` x ) )
29 xrltne 
 |-  ( ( 1 e. RR* /\ ( # ` x ) e. RR* /\ 1 < ( # ` x ) ) -> ( # ` x ) =/= 1 )
30 20 22 28 29 mp3an12i 
 |-  ( 2 <_ ( # ` x ) -> ( # ` x ) =/= 1 )
31 30 ralimi 
 |-  ( A. x e. ( Edg ` G ) 2 <_ ( # ` x ) -> A. x e. ( Edg ` G ) ( # ` x ) =/= 1 )
32 19 31 impbid1 
 |-  ( G e. UHGraph -> ( A. x e. ( Edg ` G ) ( # ` x ) =/= 1 <-> A. x e. ( Edg ` G ) 2 <_ ( # ` x ) ) )
33 3 32 bitr4d 
 |-  ( G e. UHGraph -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> A. x e. ( Edg ` G ) ( # ` x ) =/= 1 ) )