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=\mathrm{Vtx}\left(G\right)$$
	frgrwopreg.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
	frgrwopreg.a	$$⊢A=\left\{x\in V|D\left(x\right)=K\right\}$$
	frgrwopreg.b	$$⊢B=V\setminus A$$
Assertion	frgrwopreglem3	$$⊢\left(X\in A\wedge Y\in B\right)\to D\left(X\right)\ne D\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		frgrwopreg.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		frgrwopreg.d	$$⊢D=\mathrm{VtxDeg}\left(G\right)$$
3		frgrwopreg.a	$$⊢A=\left\{x\in V|D\left(x\right)=K\right\}$$
4		frgrwopreg.b	$$⊢B=V\setminus A$$
5		fveqeq2	$$⊢x=Y\to \left(D\left(x\right)=K\leftrightarrow D\left(Y\right)=K\right)$$
6	5	notbid	$$⊢x=Y\to \left(\neg D\left(x\right)=K\leftrightarrow \neg D\left(Y\right)=K\right)$$
7	3	difeq2i	$$⊢V\setminus A=V\setminus \left\{x\in V|D\left(x\right)=K\right\}$$
8		notrab	$$⊢V\setminus \left\{x\in V|D\left(x\right)=K\right\}=\left\{x\in V|\neg D\left(x\right)=K\right\}$$
9	4 7 8	3eqtri	$$⊢B=\left\{x\in V|\neg D\left(x\right)=K\right\}$$
10	6 9	elrab2	$$⊢Y\in B\leftrightarrow \left(Y\in V\wedge \neg D\left(Y\right)=K\right)$$
11		fveqeq2	$$⊢x=X\to \left(D\left(x\right)=K\leftrightarrow D\left(X\right)=K\right)$$
12	11 3	elrab2	$$⊢X\in A\leftrightarrow \left(X\in V\wedge D\left(X\right)=K\right)$$
13		eqeq2	$$⊢D\left(X\right)=K\to \left(D\left(Y\right)=D\left(X\right)\leftrightarrow D\left(Y\right)=K\right)$$
14	13	notbid	$$⊢D\left(X\right)=K\to \left(\neg D\left(Y\right)=D\left(X\right)\leftrightarrow \neg D\left(Y\right)=K\right)$$
15		neqne	$$⊢\neg D\left(Y\right)=D\left(X\right)\to D\left(Y\right)\ne D\left(X\right)$$
16	15	necomd	$$⊢\neg D\left(Y\right)=D\left(X\right)\to D\left(X\right)\ne D\left(Y\right)$$
17	14 16	biimtrrdi	$$⊢D\left(X\right)=K\to \left(\neg D\left(Y\right)=K\to D\left(X\right)\ne D\left(Y\right)\right)$$
18	12 17	simplbiim	$$⊢X\in A\to \left(\neg D\left(Y\right)=K\to D\left(X\right)\ne D\left(Y\right)\right)$$
19	18	com12	$$⊢\neg D\left(Y\right)=K\to \left(X\in A\to D\left(X\right)\ne D\left(Y\right)\right)$$
20	10 19	simplbiim	$$⊢Y\in B\to \left(X\in A\to D\left(X\right)\ne D\left(Y\right)\right)$$
21	20	impcom	$$⊢\left(X\in A\wedge Y\in B\right)\to D\left(X\right)\ne D\left(Y\right)$$