Metamath Proof Explorer

Theorem edgupgr

Description: Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020)

Ref Expression
Assertion edgupgr 
|- ( ( G e. UPGraph /\ E e. ( Edg ` G ) ) -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) )

Proof

Step Hyp Ref Expression
1 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
2 1 a1i 
 |-  ( G e. UPGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
3 2 eleq2d 
 |-  ( G e. UPGraph -> ( E e. ( Edg ` G ) <-> E e. ran ( iEdg ` G ) ) )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
6 4 5 upgrf 
 |-  ( G e. UPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
7 6 frnd 
 |-  ( G e. UPGraph -> ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
8 7 sseld 
 |-  ( G e. UPGraph -> ( E e. ran ( iEdg ` G ) -> E e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
9 fveq2 
 |-  ( x = E -> ( # ` x ) = ( # ` E ) )
10 9 breq1d 
 |-  ( x = E -> ( ( # ` x ) <_ 2 <-> ( # ` E ) <_ 2 ) )
11 10 elrab 
 |-  ( E e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( E e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` E ) <_ 2 ) )
12 eldifsn 
 |-  ( E e. ( ~P ( Vtx ` G ) \ { (/) } ) <-> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) ) )
13 12 biimpi 
 |-  ( E e. ( ~P ( Vtx ` G ) \ { (/) } ) -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) ) )
14 13 anim1i 
 |-  ( ( E e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` E ) <_ 2 ) -> ( ( E e. ~P ( Vtx ` G ) /\ E =/= (/) ) /\ ( # ` E ) <_ 2 ) )
15 df-3an 
 |-  ( ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) <-> ( ( E e. ~P ( Vtx ` G ) /\ E =/= (/) ) /\ ( # ` E ) <_ 2 ) )
16 14 15 sylibr 
 |-  ( ( E e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` E ) <_ 2 ) -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) )
17 16 a1i 
 |-  ( G e. UPGraph -> ( ( E e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` E ) <_ 2 ) -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) ) )
18 11 17 biimtrid 
 |-  ( G e. UPGraph -> ( E e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) ) )
19 8 18 syld 
 |-  ( G e. UPGraph -> ( E e. ran ( iEdg ` G ) -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) ) )
20 3 19 sylbid 
 |-  ( G e. UPGraph -> ( E e. ( Edg ` G ) -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) ) )
21 20 imp 
 |-  ( ( G e. UPGraph /\ E e. ( Edg ` G ) ) -> ( E e. ~P ( Vtx ` G ) /\ E =/= (/) /\ ( # ` E ) <_ 2 ) )