ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eupth2lem3lem6fi Unicode version
Theorem eupth2lem3lem6fi 16325
Description: If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than ( P ` 0 ) and ( P ` N ): if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.)
Hypotheses
Ref Expression
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 ) ) ) )
eupth2lem3lem6fi.g |- ( ph -> G e. UPGraph )
eupth2lem3lem6fi.v |- ( ph -> V e. Fin )
eupth2lem3lem6fi.o |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
eupth2lem3lem6fi.e |- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
Assertion
Ref Expression
eupth2lem3lem6fi |- ( ( 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 ) ) } ) ) )
Distinct variable groups:   x, U   x, V   x, X
Allowed substitution hints:   ph( x)   P( x)   F( x)   G( x)   I( x)   N( x)   Y( x)   Z( x)
Proof of Theorem eupth2lem3lem6fi
StepHypRef Expression
1 trlsegvdeg.iy . . . . . . . 8 |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
213ad2ant1 1044 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
3 trlsegvdeg.vy . . . . . . . 8 |- ( ph -> (Vtx ` Y ) = V )
433ad2ant1 1044 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> (Vtx ` Y ) = V )
5 trlsegvdeg.w . . . . . . . . . 10 |- ( ph -> F (Trails ` G ) P )
6 trlsegvdeg.i . . . . . . . . . . 11 |- I = (iEdg ` G )
76trlf1 16242 . . . . . . . . . 10 |- ( F (Trails ` G ) P -> F : ( 0..^ (♯ ` F ) ) -1-1-> dom I )
8 f1f 5542 . . . . . . . . . 10 |- ( F : ( 0..^ (♯ ` F ) ) -1-1-> dom I -> F : ( 0..^ (♯ ` F ) ) --> dom I )
95, 7, 83syl 17 . . . . . . . . 9 |- ( ph -> F : ( 0..^ (♯ ` F ) ) --> dom I )
10 trlsegvdeg.n . . . . . . . . 9 |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )
119, 10ffvelcdmd 5783 . . . . . . . 8 |- ( ph -> ( F ` N ) e. dom I )
12113ad2ant1 1044 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( F ` N ) e. dom I )
13 trlsegvdeg.u . . . . . . . 8 |- ( ph -> U e. V )
14133ad2ant1 1044 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U e. V )
15 eupth2lem3lem6fi.v . . . . . . . 8 |- ( ph -> V e. Fin )
16153ad2ant1 1044 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> V e. Fin )
17 trlsegvdeg.v . . . . . . . . 9 |- V = (Vtx ` G )
1813, 3eleqtrrd 2311 . . . . . . . . . 10 |- ( ph -> U e. (Vtx ` Y ) )
19 df-vtx 15868 . . . . . . . . . . 11 |- Vtx = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) )
2019mptrcl 5729 . . . . . . . . . 10 |- ( U e. (Vtx ` Y ) -> Y e. _V )
2118, 20syl 14 . . . . . . . . 9 |- ( ph -> Y e. _V )
22 trlsegvdeg.f . . . . . . . . . . . 12 |- ( ph -> Fun I )
2322funfnd 5357 . . . . . . . . . . 11 |- ( ph -> I Fn dom I )
24 fnressn 5840 . . . . . . . . . . 11 |- ( ( I Fn dom I /\ ( F ` N ) e. dom I ) -> ( I |` { ( F ` N ) } ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
2523, 11, 24syl2anc 411 . . . . . . . . . 10 |- ( ph -> ( I |` { ( F ` N ) } ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
261, 25eqtr4d 2267 . . . . . . . . 9 |- ( ph -> (iEdg ` Y ) = ( I |` { ( F ` N ) } ) )
27 eupth2lem3lem6fi.g . . . . . . . . 9 |- ( ph -> G e. UPGraph )
2817, 6, 21, 3, 26, 27upgrspan 16133 . . . . . . . 8 |- ( ph -> Y e. UPGraph )
29283ad2ant1 1044 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> Y e. UPGraph )
30 funfvex 5656 . . . . . . . . 9 |- ( ( Fun I /\ ( F ` N ) e. dom I ) -> ( I ` ( F ` N ) ) e. _V )
3122, 11, 30syl2anc 411 . . . . . . . 8 |- ( ph -> ( I ` ( F ` N ) ) e. _V )
32313ad2ant1 1044 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( I ` ( F ` N ) ) e. _V )
33 eupth2lem3lem6fi.e . . . . . . . . 9 |- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
34 simpl 109 . . . . . . . . . . . . . 14 |- ( ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) -> U =/= ( P ` N ) )
3534adantl 277 . . . . . . . . . . . . 13 |- ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U =/= ( P ` N ) )
36 simpr 110 . . . . . . . . . . . . . 14 |- ( ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) -> U =/= ( P ` ( N + 1 ) ) )
3736adantl 277 . . . . . . . . . . . . 13 |- ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U =/= ( P ` ( N + 1 ) ) )
3835, 37nelprd 3695 . . . . . . . . . . . 12 |- ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> -. U e. { ( P ` N ) , ( P ` ( N + 1 ) ) } )
39 df-nel 2498 . . . . . . . . . . . 12 |- ( U e/ { ( P ` N ) , ( P ` ( N + 1 ) ) } <-> -. U e. { ( P ` N ) , ( P ` ( N + 1 ) ) } )
4038, 39sylibr 134 . . . . . . . . . . 11 |- ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U e/ { ( P ` N ) , ( P ` ( N + 1 ) ) } )
41 neleq2 2502 . . . . . . . . . . 11 |- ( ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } -> ( U e/ ( I ` ( F ` N ) ) <-> U e/ { ( P ` N ) , ( P ` ( N + 1 ) ) } ) )
4240, 41imbitrrid 156 . . . . . . . . . 10 |- ( ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } -> ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U e/ ( I ` ( F ` N ) ) ) )
4342expd 258 . . . . . . . . 9 |- ( ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } -> ( ( P ` N ) =/= ( P ` ( N + 1 ) ) -> ( ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) -> U e/ ( I ` ( F ` N ) ) ) ) )
4433, 43syl 14 . . . . . . . 8 |- ( ph -> ( ( P ` N ) =/= ( P ` ( N + 1 ) ) -> ( ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) -> U e/ ( I ` ( F ` N ) ) ) ) )
45443imp 1219 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U e/ ( I ` ( F ` N ) ) )
462, 4, 12, 14, 16, 29, 32, 451hevtxdg0fi 16161 . . . . . 6 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( (VtxDeg ` Y ) ` U ) = 0 )
4746oveq2d 6034 . . . . 5 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) = ( ( (VtxDeg ` X ) ` U ) + 0 ) )
48 trlsegvdeg.vx . . . . . . . . 9 |- ( ph -> (Vtx ` X ) = V )
49 trlsegvdeg.vz . . . . . . . . 9 |- ( ph -> (Vtx ` Z ) = V )
50 trlsegvdeg.ix . . . . . . . . 9 |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )
51 trlsegvdeg.iz . . . . . . . . 9 |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )
5217, 6, 22, 10, 13, 5, 48, 3, 49, 50, 1, 51, 27, 15eupth2lem3lem1fi 16322 . . . . . . . 8 |- ( ph -> ( (VtxDeg ` X ) ` U ) e. NN0 )
5352nn0cnd 9457 . . . . . . 7 |- ( ph -> ( (VtxDeg ` X ) ` U ) e. CC )
5453addridd 8328 . . . . . 6 |- ( ph -> ( ( (VtxDeg ` X ) ` U ) + 0 ) = ( (VtxDeg ` X ) ` U ) )
55543ad2ant1 1044 . . . . 5 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( ( (VtxDeg ` X ) ` U ) + 0 ) = ( (VtxDeg ` X ) ` U ) )
5647, 55eqtrd 2264 . . . 4 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) = ( (VtxDeg ` X ) ` U ) )
5756breq2d 4100 . . 3 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( 2 || ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) <-> 2 || ( (VtxDeg ` X ) ` U ) ) )
5857notbid 673 . 2 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) <-> -. 2 || ( (VtxDeg ` X ) ` U ) ) )
59 fveq2 5639 . . . . . . . 8 |- ( x = U -> ( (VtxDeg ` X ) ` x ) = ( (VtxDeg ` X ) ` U ) )
6059breq2d 4100 . . . . . . 7 |- ( x = U -> ( 2 || ( (VtxDeg ` X ) ` x ) <-> 2 || ( (VtxDeg ` X ) ` U ) ) )
6160notbid 673 . . . . . 6 |- ( x = U -> ( -. 2 || ( (VtxDeg ` X ) ` x ) <-> -. 2 || ( (VtxDeg ` X ) ` U ) ) )
6261elrab3 2963 . . . . 5 |- ( U e. V -> ( U e. { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } <-> -. 2 || ( (VtxDeg ` X ) ` U ) ) )
6313, 62syl 14 . . . 4 |- ( ph -> ( U e. { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } <-> -. 2 || ( (VtxDeg ` X ) ` U ) ) )
64 eupth2lem3lem6fi.o . . . . 5 |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
6564eleq2d 2301 . . . 4 |- ( ph -> ( U e. { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
6663, 65bitr3d 190 . . 3 |- ( ph -> ( -. 2 || ( (VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
67663ad2ant1 1044 . 2 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( (VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
68343ad2ant3 1046 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U =/= ( P ` N ) )
69363ad2ant3 1046 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> U =/= ( P ` ( N + 1 ) ) )
7068, 692thd 175 . . . . . 6 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U =/= ( P ` N ) <-> U =/= ( P ` ( N + 1 ) ) ) )
71 neeq1 2415 . . . . . . 7 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` N ) ) )
72 neeq1 2415 . . . . . . 7 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` ( N + 1 ) ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) )
7371, 72bibi12d 235 . . . . . 6 |- ( U = ( P ` 0 ) -> ( ( U =/= ( P ` N ) <-> U =/= ( P ` ( N + 1 ) ) ) <-> ( ( P ` 0 ) =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) ) )
7470, 73syl5ibcom 155 . . . . 5 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U = ( P ` 0 ) -> ( ( P ` 0 ) =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) ) )
7574pm5.32rd 451 . . . 4 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` N ) /\ U = ( P ` 0 ) ) <-> ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ U = ( P ` 0 ) ) ) )
7668neneqd 2423 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> -. U = ( P ` N ) )
77 biorf 751 . . . . . . 7 |- ( -. U = ( P ` N ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` N ) \/ U = ( P ` 0 ) ) ) )
7876, 77syl 14 . . . . . 6 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` N ) \/ U = ( P ` 0 ) ) ) )
79 orcom 735 . . . . . 6 |- ( ( U = ( P ` N ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` N ) ) )
8078, 79bitrdi 196 . . . . 5 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) )
8180anbi2d 464 . . . 4 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` N ) /\ U = ( P ` 0 ) ) <-> ( ( P ` 0 ) =/= ( P ` N ) /\ ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) ) )
8269neneqd 2423 . . . . . . 7 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> -. U = ( P ` ( N + 1 ) ) )
83 biorf 751 . . . . . . 7 |- ( -. U = ( P ` ( N + 1 ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) ) )
8482, 83syl 14 . . . . . 6 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) ) )
85 orcom 735 . . . . . 6 |- ( ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) )
8684, 85bitrdi 196 . . . . 5 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) )
8786anbi2d 464 . . . 4 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ U = ( P ` 0 ) ) <-> ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) ) )
8875, 81, 873bitr3d 218 . . 3 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` N ) /\ ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) <-> ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) ) )
89 eupth2lem1 16312 . . . 4 |- ( U e. V -> ( U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> ( ( P ` 0 ) =/= ( P ` N ) /\ ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) ) )
9014, 89syl 14 . . 3 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> ( ( P ` 0 ) =/= ( P ` N ) /\ ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) ) )
91 eupth2lem1 16312 . . . 4 |- ( U e. V -> ( U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) <-> ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) ) )
9214, 91syl 14 . . 3 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) <-> ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) ) )
9388, 90, 923bitr4d 220 . 2 |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
9458, 67, 933bitrd 214 1 |- ( ( 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 ) ) } ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 715   /\ w3a 1004   = wceq 1397   e. wcel 2202   =/= wne 2402   e/ wnel 2497   {crab 2514   _Vcvv 2802   (/)c0 3494   ifcif 3605   {csn 3669   {cpr 3670   <.cop 3672   class class class wbr 4088   X. cxp 4723   dom cdm 4725   |` cres 4727   "cima 4728   Fun wfun 5320   Fn wfn 5321   -->wf 5322   -1-1->wf1 5323   ` cfv 5326  (class class class)co 6018   1stc1st 6301   Fincfn 6909   0cc0 8032   1c1 8033   + caddc 8035   2c2 9194   ...cfz 10243  ..^cfzo 10377  ♯chash 11038   || cdvds 12350   Basecbs 13084  Vtxcvtx 15866  iEdgciedg 15867  UPGraphcupgr 15945  VtxDegcvtxdg 16140  Trailsctrls 16234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-iinf 4686  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-mulcom 8133  ax-addass 8134  ax-mulass 8135  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-1rid 8139  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-apti 8147  ax-pre-ltadd 8148
This theorem depends on definitions:  df-bi 117  df-dc 842  df-ifp 986  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-if 3606  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-tr 4188  df-id 4390  df-iord 4463  df-on 4465  df-ilim 4466  df-suc 4468  df-iom 4689  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-1st 6303  df-2nd 6304  df-recs 6471  df-frec 6557  df-1o 6582  df-2o 6583  df-er 6702  df-map 6819  df-en 6910  df-dom 6911  df-fin 6912  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-2 9202  df-3 9203  df-4 9204  df-5 9205  df-6 9206  df-7 9207  df-8 9208  df-9 9209  df-n0 9403  df-z 9480  df-dec 9612  df-uz 9756  df-xadd 10008  df-fz 10244  df-fzo 10378  df-ihash 11039  df-word 11115  df-ndx 13087  df-slot 13088  df-base 13090  df-edgf 15859  df-vtx 15868  df-iedg 15869  df-edg 15912  df-uhgrm 15923  df-upgren 15947  df-subgr 16108  df-vtxdg 16141  df-wlks 16172  df-trls 16235
This theorem is referenced by:  eupth2lem3lem7fi  16328
  Copyright terms: Public domain W3C validator