Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  21wlkdlem6 Structured version   Visualization version   GIF version

Theorem 21wlkdlem6 41138
 Description: Lemma 6 for 21wlkd 41143. (Contributed by AV, 23-Jan-2021.)
Hypotheses
Ref Expression
21wlkd.p 𝑃 = ⟨“𝐴𝐵𝐶”⟩
21wlkd.f 𝐹 = ⟨“𝐽𝐾”⟩
21wlkd.s (𝜑 → (𝐴𝑉𝐵𝑉𝐶𝑉))
21wlkd.n (𝜑 → (𝐴𝐵𝐵𝐶))
21wlkd.e (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)))
Assertion
Ref Expression
21wlkdlem6 (𝜑 → (𝐵 ∈ (𝐼𝐽) ∧ 𝐵 ∈ (𝐼𝐾)))

Proof of Theorem 21wlkdlem6
StepHypRef Expression
1 21wlkd.e . 2 (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)))
2 prcom 4211 . . . . . . . . 9 {𝐴, 𝐵} = {𝐵, 𝐴}
32sseq1i 3592 . . . . . . . 8 ({𝐴, 𝐵} ⊆ (𝐼𝐽) ↔ {𝐵, 𝐴} ⊆ (𝐼𝐽))
43biimpi 205 . . . . . . 7 ({𝐴, 𝐵} ⊆ (𝐼𝐽) → {𝐵, 𝐴} ⊆ (𝐼𝐽))
54adantl 481 . . . . . 6 ((𝜑 ∧ {𝐴, 𝐵} ⊆ (𝐼𝐽)) → {𝐵, 𝐴} ⊆ (𝐼𝐽))
6 21wlkd.s . . . . . . . 8 (𝜑 → (𝐴𝑉𝐵𝑉𝐶𝑉))
76simp2d 1067 . . . . . . 7 (𝜑𝐵𝑉)
86simp1d 1066 . . . . . . . 8 (𝜑𝐴𝑉)
98adantr 480 . . . . . . 7 ((𝜑 ∧ {𝐴, 𝐵} ⊆ (𝐼𝐽)) → 𝐴𝑉)
10 prssg 4290 . . . . . . 7 ((𝐵𝑉𝐴𝑉) → ((𝐵 ∈ (𝐼𝐽) ∧ 𝐴 ∈ (𝐼𝐽)) ↔ {𝐵, 𝐴} ⊆ (𝐼𝐽)))
117, 9, 10syl2an2r 872 . . . . . 6 ((𝜑 ∧ {𝐴, 𝐵} ⊆ (𝐼𝐽)) → ((𝐵 ∈ (𝐼𝐽) ∧ 𝐴 ∈ (𝐼𝐽)) ↔ {𝐵, 𝐴} ⊆ (𝐼𝐽)))
125, 11mpbird 246 . . . . 5 ((𝜑 ∧ {𝐴, 𝐵} ⊆ (𝐼𝐽)) → (𝐵 ∈ (𝐼𝐽) ∧ 𝐴 ∈ (𝐼𝐽)))
1312simpld 474 . . . 4 ((𝜑 ∧ {𝐴, 𝐵} ⊆ (𝐼𝐽)) → 𝐵 ∈ (𝐼𝐽))
1413ex 449 . . 3 (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼𝐽) → 𝐵 ∈ (𝐼𝐽)))
15 simpr 476 . . . . . 6 ((𝜑 ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)) → {𝐵, 𝐶} ⊆ (𝐼𝐾))
166simp3d 1068 . . . . . . . 8 (𝜑𝐶𝑉)
1716adantr 480 . . . . . . 7 ((𝜑 ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)) → 𝐶𝑉)
18 prssg 4290 . . . . . . 7 ((𝐵𝑉𝐶𝑉) → ((𝐵 ∈ (𝐼𝐾) ∧ 𝐶 ∈ (𝐼𝐾)) ↔ {𝐵, 𝐶} ⊆ (𝐼𝐾)))
197, 17, 18syl2an2r 872 . . . . . 6 ((𝜑 ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)) → ((𝐵 ∈ (𝐼𝐾) ∧ 𝐶 ∈ (𝐼𝐾)) ↔ {𝐵, 𝐶} ⊆ (𝐼𝐾)))
2015, 19mpbird 246 . . . . 5 ((𝜑 ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)) → (𝐵 ∈ (𝐼𝐾) ∧ 𝐶 ∈ (𝐼𝐾)))
2120simpld 474 . . . 4 ((𝜑 ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)) → 𝐵 ∈ (𝐼𝐾))
2221ex 449 . . 3 (𝜑 → ({𝐵, 𝐶} ⊆ (𝐼𝐾) → 𝐵 ∈ (𝐼𝐾)))
2314, 22anim12d 584 . 2 (𝜑 → (({𝐴, 𝐵} ⊆ (𝐼𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼𝐾)) → (𝐵 ∈ (𝐼𝐽) ∧ 𝐵 ∈ (𝐼𝐾))))
241, 23mpd 15 1 (𝜑 → (𝐵 ∈ (𝐼𝐽) ∧ 𝐵 ∈ (𝐼𝐾)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ⊆ wss 3540  {cpr 4127  ‘cfv 5804  ⟨“cs2 13437  ⟨“cs3 13438 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-sn 4126  df-pr 4128 This theorem is referenced by:  21wlkdlem7  41139
 Copyright terms: Public domain W3C validator