Metamath Proof Explorer

Theorem eupth2lem3lem4

Description: Lemma for eupth2lem3 , formerly part of proof of eupth2lem3 : If an edge (not a loop) is added to a trail, the degree of the end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 25-Feb-2021)

Ref Expression
Hypotheses trlsegvdeg.v 
|- V = ( Vtx ` G )
trlsegvdeg.i 
|- I = ( iEdg ` G )
trlsegvdeg.f 
|- ( ph -> Fun I )
trlsegvdeg.n 
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
trlsegvdeg.u 
|- ( ph -> U e. V )
trlsegvdeg.w 
|- ( ph -> F ( Trails ` G ) P )
trlsegvdeg.vx 
|- ( ph -> ( Vtx ` X ) = V )
trlsegvdeg.vy 
|- ( ph -> ( Vtx ` Y ) = V )
trlsegvdeg.vz 
|- ( ph -> ( Vtx ` Z ) = V )
trlsegvdeg.ix 
|- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
trlsegvdeg.iy 
|- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
trlsegvdeg.iz 
|- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
eupth2lem3.o 
|- ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
eupth2lem3lem3.e 
|- ( ph -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
eupth2lem3lem4.i 
|- ( ph -> ( I ` ( F ` N ) ) e. ~P V )
Assertion eupth2lem3lem4 
|- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 trlsegvdeg.v 
 |-  V = ( Vtx ` G )
2 trlsegvdeg.i 
 |-  I = ( iEdg ` G )
3 trlsegvdeg.f 
 |-  ( ph -> Fun I )
4 trlsegvdeg.n 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5 trlsegvdeg.u 
 |-  ( ph -> U e. V )
6 trlsegvdeg.w 
 |-  ( ph -> F ( Trails ` G ) P )
7 trlsegvdeg.vx 
 |-  ( ph -> ( Vtx ` X ) = V )
8 trlsegvdeg.vy 
 |-  ( ph -> ( Vtx ` Y ) = V )
9 trlsegvdeg.vz 
 |-  ( ph -> ( Vtx ` Z ) = V )
10 trlsegvdeg.ix 
 |-  ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) )
11 trlsegvdeg.iy 
 |-  ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
12 trlsegvdeg.iz 
 |-  ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
13 eupth2lem3.o 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
14 eupth2lem3lem3.e 
 |-  ( ph -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
15 eupth2lem3lem4.i 
 |-  ( ph -> ( I ` ( F ` N ) ) e. ~P V )
16 fvexd 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( F ` N ) e. _V )
17 5 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
18 1 2 3 4 5 6 trlsegvdeglem1 
 |-  ( ph -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) )
19 18 simprd 
 |-  ( ph -> ( P ` ( N + 1 ) ) e. V )
20 19 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) e. V )
21 neeq1 
 |-  ( ( P ` N ) = U -> ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> U =/= ( P ` ( N + 1 ) ) ) )
22 21 biimpcd 
 |-  ( ( P ` N ) =/= ( P ` ( N + 1 ) ) -> ( ( P ` N ) = U -> U =/= ( P ` ( N + 1 ) ) ) )
