Metamath Proof Explorer

Theorem lfgredgge2

Description: An edge of a loop-free graph has at least two ends. (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 lfgredgge2 
|- ( ( I : A --> E /\ X e. A ) -> 2 <_ ( # ` ( I ` X ) ) )

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 eqid 
 |-  A = A
5 4 3 feq23i 
 |-  ( I : A --> E <-> I : A --> { x e. ~P V | 2 <_ ( # ` x ) } )
6 5 biimpi 
 |-  ( I : A --> E -> I : A --> { x e. ~P V | 2 <_ ( # ` x ) } )
7 6 ffvelrnda 
 |-  ( ( I : A --> E /\ X e. A ) -> ( I ` X ) e. { x e. ~P V | 2 <_ ( # ` x ) } )
8 fveq2 
 |-  ( y = ( I ` X ) -> ( # ` y ) = ( # ` ( I ` X ) ) )
9 8 breq2d 
 |-  ( y = ( I ` X ) -> ( 2 <_ ( # ` y ) <-> 2 <_ ( # ` ( I ` X ) ) ) )
10 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
11 10 breq2d 
 |-  ( x = y -> ( 2 <_ ( # ` x ) <-> 2 <_ ( # ` y ) ) )
12 11 cbvrabv 
 |-  { x e. ~P V | 2 <_ ( # ` x ) } = { y e. ~P V | 2 <_ ( # ` y ) }
13 9 12 elrab2 
 |-  ( ( I ` X ) e. { x e. ~P V | 2 <_ ( # ` x ) } <-> ( ( I ` X ) e. ~P V /\ 2 <_ ( # ` ( I ` X ) ) ) )
14 13 simprbi 
 |-  ( ( I ` X ) e. { x e. ~P V | 2 <_ ( # ` x ) } -> 2 <_ ( # ` ( I ` X ) ) )
15 7 14 syl 
 |-  ( ( I : A --> E /\ X e. A ) -> 2 <_ ( # ` ( I ` X ) ) )