Metamath Proof Explorer

Theorem lfuhgr3

Description: A hypergraph is loop-free if and only if none of its edges connect to only one vertex. (Contributed by BTernaryTau, 15-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 lfuhgr3.1 
 |-  V = ( Vtx ` G )
2 lfuhgr3.2 
 |-  I = ( iEdg ` G )
3 1 2 lfuhgr2 
 |-  ( G e. UHGraph -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> A. x e. ( Edg ` G ) ( # ` x ) =/= 1 ) )
4 df-ne 
 |-  ( ( # ` x ) =/= 1 <-> -. ( # ` x ) = 1 )
5 4 ralbii 
 |-  ( A. x e. ( Edg ` G ) ( # ` x ) =/= 1 <-> A. x e. ( Edg ` G ) -. ( # ` x ) = 1 )
6 ralnex 
 |-  ( A. x e. ( Edg ` G ) -. ( # ` x ) = 1 <-> -. E. x e. ( Edg ` G ) ( # ` x ) = 1 )
7 df-rex 
 |-  ( E. x e. ( Edg ` G ) ( # ` x ) = 1 <-> E. x ( x e. ( Edg ` G ) /\ ( # ` x ) = 1 ) )
8 7 notbii 
 |-  ( -. E. x e. ( Edg ` G ) ( # ` x ) = 1 <-> -. E. x ( x e. ( Edg ` G ) /\ ( # ` x ) = 1 ) )
9 5 6 8 3bitri 
 |-  ( A. x e. ( Edg ` G ) ( # ` x ) =/= 1 <-> -. E. x ( x e. ( Edg ` G ) /\ ( # ` x ) = 1 ) )
10 hashen1 
 |-  ( x e. _V -> ( ( # ` x ) = 1 <-> x ~~ 1o ) )
11 10 elv 
 |-  ( ( # ` x ) = 1 <-> x ~~ 1o )
12 en1 
 |-  ( x ~~ 1o <-> E. a x = { a } )
13 11 12 bitri 
 |-  ( ( # ` x ) = 1 <-> E. a x = { a } )
14 13 anbi2i 
 |-  ( ( x e. ( Edg ` G ) /\ ( # ` x ) = 1 ) <-> ( x e. ( Edg ` G ) /\ E. a x = { a } ) )
15 14 exbii 
 |-  ( E. x ( x e. ( Edg ` G ) /\ ( # ` x ) = 1 ) <-> E. x ( x e. ( Edg ` G ) /\ E. a x = { a } ) )
16 15 notbii 
 |-  ( -. E. x ( x e. ( Edg ` G ) /\ ( # ` x ) = 1 ) <-> -. E. x ( x e. ( Edg ` G ) /\ E. a x = { a } ) )
17 19.3v 
 |-  ( A. a x e. ( Edg ` G ) <-> x e. ( Edg ` G ) )
18 19.29 
 |-  ( ( A. a x e. ( Edg ` G ) /\ E. a x = { a } ) -> E. a ( x e. ( Edg ` G ) /\ x = { a } ) )
19 17 18 sylanbr 
 |-  ( ( x e. ( Edg ` G ) /\ E. a x = { a } ) -> E. a ( x e. ( Edg ` G ) /\ x = { a } ) )
20 eleq1 
 |-  ( x = { a } -> ( x e. ( Edg ` G ) <-> { a } e. ( Edg ` G ) ) )
21 20 biimpac 
 |-  ( ( x e. ( Edg ` G ) /\ x = { a } ) -> { a } e. ( Edg ` G ) )
22 21 eximi 
 |-  ( E. a ( x e. ( Edg ` G ) /\ x = { a } ) -> E. a { a } e. ( Edg ` G ) )
23 19 22 syl 
 |-  ( ( x e. ( Edg ` G ) /\ E. a x = { a } ) -> E. a { a } e. ( Edg ` G ) )
24 23 exlimiv 
 |-  ( E. x ( x e. ( Edg ` G ) /\ E. a x = { a } ) -> E. a { a } e. ( Edg ` G ) )
25 dfclel 
 |-  ( { a } e. ( Edg ` G ) <-> E. x ( x = { a } /\ x e. ( Edg ` G ) ) )
26 pm3.22 
 |-  ( ( x = { a } /\ x e. ( Edg ` G ) ) -> ( x e. ( Edg ` G ) /\ x = { a } ) )
27 26 eximi 
 |-  ( E. x ( x = { a } /\ x e. ( Edg ` G ) ) -> E. x ( x e. ( Edg ` G ) /\ x = { a } ) )
28 25 27 sylbi 
 |-  ( { a } e. ( Edg ` G ) -> E. x ( x e. ( Edg ` G ) /\ x = { a } ) )
29 28 eximi 
 |-  ( E. a { a } e. ( Edg ` G ) -> E. a E. x ( x e. ( Edg ` G ) /\ x = { a } ) )
30 excomim 
 |-  ( E. a E. x ( x e. ( Edg ` G ) /\ x = { a } ) -> E. x E. a ( x e. ( Edg ` G ) /\ x = { a } ) )
31 19.40 
 |-  ( E. a ( x e. ( Edg ` G ) /\ x = { a } ) -> ( E. a x e. ( Edg ` G ) /\ E. a x = { a } ) )
32 ax5e 
 |-  ( E. a x e. ( Edg ` G ) -> x e. ( Edg ` G ) )
33 32 anim1i 
 |-  ( ( E. a x e. ( Edg ` G ) /\ E. a x = { a } ) -> ( x e. ( Edg ` G ) /\ E. a x = { a } ) )
34 31 33 syl 
 |-  ( E. a ( x e. ( Edg ` G ) /\ x = { a } ) -> ( x e. ( Edg ` G ) /\ E. a x = { a } ) )
35 34 eximi 
 |-  ( E. x E. a ( x e. ( Edg ` G ) /\ x = { a } ) -> E. x ( x e. ( Edg ` G ) /\ E. a x = { a } ) )
36 29 30 35 3syl 
 |-  ( E. a { a } e. ( Edg ` G ) -> E. x ( x e. ( Edg ` G ) /\ E. a x = { a } ) )
37 24 36 impbii 
 |-  ( E. x ( x e. ( Edg ` G ) /\ E. a x = { a } ) <-> E. a { a } e. ( Edg ` G ) )
38 37 notbii 
 |-  ( -. E. x ( x e. ( Edg ` G ) /\ E. a x = { a } ) <-> -. E. a { a } e. ( Edg ` G ) )
39 9 16 38 3bitri 
 |-  ( A. x e. ( Edg ` G ) ( # ` x ) =/= 1 <-> -. E. a { a } e. ( Edg ` G ) )
40 3 39 bitrdi 
 |-  ( G e. UHGraph -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } <-> -. E. a { a } e. ( Edg ` G ) ) )