Theorem frgrwopreglem3

Description: Lemma 3 for frgrwopreg . The vertices in the sets A and B have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 2-Jan-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 )
Assertion	frgrwopreglem3	|- ( ( X e. A /\ Y e. 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		fveqeq2	|- ( x = Y -> ( ( D ` x ) = K <-> ( D ` Y ) = K ) )
6	5	notbid	|- ( x = Y -> ( -. ( D ` x ) = K <-> -. ( D ` Y ) = K ) )
7	3	difeq2i	|- ( V \ A ) = ( V \ { x e. V | ( D ` x ) = K } )
8		notrab	|- ( V \ { x e. V | ( D ` x ) = K } ) = { x e. V | -. ( D ` x ) = K }
9	4 7 8	3eqtri	|- B = { x e. V | -. ( D ` x ) = K }
10	6 9	elrab2	|- ( Y e. B <-> ( Y e. V /\ -. ( D ` Y ) = K ) )
11		fveqeq2	|- ( x = X -> ( ( D ` x ) = K <-> ( D ` X ) = K ) )
12	11 3	elrab2	|- ( X e. A <-> ( X e. V /\ ( D ` X ) = K ) )
13		eqeq2	|- ( ( D ` X ) = K -> ( ( D ` Y ) = ( D ` X ) <-> ( D ` Y ) = K ) )
14	13	notbid	|- ( ( D ` X ) = K -> ( -. ( D ` Y ) = ( D ` X ) <-> -. ( D ` Y ) = K ) )
15		neqne	|- ( -. ( D ` Y ) = ( D ` X ) -> ( D ` Y ) =/= ( D ` X ) )
16	15	necomd	|- ( -. ( D ` Y ) = ( D ` X ) -> ( D ` X ) =/= ( D ` Y ) )
17	14 16	biimtrrdi	|- ( ( D ` X ) = K -> ( -. ( D ` Y ) = K -> ( D ` X ) =/= ( D ` Y ) ) )
18	12 17	simplbiim	|- ( X e. A -> ( -. ( D ` Y ) = K -> ( D ` X ) =/= ( D ` Y ) ) )
19	18	com12	|- ( -. ( D ` Y ) = K -> ( X e. A -> ( D ` X ) =/= ( D ` Y ) ) )
20	10 19	simplbiim	|- ( Y e. B -> ( X e. A -> ( D ` X ) =/= ( D ` Y ) ) )
21	20	impcom	|- ( ( X e. A /\ Y e. B ) -> ( D ` X ) =/= ( D ` Y ) )