# Metamath Proof Explorer

## 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}↔{D}\left({Y}\right)={K}\right)$
6 5 notbid ${⊢}{x}={Y}\to \left(¬{D}\left({x}\right)={K}↔¬{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}|¬{D}\left({x}\right)={K}\right\}$
9 4 7 8 3eqtri ${⊢}{B}=\left\{{x}\in {V}|¬{D}\left({x}\right)={K}\right\}$
10 6 9 elrab2 ${⊢}{Y}\in {B}↔\left({Y}\in {V}\wedge ¬{D}\left({Y}\right)={K}\right)$
11 fveqeq2 ${⊢}{x}={X}\to \left({D}\left({x}\right)={K}↔{D}\left({X}\right)={K}\right)$
12 11 3 elrab2 ${⊢}{X}\in {A}↔\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)↔{D}\left({Y}\right)={K}\right)$
14 13 notbid ${⊢}{D}\left({X}\right)={K}\to \left(¬{D}\left({Y}\right)={D}\left({X}\right)↔¬{D}\left({Y}\right)={K}\right)$
15 neqne ${⊢}¬{D}\left({Y}\right)={D}\left({X}\right)\to {D}\left({Y}\right)\ne {D}\left({X}\right)$
16 15 necomd ${⊢}¬{D}\left({Y}\right)={D}\left({X}\right)\to {D}\left({X}\right)\ne {D}\left({Y}\right)$
17 14 16 syl6bir ${⊢}{D}\left({X}\right)={K}\to \left(¬{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(¬{D}\left({Y}\right)={K}\to {D}\left({X}\right)\ne {D}\left({Y}\right)\right)$
19 18 com12 ${⊢}¬{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)$