Metamath Proof Explorer

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 reqabi 
 |-  ( 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 biimtrid 
 |-  ( 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 ) ) )