Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3dim1lem5 Structured version   Visualization version   GIF version

Theorem 3dim1lem5 33569
Description: Lemma for 3dim1 33570. (Contributed by NM, 26-Jul-2012.)
Hypotheses
Ref Expression
3dim0.j = (join‘𝐾)
3dim0.l = (le‘𝐾)
3dim0.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
3dim1lem5 (((𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑤 ((𝑃 𝑢) 𝑣))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
Distinct variable groups:   𝑟,𝑞,𝑠,𝐴   ,𝑟,𝑠   𝑣,𝑢,𝑤,𝐴,𝑞   ,𝑞,𝑢,𝑣,𝑤   𝑢,𝐾,𝑣,𝑤   ,𝑞   𝑢,𝑟,𝑣,𝑤, ,𝑠   𝑃,𝑞,𝑟,𝑠,𝑢,𝑣,𝑤
Allowed substitution hints:   𝐾(𝑠,𝑟,𝑞)

Proof of Theorem 3dim1lem5
StepHypRef Expression
1 neeq2 2840 . . 3 (𝑞 = 𝑢 → (𝑃𝑞𝑃𝑢))
2 oveq2 6531 . . . . 5 (𝑞 = 𝑢 → (𝑃 𝑞) = (𝑃 𝑢))
32breq2d 4585 . . . 4 (𝑞 = 𝑢 → (𝑟 (𝑃 𝑞) ↔ 𝑟 (𝑃 𝑢)))
43notbid 306 . . 3 (𝑞 = 𝑢 → (¬ 𝑟 (𝑃 𝑞) ↔ ¬ 𝑟 (𝑃 𝑢)))
52oveq1d 6538 . . . . 5 (𝑞 = 𝑢 → ((𝑃 𝑞) 𝑟) = ((𝑃 𝑢) 𝑟))
65breq2d 4585 . . . 4 (𝑞 = 𝑢 → (𝑠 ((𝑃 𝑞) 𝑟) ↔ 𝑠 ((𝑃 𝑢) 𝑟)))
76notbid 306 . . 3 (𝑞 = 𝑢 → (¬ 𝑠 ((𝑃 𝑞) 𝑟) ↔ ¬ 𝑠 ((𝑃 𝑢) 𝑟)))
81, 4, 73anbi123d 1390 . 2 (𝑞 = 𝑢 → ((𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)) ↔ (𝑃𝑢 ∧ ¬ 𝑟 (𝑃 𝑢) ∧ ¬ 𝑠 ((𝑃 𝑢) 𝑟))))
9 breq1 4576 . . . 4 (𝑟 = 𝑣 → (𝑟 (𝑃 𝑢) ↔ 𝑣 (𝑃 𝑢)))
109notbid 306 . . 3 (𝑟 = 𝑣 → (¬ 𝑟 (𝑃 𝑢) ↔ ¬ 𝑣 (𝑃 𝑢)))
11 oveq2 6531 . . . . 5 (𝑟 = 𝑣 → ((𝑃 𝑢) 𝑟) = ((𝑃 𝑢) 𝑣))
1211breq2d 4585 . . . 4 (𝑟 = 𝑣 → (𝑠 ((𝑃 𝑢) 𝑟) ↔ 𝑠 ((𝑃 𝑢) 𝑣)))
1312notbid 306 . . 3 (𝑟 = 𝑣 → (¬ 𝑠 ((𝑃 𝑢) 𝑟) ↔ ¬ 𝑠 ((𝑃 𝑢) 𝑣)))
1410, 133anbi23d 1393 . 2 (𝑟 = 𝑣 → ((𝑃𝑢 ∧ ¬ 𝑟 (𝑃 𝑢) ∧ ¬ 𝑠 ((𝑃 𝑢) 𝑟)) ↔ (𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑠 ((𝑃 𝑢) 𝑣))))
15 breq1 4576 . . . 4 (𝑠 = 𝑤 → (𝑠 ((𝑃 𝑢) 𝑣) ↔ 𝑤 ((𝑃 𝑢) 𝑣)))
1615notbid 306 . . 3 (𝑠 = 𝑤 → (¬ 𝑠 ((𝑃 𝑢) 𝑣) ↔ ¬ 𝑤 ((𝑃 𝑢) 𝑣)))
17163anbi3d 1396 . 2 (𝑠 = 𝑤 → ((𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑠 ((𝑃 𝑢) 𝑣)) ↔ (𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑤 ((𝑃 𝑢) 𝑣))))
188, 14, 17rspc3ev 3292 1 (((𝑢𝐴𝑣𝐴𝑤𝐴) ∧ (𝑃𝑢 ∧ ¬ 𝑣 (𝑃 𝑢) ∧ ¬ 𝑤 ((𝑃 𝑢) 𝑣))) → ∃𝑞𝐴𝑟𝐴𝑠𝐴 (𝑃𝑞 ∧ ¬ 𝑟 (𝑃 𝑞) ∧ ¬ 𝑠 ((𝑃 𝑞) 𝑟)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1975  wne 2775  wrex 2892   class class class wbr 4573  cfv 5786  (class class class)co 6523  lecple 15717  joincjn 16709  Atomscatm 33367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-ov 6526
This theorem is referenced by:  3dim1  33570
  Copyright terms: Public domain W3C validator