23 22 adantl 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( ( P ` N ) = U -> U =/= ( P ` ( N + 1 ) ) ) )
24 23 imp 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U =/= ( P ` ( N + 1 ) ) )
25 15 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( I ` ( F ` N ) ) e. ~P V )
26 11 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
27 14 adantr 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
28 df-ne 
 |-  ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> -. ( P ` N ) = ( P ` ( N + 1 ) ) )
29 ifpfal 
 |-  ( -. ( P ` N ) = ( P ` ( N + 1 ) ) -> ( if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) <-> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
30 28 29 sylbi 
 |-  ( ( P ` N ) =/= ( P ` ( N + 1 ) ) -> ( if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) <-> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
31 30 adantl 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) <-> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
32 preq1 
 |-  ( ( P ` N ) = U -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , ( P ` ( N + 1 ) ) } )
33 32 sseq1d 
 |-  ( ( P ` N ) = U -> ( { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) <-> { U , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
34 33 biimpcd 
 |-  ( { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) -> ( ( P ` N ) = U -> { U , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
35 31 34 biimtrdi 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) -> ( ( P ` N ) = U -> { U , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) ) )
36 27 35 mpd 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( ( P ` N ) = U -> { U , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )
37 36 imp 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { U , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) )
38 8 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( Vtx ` Y ) = V )
39 16 17 20 24 25 26 37 38 1hegrvtxdg1 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( VtxDeg ` Y ) ` U ) = 1 )
40 39 oveq2d 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) = ( ( ( VtxDeg ` X ) ` U ) + 1 ) )
41 40 breq2d 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
42 41 notbid 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> -. 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
43 1 2 3 4 5 6 7 8 9 10 11 12 eupth2lem3lem1 
 |-  ( ph -> ( ( VtxDeg ` X ) ` U ) e. NN0 )
44 43 nn0zd 
 |-  ( ph -> ( ( VtxDeg ` X ) ` U ) e. ZZ )
45 2nn 
 |-  2 e. NN
46 45 a1i 
 |-  ( ph -> 2 e. NN )
47 1lt2 
 |-  1 < 2
48 47 a1i 
 |-  ( ph -> 1 < 2 )
49 ndvdsp1 
 |-  ( ( ( ( VtxDeg ` X ) ` U ) e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || ( ( VtxDeg ` X ) ` U ) -> -. 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
50 44 46 48 49 syl3anc 
 |-  ( ph -> ( 2 || ( ( VtxDeg ` X ) ` U ) -> -. 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
51 50 con2d 
 |-  ( ph -> ( 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) -> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
52 1z 
 |-  1 e. ZZ
53 n2dvds1 
 |-  -. 2 || 1
54 opoe 
 |-  ( ( ( ( ( VtxDeg ` X ) ` U ) e. ZZ /\ -. 2 || ( ( VtxDeg ` X ) ` U ) ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) )
55 52 53 54 mpanr12 
 |-  ( ( ( ( VtxDeg ` X ) ` U ) e. ZZ /\ -. 2 || ( ( VtxDeg ` X ) ` U ) ) -> 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) )
56 55 ex 
 |-  ( ( ( VtxDeg ` X ) ` U ) e. ZZ -> ( -. 2 || ( ( VtxDeg ` X ) ` U ) -> 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
57 44 56 syl 
 |-  ( ph -> ( -. 2 || ( ( VtxDeg ` X ) ` U ) -> 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
58 51 57 impbid 
 |-  ( ph -> ( 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) <-> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
59 fveq2 
 |-  ( x = U -> ( ( VtxDeg ` X ) ` x ) = ( ( VtxDeg ` X ) ` U ) )
60 59 breq2d 
 |-  ( x = U -> ( 2 || ( ( VtxDeg ` X ) ` x ) <-> 2 || ( ( VtxDeg ` X ) ` U ) ) )
61 60 notbid 
 |-  ( x = U -> ( -. 2 || ( ( VtxDeg ` X ) ` x ) <-> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
62 61 elrab3 
 |-  ( U e. V -> ( U e. { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } <-> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
63 5 62 syl 
 |-  ( ph -> ( U e. { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } <-> -. 2 || ( ( VtxDeg ` X ) ` U ) ) )
64 13 eleq2d 
 |-  ( ph -> ( U e. { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
65 58 63 64 3bitr2d 
 |-  ( ph -> ( 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
66 65 notbid 
 |-  ( ph -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) <-> -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
67 66 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) <-> -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
68 fvex 
 |-  ( P ` N ) e. _V
69 68 eupth2lem2 
 |-  ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( P ` N ) = U ) -> ( -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
70 69 adantll 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
71 42 67 70 3bitrd 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
72 71 expcom 
 |-  ( ( P ` N ) = U -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
73 72 eqcoms 
 |-  ( U = ( P ` N ) -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
74 fvexd 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( F ` N ) e. _V )
75 18 simpld 
 |-  ( ph -> ( P ` N ) e. V )
76 75 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) e. V )
77 5 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> U e. V )
78 neeq2 
 |-  ( ( P ` ( N + 1 ) ) = U -> ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> ( P ` N ) =/= U ) )
79 78 biimpcd 
 |-  ( ( P ` N ) =/= ( P ` ( N + 1 ) ) -> ( ( P ` ( N + 1 ) ) = U -> ( P ` N ) =/= U ) )
80 79 adantl 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( ( P ` ( N + 1 ) ) = U -> ( P ` N ) =/= U ) )
81 80 imp 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= U )
82 15 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( I ` ( F ` N ) ) e. ~P V )
83 11 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
84 preq2 
 |-  ( ( P ` ( N + 1 ) ) = U -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , U } )
85 84 sseq1d 
 |-  ( ( P ` ( N + 1 ) ) = U -> ( { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) <-> { ( P ` N ) , U } C_ ( I ` ( F ` N ) ) ) )
86 85 biimpcd 
 |-  ( { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) -> ( ( P ` ( N + 1 ) ) = U -> { ( P ` N ) , U } C_ ( I ` ( F ` N ) ) ) )
87 31 86 biimtrdi 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) -> ( ( P ` ( N + 1 ) ) = U -> { ( P ` N ) , U } C_ ( I ` ( F ` N ) ) ) ) )
88 27 87 mpd 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( ( P ` ( N + 1 ) ) = U -> { ( P ` N ) , U } C_ ( I ` ( F ` N ) ) ) )
89 88 imp 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> { ( P ` N ) , U } C_ ( I ` ( F ` N ) ) )
90 8 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( Vtx ` Y ) = V )
91 74 76 77 81 82 83 89 90 1hegrvtxdg1r 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( ( VtxDeg ` Y ) ` U ) = 1 )
92 91 oveq2d 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) = ( ( ( VtxDeg ` X ) ` U ) + 1 ) )
93 92 breq2d 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
94 93 notbid 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> -. 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) ) )
95 66 ad2antrr 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + 1 ) <-> -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
96 necom 
 |-  ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> ( P ` ( N + 1 ) ) =/= ( P ` N ) )
97 fvex 
 |-  ( P ` ( N + 1 ) ) e. _V
98 97 eupth2lem2 
 |-  ( ( ( P ` ( N + 1 ) ) =/= ( P ` N ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
99 96 98 sylanb 
 |-  ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
100 99 con1bid 
 |-  ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
101 100 adantll 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
102 94 95 101 3bitrd 
 |-  ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
103 102 expcom 
 |-  ( ( P ` ( N + 1 ) ) = U -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
104 103 eqcoms 
 |-  ( U = ( P ` ( N + 1 ) ) -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
105 73 104 jaoi 
 |-  ( ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) -> ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
106 105 com12 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) -> ( ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) ) )
107 106 3impia 
 |-  ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( ( VtxDeg ` X ) ` U ) + ( ( VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )