Metamath Proof Explorer

Theorem vdegp1bi

Description: The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of U in the edge set E is P , then adding { U , X } to the edge set, where X =/= U , yields degree P + 1 . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 3-Mar-2021)

Ref Expression
Hypotheses vdegp1ai.vg 
|- V = ( Vtx ` G )
vdegp1ai.u 
|- U e. V
vdegp1ai.i 
|- I = ( iEdg ` G )
vdegp1ai.w 
|- I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }
vdegp1ai.d 
|- ( ( VtxDeg ` G ) ` U ) = P
vdegp1ai.vf 
|- ( Vtx ` F ) = V
vdegp1bi.x 
|- X e. V
vdegp1bi.xu 
|- X =/= U
vdegp1bi.f 
|- ( iEdg ` F ) = ( I ++ <" { U , X } "> )
Assertion vdegp1bi 
|- ( ( VtxDeg ` F ) ` U ) = ( P + 1 )

Proof

Step Hyp Ref Expression
1 vdegp1ai.vg 
 |-  V = ( Vtx ` G )
2 vdegp1ai.u 
 |-  U e. V
3 vdegp1ai.i 
 |-  I = ( iEdg ` G )
4 vdegp1ai.w 
 |-  I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }
5 vdegp1ai.d 
 |-  ( ( VtxDeg ` G ) ` U ) = P
6 vdegp1ai.vf 
 |-  ( Vtx ` F ) = V
7 vdegp1bi.x 
 |-  X e. V
8 vdegp1bi.xu 
 |-  X =/= U
9 vdegp1bi.f 
 |-  ( iEdg ` F ) = ( I ++ <" { U , X } "> )
10 prex 
 |-  { U , X } e. _V
11 wrdf 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> I : ( 0 ..^ ( # ` I ) ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
12 11 ffund 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> Fun I )
13 4 12 mp1i 
 |-  ( { U , X } e. _V -> Fun I )
14 6 a1i 
 |-  ( { U , X } e. _V -> ( Vtx ` F ) = V )
15 wrdv 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> I e. Word _V )
16 4 15 ax-mp 
 |-  I e. Word _V
17 cats1un 
 |-  ( ( I e. Word _V /\ { U , X } e. _V ) -> ( I ++ <" { U , X } "> ) = ( I u. { <. ( # ` I ) , { U , X } >. } ) )
18 16 17 mpan 
 |-  ( { U , X } e. _V -> ( I ++ <" { U , X } "> ) = ( I u. { <. ( # ` I ) , { U , X } >. } ) )
19 9 18 eqtrid 
 |-  ( { U , X } e. _V -> ( iEdg ` F ) = ( I u. { <. ( # ` I ) , { U , X } >. } ) )
20 fvexd 
 |-  ( { U , X } e. _V -> ( # ` I ) e. _V )
21 wrdlndm 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> ( # ` I ) e/ dom I )
22 4 21 mp1i 
 |-  ( { U , X } e. _V -> ( # ` I ) e/ dom I )
23 2 a1i 
 |-  ( { U , X } e. _V -> U e. V )
24 2 7 pm3.2i 
 |-  ( U e. V /\ X e. V )
25 prelpwi 
 |-  ( ( U e. V /\ X e. V ) -> { U , X } e. ~P V )
26 24 25 mp1i 
 |-  ( { U , X } e. _V -> { U , X } e. ~P V )
27 prid1g 
 |-  ( U e. V -> U e. { U , X } )
28 2 27 mp1i 
 |-  ( { U , X } e. _V -> U e. { U , X } )
29 8 necomi 
 |-  U =/= X
30 hashprg 
 |-  ( ( U e. V /\ X e. V ) -> ( U =/= X <-> ( # ` { U , X } ) = 2 ) )
31 2 7 30 mp2an 
 |-  ( U =/= X <-> ( # ` { U , X } ) = 2 )
32 29 31 mpbi 
 |-  ( # ` { U , X } ) = 2
33 32 eqcomi 
 |-  2 = ( # ` { U , X } )
34 2re 
 |-  2 e. RR
35 34 eqlei 
 |-  ( 2 = ( # ` { U , X } ) -> 2 <_ ( # ` { U , X } ) )
36 33 35 mp1i 
 |-  ( { U , X } e. _V -> 2 <_ ( # ` { U , X } ) )
37 1 3 13 14 19 20 22 23 26 28 36 p1evtxdp1 
 |-  ( { U , X } e. _V -> ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e 1 ) )
38 10 37 ax-mp 
 |-  ( ( VtxDeg ` F ) ` U ) = ( ( ( VtxDeg ` G ) ` U ) +e 1 )
39 fzofi 
 |-  ( 0 ..^ ( # ` I ) ) e. Fin
40 wrddm 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> dom I = ( 0 ..^ ( # ` I ) ) )
41 4 40 ax-mp 
 |-  dom I = ( 0 ..^ ( # ` I ) )
42 41 eqcomi 
 |-  ( 0 ..^ ( # ` I ) ) = dom I
43 1 3 42 vtxdgfisnn0 
 |-  ( ( ( 0 ..^ ( # ` I ) ) e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) e. NN0 )
44 39 2 43 mp2an 
 |-  ( ( VtxDeg ` G ) ` U ) e. NN0
45 44 nn0rei 
 |-  ( ( VtxDeg ` G ) ` U ) e. RR
46 1re 
 |-  1 e. RR
47 rexadd 
 |-  ( ( ( ( VtxDeg ` G ) ` U ) e. RR /\ 1 e. RR ) -> ( ( ( VtxDeg ` G ) ` U ) +e 1 ) = ( ( ( VtxDeg ` G ) ` U ) + 1 ) )
48 45 46 47 mp2an 
 |-  ( ( ( VtxDeg ` G ) ` U ) +e 1 ) = ( ( ( VtxDeg ` G ) ` U ) + 1 )
49 5 oveq1i 
 |-  ( ( ( VtxDeg ` G ) ` U ) + 1 ) = ( P + 1 )
50 38 48 49 3eqtri 
 |-  ( ( VtxDeg ` F ) ` U ) = ( P + 1 )