Theorem frgrwopreglem5lem

Description: Lemma for frgrwopreglem5 . (Contributed by AV, 5-Feb-2022)

	Ref	Expression
Hypotheses	frgrwopreg.v	|- V = ( Vtx ` G )
	frgrwopreg.d	|- D = ( VtxDeg ` G )
	frgrwopreg.a	|- A = { x e. V | ( D ` x ) = K }
	frgrwopreg.b	|- B = ( V \ A )
	frgrwopreg.e	|- E = ( Edg ` G )
Assertion	frgrwopreglem5lem	|- ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( ( D ` a ) = ( D ` x ) /\ ( D ` a ) =/= ( D ` b ) /\ ( D ` x ) =/= ( D ` y ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgrwopreg.v	|- V = ( Vtx ` G )
2		frgrwopreg.d	|- D = ( VtxDeg ` G )
3		frgrwopreg.a	|- A = { x e. V | ( D ` x ) = K }
4		frgrwopreg.b	|- B = ( V \ A )
5		frgrwopreg.e	|- E = ( Edg ` G )
6	3	rabeq2i	|- ( x e. A <-> ( x e. V /\ ( D ` x ) = K ) )
7		fveqeq2	|- ( x = a -> ( ( D ` x ) = K <-> ( D ` a ) = K ) )
8	7 3	elrab2	|- ( a e. A <-> ( a e. V /\ ( D ` a ) = K ) )
9		eqtr3	|- ( ( ( D ` a ) = K /\ ( D ` x ) = K ) -> ( D ` a ) = ( D ` x ) )
10	9	expcom	|- ( ( D ` x ) = K -> ( ( D ` a ) = K -> ( D ` a ) = ( D ` x ) ) )
11	10	adantl	|- ( ( x e. V /\ ( D ` x ) = K ) -> ( ( D ` a ) = K -> ( D ` a ) = ( D ` x ) ) )
12	11	com12	|- ( ( D ` a ) = K -> ( ( x e. V /\ ( D ` x ) = K ) -> ( D ` a ) = ( D ` x ) ) )
13	8 12	simplbiim	|- ( a e. A -> ( ( x e. V /\ ( D ` x ) = K ) -> ( D ` a ) = ( D ` x ) ) )
14	6 13	syl5bi	|- ( a e. A -> ( x e. A -> ( D ` a ) = ( D ` x ) ) )
15	14	imp	|- ( ( a e. A /\ x e. A ) -> ( D ` a ) = ( D ` x ) )
16	15	adantr	|- ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( D ` a ) = ( D ` x ) )
17	1 2 3 4	frgrwopreglem3	|- ( ( a e. A /\ b e. B ) -> ( D ` a ) =/= ( D ` b ) )
18	17	ad2ant2r	|- ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( D ` a ) =/= ( D ` b ) )
19		fveqeq2	|- ( x = z -> ( ( D ` x ) = K <-> ( D ` z ) = K ) )
20	19	cbvrabv	|- { x e. V | ( D ` x ) = K } = { z e. V | ( D ` z ) = K }
21	3 20	eqtri	|- A = { z e. V | ( D ` z ) = K }
22	1 2 21 4	frgrwopreglem3	|- ( ( x e. A /\ y e. B ) -> ( D ` x ) =/= ( D ` y ) )
23	22	ad2ant2l	|- ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( D ` x ) =/= ( D ` y ) )
24	16 18 23	3jca	|- ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( ( D ` a ) = ( D ` x ) /\ ( D ` a ) =/= ( D ` b ) /\ ( D ` x ) =/= ( D ` y ) ) )