This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lfgrnloop

Description: A loop-free graph has no loops. (Contributed by AV, 23-Feb-2021)

Ref Expression
Hypotheses lfuhgrnloopv.i 
|- I = ( iEdg ` G )
lfuhgrnloopv.a 
|- A = dom I
lfuhgrnloopv.e 
|- E = { x e. ~P V | 2 <_ ( # ` x ) }
Assertion lfgrnloop 
|- ( I : A --> E -> { x e. A | ( I ` x ) = { U } } = (/) )

Proof

Step Hyp Ref Expression
1 lfuhgrnloopv.i 
 |-  I = ( iEdg ` G )
2 lfuhgrnloopv.a 
 |-  A = dom I
3 lfuhgrnloopv.e 
 |-  E = { x e. ~P V | 2 <_ ( # ` x ) }
4 nfcv 
 |-  F/_ x I
5 nfcv 
 |-  F/_ x A
6 nfrab1 
 |-  F/_ x { x e. ~P V | 2 <_ ( # ` x ) }
7 3 6 nfcxfr 
 |-  F/_ x E
8 4 5 7 nff 
 |-  F/ x I : A --> E
9 hashsn01 
 |-  ( ( # ` { U } ) = 0 \/ ( # ` { U } ) = 1 )
10 2pos 
 |-  0 < 2
11 0re 
 |-  0 e. RR
12 2re 
 |-  2 e. RR
13 11 12 ltnlei 
 |-  ( 0 < 2 <-> -. 2 <_ 0 )
14 10 13 mpbi 
 |-  -. 2 <_ 0
15 breq2 
 |-  ( ( # ` { U } ) = 0 -> ( 2 <_ ( # ` { U } ) <-> 2 <_ 0 ) )
16 14 15 mtbiri 
 |-  ( ( # ` { U } ) = 0 -> -. 2 <_ ( # ` { U } ) )
17 1lt2 
 |-  1 < 2
18 1re 
 |-  1 e. RR
19 18 12 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
20 17 19 mpbi 
 |-  -. 2 <_ 1
21 breq2 
 |-  ( ( # ` { U } ) = 1 -> ( 2 <_ ( # ` { U } ) <-> 2 <_ 1 ) )
22 20 21 mtbiri 
 |-  ( ( # ` { U } ) = 1 -> -. 2 <_ ( # ` { U } ) )
23 16 22 jaoi 
 |-  ( ( ( # ` { U } ) = 0 \/ ( # ` { U } ) = 1 ) -> -. 2 <_ ( # ` { U } ) )
24 9 23 ax-mp 
 |-  -. 2 <_ ( # ` { U } )
25 fveq2 
 |-  ( ( I ` x ) = { U } -> ( # ` ( I ` x ) ) = ( # ` { U } ) )
26 25 breq2d 
 |-  ( ( I ` x ) = { U } -> ( 2 <_ ( # ` ( I ` x ) ) <-> 2 <_ ( # ` { U } ) ) )
27 24 26 mtbiri 
 |-  ( ( I ` x ) = { U } -> -. 2 <_ ( # ` ( I ` x ) ) )
28 1 2 3 lfgredgge2 
 |-  ( ( I : A --> E /\ x e. A ) -> 2 <_ ( # ` ( I ` x ) ) )
29 27 28 nsyl3 
 |-  ( ( I : A --> E /\ x e. A ) -> -. ( I ` x ) = { U } )
30 29 ex 
 |-  ( I : A --> E -> ( x e. A -> -. ( I ` x ) = { U } ) )
31 8 30 ralrimi 
 |-  ( I : A --> E -> A. x e. A -. ( I ` x ) = { U } )
32 rabeq0 
 |-  ( { x e. A | ( I ` x ) = { U } } = (/) <-> A. x e. A -. ( I ` x ) = { U } )
33 31 32 sylibr 
 |-  ( I : A --> E -> { x e. A | ( I ` x ) = { U } } = (/) )