Metamath Proof Explorer

Theorem 1egrvtxdg1

Description: The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1egrvtxdg1.v 
|- ( ph -> ( Vtx ` G ) = V )
1egrvtxdg1.a 
|- ( ph -> A e. X )
1egrvtxdg1.b 
|- ( ph -> B e. V )
1egrvtxdg1.c 
|- ( ph -> C e. V )
1egrvtxdg1.n 
|- ( ph -> B =/= C )
1egrvtxdg1.i 
|- ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
Assertion 1egrvtxdg1 
|- ( ph -> ( ( VtxDeg ` G ) ` B ) = 1 )

Proof

Step Hyp Ref Expression
1 1egrvtxdg1.v 
 |-  ( ph -> ( Vtx ` G ) = V )
2 1egrvtxdg1.a 
 |-  ( ph -> A e. X )
3 1egrvtxdg1.b 
 |-  ( ph -> B e. V )
4 1egrvtxdg1.c 
 |-  ( ph -> C e. V )
5 1egrvtxdg1.n 
 |-  ( ph -> B =/= C )
6 1egrvtxdg1.i 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 3 1 eleqtrrd 
 |-  ( ph -> B e. ( Vtx ` G ) )
9 4 1 eleqtrrd 
 |-  ( ph -> C e. ( Vtx ` G ) )
10 7 2 8 9 6 5 usgr1e 
 |-  ( ph -> G e. USGraph )
11 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
12 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
13 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
14 7 11 12 13 vtxdusgrval 
 |-  ( ( G e. USGraph /\ B e. ( Vtx ` G ) ) -> ( ( VtxDeg ` G ) ` B ) = ( # ` { x e. dom ( iEdg ` G ) | B e. ( ( iEdg ` G ) ` x ) } ) )
15 10 8 14 syl2anc 
 |-  ( ph -> ( ( VtxDeg ` G ) ` B ) = ( # ` { x e. dom ( iEdg ` G ) | B e. ( ( iEdg ` G ) ` x ) } ) )
16 dmeq 
 |-  ( ( iEdg ` G ) = { <. A , { B , C } >. } -> dom ( iEdg ` G ) = dom { <. A , { B , C } >. } )
17 16 adantl 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> dom ( iEdg ` G ) = dom { <. A , { B , C } >. } )
18 prex 
 |-  { B , C } e. _V
19 dmsnopg 
 |-  ( { B , C } e. _V -> dom { <. A , { B , C } >. } = { A } )
20 18 19 mp1i 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> dom { <. A , { B , C } >. } = { A } )
21 17 20 eqtrd 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> dom ( iEdg ` G ) = { A } )
22 fveq1 
 |-  ( ( iEdg ` G ) = { <. A , { B , C } >. } -> ( ( iEdg ` G ) ` x ) = ( { <. A , { B , C } >. } ` x ) )
23 22 eleq2d 
 |-  ( ( iEdg ` G ) = { <. A , { B , C } >. } -> ( B e. ( ( iEdg ` G ) ` x ) <-> B e. ( { <. A , { B , C } >. } ` x ) ) )
24 23 adantl 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> ( B e. ( ( iEdg ` G ) ` x ) <-> B e. ( { <. A , { B , C } >. } ` x ) ) )
25 21 24 rabeqbidv 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> { x e. dom ( iEdg ` G ) | B e. ( ( iEdg ` G ) ` x ) } = { x e. { A } | B e. ( { <. A , { B , C } >. } ` x ) } )
26 25 fveq2d 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> ( # ` { x e. dom ( iEdg ` G ) | B e. ( ( iEdg ` G ) ` x ) } ) = ( # ` { x e. { A } | B e. ( { <. A , { B , C } >. } ` x ) } ) )
27 fveq2 
 |-  ( x = A -> ( { <. A , { B , C } >. } ` x ) = ( { <. A , { B , C } >. } ` A ) )
28 27 eleq2d 
 |-  ( x = A -> ( B e. ( { <. A , { B , C } >. } ` x ) <-> B e. ( { <. A , { B , C } >. } ` A ) ) )
29 28 rabsnif 
 |-  { x e. { A } | B e. ( { <. A , { B , C } >. } ` x ) } = if ( B e. ( { <. A , { B , C } >. } ` A ) , { A } , (/) )
30 prid1g 
 |-  ( B e. V -> B e. { B , C } )
31 3 30 syl 
 |-  ( ph -> B e. { B , C } )
32 fvsng 
 |-  ( ( A e. X /\ { B , C } e. _V ) -> ( { <. A , { B , C } >. } ` A ) = { B , C } )
33 2 18 32 sylancl 
 |-  ( ph -> ( { <. A , { B , C } >. } ` A ) = { B , C } )
34 31 33 eleqtrrd 
 |-  ( ph -> B e. ( { <. A , { B , C } >. } ` A ) )
35 34 iftrued 
 |-  ( ph -> if ( B e. ( { <. A , { B , C } >. } ` A ) , { A } , (/) ) = { A } )
36 29 35 syl5eq 
 |-  ( ph -> { x e. { A } | B e. ( { <. A , { B , C } >. } ` x ) } = { A } )
37 36 fveq2d 
 |-  ( ph -> ( # ` { x e. { A } | B e. ( { <. A , { B , C } >. } ` x ) } ) = ( # ` { A } ) )
38 hashsng 
 |-  ( A e. X -> ( # ` { A } ) = 1 )
39 2 38 syl 
 |-  ( ph -> ( # ` { A } ) = 1 )
40 37 39 eqtrd 
 |-  ( ph -> ( # ` { x e. { A } | B e. ( { <. A , { B , C } >. } ` x ) } ) = 1 )
41 40 adantr 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> ( # ` { x e. { A } | B e. ( { <. A , { B , C } >. } ` x ) } ) = 1 )
42 26 41 eqtrd 
 |-  ( ( ph /\ ( iEdg ` G ) = { <. A , { B , C } >. } ) -> ( # ` { x e. dom ( iEdg ` G ) | B e. ( ( iEdg ` G ) ` x ) } ) = 1 )
43 6 42 mpdan 
 |-  ( ph -> ( # ` { x e. dom ( iEdg ` G ) | B e. ( ( iEdg ` G ) ` x ) } ) = 1 )
44 15 43 eqtrd 
 |-  ( ph -> ( ( VtxDeg ` G ) ` B ) = 1 )