Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgrawopreglem3 Structured version   Unicode version

Theorem frgrawopreglem3 25716
 Description: Lemma 3 for frgrawopreg 25719. The vertices in the sets A and B have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.)
Hypotheses
Ref Expression
frgrawopreg.a VDeg
frgrawopreg.b
Assertion
Ref Expression
frgrawopreglem3 VDeg VDeg
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem frgrawopreglem3
StepHypRef Expression
1 fveq2 5825 . . . . 5 VDeg VDeg
21eqeq1d 2430 . . . 4 VDeg VDeg
3 frgrawopreg.a . . . 4 VDeg
42, 3elrab2 3173 . . 3 VDeg
5 frgrawopreg.b . . . . . 6
65eleq2i 2498 . . . . 5
7 eldif 3389 . . . . 5
86, 7bitri 252 . . . 4
9 fveq2 5825 . . . . . . . . 9 VDeg VDeg
109eqeq1d 2430 . . . . . . . 8 VDeg VDeg
1110, 3elrab2 3173 . . . . . . 7 VDeg
12 ianor 490 . . . . . . . 8 VDeg VDeg
13 pm2.21 111 . . . . . . . . 9 VDeg VDeg VDeg
14 nesym 2657 . . . . . . . . . . . . . 14 VDeg VDeg
1514biimpri 209 . . . . . . . . . . . . 13 VDeg VDeg
16 neeq1 2663 . . . . . . . . . . . . 13 VDeg VDeg VDeg VDeg
1715, 16syl5ibr 224 . . . . . . . . . . . 12 VDeg VDeg VDeg VDeg
1817adantl 467 . . . . . . . . . . 11 VDeg VDeg VDeg VDeg
1918com12 32 . . . . . . . . . 10 VDeg VDeg VDeg VDeg
2019a1d 26 . . . . . . . . 9 VDeg VDeg VDeg VDeg
2113, 20jaoi 380 . . . . . . . 8 VDeg VDeg VDeg VDeg
2212, 21sylbi 198 . . . . . . 7 VDeg VDeg VDeg VDeg
2311, 22sylnbi 307 . . . . . 6 VDeg VDeg VDeg
2423impcom 431 . . . . 5 VDeg VDeg VDeg
2524com12 32 . . . 4 VDeg VDeg VDeg
268, 25syl5bi 220 . . 3 VDeg VDeg VDeg
274, 26sylbi 198 . 2 VDeg VDeg
2827imp 430 1 VDeg VDeg
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 369   wa 370   wceq 1437   wcel 1872   wne 2599  crab 2718   cdif 3376  cfv 5544  (class class class)co 6249   VDeg cvdg 25563 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-iota 5508  df-fv 5552 This theorem is referenced by:  frgrawopreglem4  25717
 Copyright terms: Public domain W3C validator