Metamath Proof Explorer

Theorem 1egrvtxdg0

Description: The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex 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 )
1egrvtxdg0.d 
|- ( ph -> D e. V )
1egrvtxdg0.n 
|- ( ph -> C =/= D )
1egrvtxdg0.i 
|- ( ph -> ( iEdg ` G ) = { <. A , { B , D } >. } )
Assertion 1egrvtxdg0 
|- ( ph -> ( ( VtxDeg ` G ) ` C ) = 0 )

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 1egrvtxdg0.d 
 |-  ( ph -> D e. V )
7 1egrvtxdg0.n 
 |-  ( ph -> C =/= D )
8 1egrvtxdg0.i 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { B , D } >. } )
9 1 adantl 
 |-  ( ( B = D /\ ph ) -> ( Vtx ` G ) = V )
10 2 adantl 
 |-  ( ( B = D /\ ph ) -> A e. X )
11 3 adantl 
 |-  ( ( B = D /\ ph ) -> B e. V )
12 8 adantl 
 |-  ( ( B = D /\ ph ) -> ( iEdg ` G ) = { <. A , { B , D } >. } )
13 preq2 
 |-  ( D = B -> { B , D } = { B , B } )
14 13 eqcoms 
 |-  ( B = D -> { B , D } = { B , B } )
15 dfsn2 
 |-  { B } = { B , B }
16 14 15 eqtr4di 
 |-  ( B = D -> { B , D } = { B } )
17 16 adantr 
 |-  ( ( B = D /\ ph ) -> { B , D } = { B } )
18 17 opeq2d 
 |-  ( ( B = D /\ ph ) -> <. A , { B , D } >. = <. A , { B } >. )
19 18 sneqd 
 |-  ( ( B = D /\ ph ) -> { <. A , { B , D } >. } = { <. A , { B } >. } )
20 12 19 eqtrd 
 |-  ( ( B = D /\ ph ) -> ( iEdg ` G ) = { <. A , { B } >. } )
21 5 necomd 
 |-  ( ph -> C =/= B )
22 4 21 jca 
 |-  ( ph -> ( C e. V /\ C =/= B ) )
23 eldifsn 
 |-  ( C e. ( V \ { B } ) <-> ( C e. V /\ C =/= B ) )
24 22 23 sylibr 
 |-  ( ph -> C e. ( V \ { B } ) )
25 24 adantl 
 |-  ( ( B = D /\ ph ) -> C e. ( V \ { B } ) )
