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

Theorem 1wlkdlem2 27558
 Description: Lemma 2 for 1wlkd 27561. (Contributed by AV, 22-Jan-2021.)
Hypotheses
Ref Expression
1wlkd.p 𝑃 = ⟨“𝑋𝑌”⟩
1wlkd.f 𝐹 = ⟨“𝐽”⟩
1wlkd.x (𝜑𝑋𝑉)
1wlkd.y (𝜑𝑌𝑉)
1wlkd.l ((𝜑𝑋 = 𝑌) → (𝐼𝐽) = {𝑋})
1wlkd.j ((𝜑𝑋𝑌) → {𝑋, 𝑌} ⊆ (𝐼𝐽))
Assertion
Ref Expression
1wlkdlem2 (𝜑𝑋 ∈ (𝐼𝐽))

Proof of Theorem 1wlkdlem2
StepHypRef Expression
1 1wlkd.x . . . . 5 (𝜑𝑋𝑉)
2 snidg 4428 . . . . 5 (𝑋𝑉𝑋 ∈ {𝑋})
31, 2syl 17 . . . 4 (𝜑𝑋 ∈ {𝑋})
43adantr 474 . . 3 ((𝜑𝑋 = 𝑌) → 𝑋 ∈ {𝑋})
5 1wlkd.l . . 3 ((𝜑𝑋 = 𝑌) → (𝐼𝐽) = {𝑋})
64, 5eleqtrrd 2862 . 2 ((𝜑𝑋 = 𝑌) → 𝑋 ∈ (𝐼𝐽))
7 1wlkd.j . . . 4 ((𝜑𝑋𝑌) → {𝑋, 𝑌} ⊆ (𝐼𝐽))
8 1wlkd.y . . . . . 6 (𝜑𝑌𝑉)
98adantr 474 . . . . 5 ((𝜑𝑋𝑌) → 𝑌𝑉)
10 prssg 4583 . . . . 5 ((𝑋𝑉𝑌𝑉) → ((𝑋 ∈ (𝐼𝐽) ∧ 𝑌 ∈ (𝐼𝐽)) ↔ {𝑋, 𝑌} ⊆ (𝐼𝐽)))
111, 9, 10syl2an2r 675 . . . 4 ((𝜑𝑋𝑌) → ((𝑋 ∈ (𝐼𝐽) ∧ 𝑌 ∈ (𝐼𝐽)) ↔ {𝑋, 𝑌} ⊆ (𝐼𝐽)))
127, 11mpbird 249 . . 3 ((𝜑𝑋𝑌) → (𝑋 ∈ (𝐼𝐽) ∧ 𝑌 ∈ (𝐼𝐽)))
1312simpld 490 . 2 ((𝜑𝑋𝑌) → 𝑋 ∈ (𝐼𝐽))
146, 13pm2.61dane 3057 1 (𝜑𝑋 ∈ (𝐼𝐽))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107   ≠ wne 2969   ⊆ wss 3792  {csn 4398  {cpr 4400  ‘cfv 6137  ⟨“cs1 13691  ⟨“cs2 13998 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-v 3400  df-un 3797  df-in 3799  df-ss 3806  df-sn 4399  df-pr 4401 This theorem is referenced by:  1wlkdlem3  27559  1wlkdlem4  27560
 Copyright terms: Public domain W3C validator