Metamath Proof Explorer

Theorem vdegp1ai

Description: The induction step for a vertex degree calculation. If the degree of U in the edge set E is P , then adding { X , Y } to the edge set, where X =/= U =/= Y , yields degree P as well. (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
vdegp1ai.x 
|- X e. V
vdegp1ai.xu 
|- X =/= U
vdegp1ai.y 
|- Y e. V
vdegp1ai.yu 
|- Y =/= U
vdegp1ai.f 
|- ( iEdg ` F ) = ( I ++ <" { X , Y } "> )
Assertion vdegp1ai 
|- ( ( VtxDeg ` F ) ` U ) = P

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 vdegp1ai.x 
 |-  X e. V
8 vdegp1ai.xu 
 |-  X =/= U
9 vdegp1ai.y 
 |-  Y e. V
10 vdegp1ai.yu 
 |-  Y =/= U
11 vdegp1ai.f 
 |-  ( iEdg ` F ) = ( I ++ <" { X , Y } "> )
12 prex 
 |-  { X , Y } e. _V
13 wrdf 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> I : ( 0 ..^ ( # ` I ) ) --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
14 13 ffund 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> Fun I )
15 4 14 mp1i 
 |-  ( { X , Y } e. _V -> Fun I )
16 6 a1i 
 |-  ( { X , Y } e. _V -> ( Vtx ` F ) = V )
17 wrdv 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> I e. Word _V )
18 4 17 ax-mp 
 |-  I e. Word _V
19 cats1un 
 |-  ( ( I e. Word _V /\ { X , Y } e. _V ) -> ( I ++ <" { X , Y } "> ) = ( I u. { <. ( # ` I ) , { X , Y } >. } ) )
20 18 19 mpan 
 |-  ( { X , Y } e. _V -> ( I ++ <" { X , Y } "> ) = ( I u. { <. ( # ` I ) , { X , Y } >. } ) )
21 11 20 syl5eq 
 |-  ( { X , Y } e. _V -> ( iEdg ` F ) = ( I u. { <. ( # ` I ) , { X , Y } >. } ) )
22 fvexd 
 |-  ( { X , Y } e. _V -> ( # ` I ) e. _V )
23 wrdlndm 
 |-  ( I e. Word { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> ( # ` I ) e/ dom I )
24 4 23 mp1i 
 |-  ( { X , Y } e. _V -> ( # ` I ) e/ dom I )
25 2 a1i 
 |-  ( { X , Y } e. _V -> U e. V )
26 id 
 |-  ( { X , Y } e. _V -> { X , Y } e. _V )
27 8 necomi 
 |-  U =/= X
28 10 necomi 
 |-  U =/= Y
29 27 28 prneli 
 |-  U e/ { X , Y }
30 29 a1i 
 |-  ( { X , Y } e. _V -> U e/ { X , Y } )
31 1 3 15 16 21 22 24 25 26 30 p1evtxdeq 
 |-  ( { X , Y } e. _V -> ( ( VtxDeg ` F ) ` U ) = ( ( VtxDeg ` G ) ` U ) )
32 12 31 ax-mp 
 |-  ( ( VtxDeg ` F ) ` U ) = ( ( VtxDeg ` G ) ` U )
33 32 5 eqtri 
 |-  ( ( VtxDeg ` F ) ` U ) = P