26 9 10 11 20 25 1loopgrvd0 
 |-  ( ( B = D /\ ph ) -> ( ( VtxDeg ` G ) ` C ) = 0 )
27 26 ex 
 |-  ( B = D -> ( ph -> ( ( VtxDeg ` G ) ` C ) = 0 ) )
28 necom 
 |-  ( B =/= C <-> C =/= B )
29 df-ne 
 |-  ( C =/= B <-> -. C = B )
30 28 29 sylbb 
 |-  ( B =/= C -> -. C = B )
31 5 30 syl 
 |-  ( ph -> -. C = B )
32 7 neneqd 
 |-  ( ph -> -. C = D )
33 31 32 jca 
 |-  ( ph -> ( -. C = B /\ -. C = D ) )
34 33 adantl 
 |-  ( ( B =/= D /\ ph ) -> ( -. C = B /\ -. C = D ) )
35 ioran 
 |-  ( -. ( C = B \/ C = D ) <-> ( -. C = B /\ -. C = D ) )
36 34 35 sylibr 
 |-  ( ( B =/= D /\ ph ) -> -. ( C = B \/ C = D ) )
37 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
38 8 rneqd 
 |-  ( ph -> ran ( iEdg ` G ) = ran { <. A , { B , D } >. } )
39 rnsnopg 
 |-  ( A e. X -> ran { <. A , { B , D } >. } = { { B , D } } )
40 2 39 syl 
 |-  ( ph -> ran { <. A , { B , D } >. } = { { B , D } } )
41 38 40 eqtrd 
 |-  ( ph -> ran ( iEdg ` G ) = { { B , D } } )
42 37 41 syl5eq 
 |-  ( ph -> ( Edg ` G ) = { { B , D } } )
43 42 adantl 
 |-  ( ( B =/= D /\ ph ) -> ( Edg ` G ) = { { B , D } } )
44 43 rexeqdv 
 |-  ( ( B =/= D /\ ph ) -> ( E. e e. ( Edg ` G ) C e. e <-> E. e e. { { B , D } } C e. e ) )
45 prex 
 |-  { B , D } e. _V
46 eleq2 
 |-  ( e = { B , D } -> ( C e. e <-> C e. { B , D } ) )
47 46 rexsng 
 |-  ( { B , D } e. _V -> ( E. e e. { { B , D } } C e. e <-> C e. { B , D } ) )
48 45 47 mp1i 
 |-  ( ( B =/= D /\ ph ) -> ( E. e e. { { B , D } } C e. e <-> C e. { B , D } ) )
49 elprg 
 |-  ( C e. V -> ( C e. { B , D } <-> ( C = B \/ C = D ) ) )
50 4 49 syl 
 |-  ( ph -> ( C e. { B , D } <-> ( C = B \/ C = D ) ) )
51 50 adantl 
 |-  ( ( B =/= D /\ ph ) -> ( C e. { B , D } <-> ( C = B \/ C = D ) ) )
52 44 48 51 3bitrd 
 |-  ( ( B =/= D /\ ph ) -> ( E. e e. ( Edg ` G ) C e. e <-> ( C = B \/ C = D ) ) )
53 36 52 mtbird 
 |-  ( ( B =/= D /\ ph ) -> -. E. e e. ( Edg ` G ) C e. e )
54 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
55 2 adantl 
 |-  ( ( B =/= D /\ ph ) -> A e. X )
56 3 1 eleqtrrd 
 |-  ( ph -> B e. ( Vtx ` G ) )
57 56 adantl 
 |-  ( ( B =/= D /\ ph ) -> B e. ( Vtx ` G ) )
58 6 1 eleqtrrd 
 |-  ( ph -> D e. ( Vtx ` G ) )
59 58 adantl 
 |-  ( ( B =/= D /\ ph ) -> D e. ( Vtx ` G ) )
60 8 adantl 
 |-  ( ( B =/= D /\ ph ) -> ( iEdg ` G ) = { <. A , { B , D } >. } )
61 simpl 
 |-  ( ( B =/= D /\ ph ) -> B =/= D )
62 54 55 57 59 60 61 usgr1e 
 |-  ( ( B =/= D /\ ph ) -> G e. USGraph )
63 4 1 eleqtrrd 
 |-  ( ph -> C e. ( Vtx ` G ) )
64 63 adantl 
 |-  ( ( B =/= D /\ ph ) -> C e. ( Vtx ` G ) )
65 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
66 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
67 54 65 66 vtxdusgr0edgnel 
 |-  ( ( G e. USGraph /\ C e. ( Vtx ` G ) ) -> ( ( ( VtxDeg ` G ) ` C ) = 0 <-> -. E. e e. ( Edg ` G ) C e. e ) )
68 62 64 67 syl2anc 
 |-  ( ( B =/= D /\ ph ) -> ( ( ( VtxDeg ` G ) ` C ) = 0 <-> -. E. e e. ( Edg ` G ) C e. e ) )
69 53 68 mpbird 
 |-  ( ( B =/= D /\ ph ) -> ( ( VtxDeg ` G ) ` C ) = 0 )
70 69 ex 
 |-  ( B =/= D -> ( ph -> ( ( VtxDeg ` G ) ` C ) = 0 ) )
71 27 70 pm2.61ine 
 |-  ( ph -> ( ( VtxDeg ` G ) ` C ) = 0 )