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 syl6bi
 |-  ( ( 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 syl6bi
 |-  ( ( 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 ) ) } ) ) )