Metamath Proof Explorer

Theorem cusgrfilem1

Description: Lemma 1 for cusgrfi . (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 11-Nov-2020)

Ref Expression
Hypotheses cusgrfi.v 
|- V = ( Vtx ` G )
cusgrfi.p 
|- P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) }
Assertion cusgrfilem1 
|- ( ( G e. ComplUSGraph /\ N e. V ) -> P C_ ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 cusgrfi.v 
 |-  V = ( Vtx ` G )
2 cusgrfi.p 
 |-  P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) }
3 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
4 1 3 cusgredg 
 |-  ( G e. ComplUSGraph -> ( Edg ` G ) = { x e. ~P V | ( # ` x ) = 2 } )
5 fveq2 
 |-  ( x = { a , N } -> ( # ` x ) = ( # ` { a , N } ) )
6 5 ad2antlr 
 |-  ( ( ( a =/= N /\ x = { a , N } ) /\ ( a e. V /\ ( N e. V /\ x e. ~P V ) ) ) -> ( # ` x ) = ( # ` { a , N } ) )
7 hashprg 
 |-  ( ( a e. V /\ N e. V ) -> ( a =/= N <-> ( # ` { a , N } ) = 2 ) )
8 7 adantrr 
 |-  ( ( a e. V /\ ( N e. V /\ x e. ~P V ) ) -> ( a =/= N <-> ( # ` { a , N } ) = 2 ) )
9 8 biimpcd 
 |-  ( a =/= N -> ( ( a e. V /\ ( N e. V /\ x e. ~P V ) ) -> ( # ` { a , N } ) = 2 ) )
10 9 adantr 
 |-  ( ( a =/= N /\ x = { a , N } ) -> ( ( a e. V /\ ( N e. V /\ x e. ~P V ) ) -> ( # ` { a , N } ) = 2 ) )
11 10 imp 
 |-  ( ( ( a =/= N /\ x = { a , N } ) /\ ( a e. V /\ ( N e. V /\ x e. ~P V ) ) ) -> ( # ` { a , N } ) = 2 )
12 6 11 eqtrd 
 |-  ( ( ( a =/= N /\ x = { a , N } ) /\ ( a e. V /\ ( N e. V /\ x e. ~P V ) ) ) -> ( # ` x ) = 2 )
13 12 an13s 
 |-  ( ( ( N e. V /\ x e. ~P V ) /\ ( a e. V /\ ( a =/= N /\ x = { a , N } ) ) ) -> ( # ` x ) = 2 )
14 13 rexlimdvaa 
 |-  ( ( N e. V /\ x e. ~P V ) -> ( E. a e. V ( a =/= N /\ x = { a , N } ) -> ( # ` x ) = 2 ) )
15 14 ss2rabdv 
 |-  ( N e. V -> { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) } C_ { x e. ~P V | ( # ` x ) = 2 } )
16 2 a1i 
 |-  ( ( Edg ` G ) = { x e. ~P V | ( # ` x ) = 2 } -> P = { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) } )
17 id 
 |-  ( ( Edg ` G ) = { x e. ~P V | ( # ` x ) = 2 } -> ( Edg ` G ) = { x e. ~P V | ( # ` x ) = 2 } )
18 16 17 sseq12d 
 |-  ( ( Edg ` G ) = { x e. ~P V | ( # ` x ) = 2 } -> ( P C_ ( Edg ` G ) <-> { x e. ~P V | E. a e. V ( a =/= N /\ x = { a , N } ) } C_ { x e. ~P V | ( # ` x ) = 2 } ) )
19 15 18 syl5ibr 
 |-  ( ( Edg ` G ) = { x e. ~P V | ( # ` x ) = 2 } -> ( N e. V -> P C_ ( Edg ` G ) ) )
20 4 19 syl 
 |-  ( G e. ComplUSGraph -> ( N e. V -> P C_ ( Edg ` G ) ) )
21 20 imp 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> P C_ ( Edg ` G ) )