MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frgrancvvdeqlem1 Structured version   Visualization version   GIF version

Theorem frgrancvvdeqlem1 26295
Description: Lemma 1 for frgrancvvdeq 26307. (Contributed by Alexander van der Vekens, 22-Dec-2017.)
Hypotheses
Ref Expression
frgrancvvdeq.nx 𝐷 = (⟨𝑉, 𝐸⟩ Neighbors 𝑋)
frgrancvvdeq.ny 𝑁 = (⟨𝑉, 𝐸⟩ Neighbors 𝑌)
frgrancvvdeq.x (𝜑𝑋𝑉)
frgrancvvdeq.y (𝜑𝑌𝑉)
frgrancvvdeq.ne (𝜑𝑋𝑌)
frgrancvvdeq.xy (𝜑𝑌𝐷)
frgrancvvdeq.f (𝜑𝑉 FriendGrph 𝐸)
frgrancvvdeq.a 𝐴 = (𝑥𝐷 ↦ (𝑦𝑁 {𝑥, 𝑦} ∈ ran 𝐸))
Assertion
Ref Expression
frgrancvvdeqlem1 ((𝜑𝑥𝐷) → 𝑌 ∈ (𝑉 ∖ {𝑥}))
Distinct variable groups:   𝑦,𝐷   𝑥,𝑦,𝑉   𝑥,𝐸,𝑦   𝑦,𝑌   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥,𝑦)   𝐷(𝑥)   𝑁(𝑥,𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥)

Proof of Theorem frgrancvvdeqlem1
StepHypRef Expression
1 frgrancvvdeq.y . . 3 (𝜑𝑌𝑉)
21adantr 479 . 2 ((𝜑𝑥𝐷) → 𝑌𝑉)
3 frgrancvvdeq.xy . . . . 5 (𝜑𝑌𝐷)
4 df-nel 2687 . . . . . 6 (𝑌𝐷 ↔ ¬ 𝑌𝐷)
5 eleq1a 2587 . . . . . . 7 (𝑥𝐷 → (𝑌 = 𝑥𝑌𝐷))
65con3rr3 149 . . . . . 6 𝑌𝐷 → (𝑥𝐷 → ¬ 𝑌 = 𝑥))
74, 6sylbi 205 . . . . 5 (𝑌𝐷 → (𝑥𝐷 → ¬ 𝑌 = 𝑥))
83, 7syl 17 . . . 4 (𝜑 → (𝑥𝐷 → ¬ 𝑌 = 𝑥))
98imp 443 . . 3 ((𝜑𝑥𝐷) → ¬ 𝑌 = 𝑥)
10 elsng 4042 . . . . 5 (𝑌𝑉 → (𝑌 ∈ {𝑥} ↔ 𝑌 = 𝑥))
111, 10syl 17 . . . 4 (𝜑 → (𝑌 ∈ {𝑥} ↔ 𝑌 = 𝑥))
1211adantr 479 . . 3 ((𝜑𝑥𝐷) → (𝑌 ∈ {𝑥} ↔ 𝑌 = 𝑥))
139, 12mtbird 313 . 2 ((𝜑𝑥𝐷) → ¬ 𝑌 ∈ {𝑥})
142, 13eldifd 3455 1 ((𝜑𝑥𝐷) → 𝑌 ∈ (𝑉 ∖ {𝑥}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  wne 2684  wnel 2685  cdif 3441  {csn 4028  {cpr 4030  cop 4034   class class class wbr 4481  cmpt 4541  ran crn 4933  crio 6387  (class class class)co 6426   Neighbors cnbgra 25684   FriendGrph cfrgra 26253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-nel 2687  df-v 3079  df-dif 3447  df-sn 4029
This theorem is referenced by:  frgrancvvdeqlem3  26297  frgrancvvdeqlem4  26298
  Copyright terms: Public domain W3C validator