Metamath Proof Explorer

Theorem lfuhgr1v0e

Description: A loop-free hypergraph with one vertex has no edges. (Contributed by AV, 18-Oct-2020) (Revised by AV, 2-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 lfuhgr1v0e.v 
 |-  V = ( Vtx ` G )
2 lfuhgr1v0e.i 
 |-  I = ( iEdg ` G )
3 lfuhgr1v0e.e 
 |-  E = { x e. ~P V | 2 <_ ( # ` x ) }
4 2 a1i 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 ) -> I = ( iEdg ` G ) )
5 2 dmeqi 
 |-  dom I = dom ( iEdg ` G )
6 5 a1i 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 ) -> dom I = dom ( iEdg ` G ) )
7 1 fvexi 
 |-  V e. _V
8 hash1snb 
 |-  ( V e. _V -> ( ( # ` V ) = 1 <-> E. v V = { v } ) )
9 7 8 ax-mp 
 |-  ( ( # ` V ) = 1 <-> E. v V = { v } )
10 pweq 
 |-  ( V = { v } -> ~P V = ~P { v } )
11 10 rabeqdv 
 |-  ( V = { v } -> { x e. ~P V | 2 <_ ( # ` x ) } = { x e. ~P { v } | 2 <_ ( # ` x ) } )
12 2pos 
 |-  0 < 2
13 0re 
 |-  0 e. RR
14 2re 
 |-  2 e. RR
15 13 14 ltnlei 
 |-  ( 0 < 2 <-> -. 2 <_ 0 )
16 12 15 mpbi 
 |-  -. 2 <_ 0
17 1lt2 
 |-  1 < 2
18 1re 
 |-  1 e. RR
19 18 14 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
20 17 19 mpbi 
 |-  -. 2 <_ 1
21 0ex 
 |-  (/) e. _V
22 snex 
 |-  { v } e. _V
23 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
24 hash0 
 |-  ( # ` (/) ) = 0
25 23 24 eqtrdi 
 |-  ( x = (/) -> ( # ` x ) = 0 )
26 25 breq2d 
 |-  ( x = (/) -> ( 2 <_ ( # ` x ) <-> 2 <_ 0 ) )
27 26 notbid 
 |-  ( x = (/) -> ( -. 2 <_ ( # ` x ) <-> -. 2 <_ 0 ) )
28 fveq2 
 |-  ( x = { v } -> ( # ` x ) = ( # ` { v } ) )
29 hashsng 
 |-  ( v e. _V -> ( # ` { v } ) = 1 )
30 29 elv 
 |-  ( # ` { v } ) = 1
31 28 30 eqtrdi 
 |-  ( x = { v } -> ( # ` x ) = 1 )
32 31 breq2d 
 |-  ( x = { v } -> ( 2 <_ ( # ` x ) <-> 2 <_ 1 ) )
33 32 notbid 
 |-  ( x = { v } -> ( -. 2 <_ ( # ` x ) <-> -. 2 <_ 1 ) )
34 21 22 27 33 ralpr 
 |-  ( A. x e. { (/) , { v } } -. 2 <_ ( # ` x ) <-> ( -. 2 <_ 0 /\ -. 2 <_ 1 ) )
35 16 20 34 mpbir2an 
 |-  A. x e. { (/) , { v } } -. 2 <_ ( # ` x )
36 pwsn 
 |-  ~P { v } = { (/) , { v } }
37 36 raleqi 
 |-  ( A. x e. ~P { v } -. 2 <_ ( # ` x ) <-> A. x e. { (/) , { v } } -. 2 <_ ( # ` x ) )
38 35 37 mpbir 
 |-  A. x e. ~P { v } -. 2 <_ ( # ` x )
39 rabeq0 
 |-  ( { x e. ~P { v } | 2 <_ ( # ` x ) } = (/) <-> A. x e. ~P { v } -. 2 <_ ( # ` x ) )
40 38 39 mpbir 
 |-  { x e. ~P { v } | 2 <_ ( # ` x ) } = (/)
41 11 40 eqtrdi 
 |-  ( V = { v } -> { x e. ~P V | 2 <_ ( # ` x ) } = (/) )
42 41 a1d 
 |-  ( V = { v } -> ( G e. UHGraph -> { x e. ~P V | 2 <_ ( # ` x ) } = (/) ) )
43 42 exlimiv 
 |-  ( E. v V = { v } -> ( G e. UHGraph -> { x e. ~P V | 2 <_ ( # ` x ) } = (/) ) )
44 9 43 sylbi 
 |-  ( ( # ` V ) = 1 -> ( G e. UHGraph -> { x e. ~P V | 2 <_ ( # ` x ) } = (/) ) )
45 44 impcom 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 ) -> { x e. ~P V | 2 <_ ( # ` x ) } = (/) )
46 3 45 syl5eq 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 ) -> E = (/) )
47 4 6 46 feq123d 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 ) -> ( I : dom I --> E <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) ) )
48 47 biimp3a 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) )
49 f00 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) <-> ( ( iEdg ` G ) = (/) /\ dom ( iEdg ` G ) = (/) ) )
50 49 simplbi 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) -> ( iEdg ` G ) = (/) )
51 48 50 syl 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> ( iEdg ` G ) = (/) )
52 uhgriedg0edg0 
 |-  ( G e. UHGraph -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
53 52 3ad2ant1 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> ( ( Edg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) )
54 51 53 mpbird 
 |-  ( ( G e. UHGraph /\ ( # ` V ) = 1 /\ I : dom I --> E ) -> ( Edg ` G ) = (/) )