Metamath Proof Explorer

Theorem edgssv2

Description: An edge of a simple graph is an unordered pair of vertices, i.e. a subset of the set of vertices of size 2. (Contributed by AV, 10-Jan-2020) (Revised by AV, 23-Oct-2020)

Ref Expression
Hypotheses edgssv2.v 
|- V = ( Vtx ` G )
edgssv2.e 
|- E = ( Edg ` G )
Assertion edgssv2 
|- ( ( G e. USGraph /\ C e. E ) -> ( C C_ V /\ ( # ` C ) = 2 ) )

Proof

Step Hyp Ref Expression
1 edgssv2.v 
 |-  V = ( Vtx ` G )
2 edgssv2.e 
 |-  E = ( Edg ` G )
3 2 eleq2i 
 |-  ( C e. E <-> C e. ( Edg ` G ) )
4 edgusgr 
 |-  ( ( G e. USGraph /\ C e. ( Edg ` G ) ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
5 3 4 sylan2b 
 |-  ( ( G e. USGraph /\ C e. E ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
6 elpwi 
 |-  ( C e. ~P ( Vtx ` G ) -> C C_ ( Vtx ` G ) )
7 6 anim1i 
 |-  ( ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) -> ( C C_ ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
8 5 7 syl 
 |-  ( ( G e. USGraph /\ C e. E ) -> ( C C_ ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
9 1 a1i 
 |-  ( ( G e. USGraph /\ C e. E ) -> V = ( Vtx ` G ) )
10 9 sseq2d 
 |-  ( ( G e. USGraph /\ C e. E ) -> ( C C_ V <-> C C_ ( Vtx ` G ) ) )
11 10 anbi1d 
 |-  ( ( G e. USGraph /\ C e. E ) -> ( ( C C_ V /\ ( # ` C ) = 2 ) <-> ( C C_ ( Vtx ` G ) /\ ( # ` C ) = 2 ) ) )
12 8 11 mpbird 
 |-  ( ( G e. USGraph /\ C e. E ) -> ( C C_ V /\ ( # ` C ) = 2 ) )