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

Theorem cvlexch1 36506
Description: An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)
Hypotheses
Ref Expression
cvlexch.b 𝐵 = (Base‘𝐾)
cvlexch.l = (le‘𝐾)
cvlexch.j = (join‘𝐾)
cvlexch.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
cvlexch1 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))

Proof of Theorem cvlexch1
Dummy variables 𝑞 𝑝 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvlexch.b . . . . . 6 𝐵 = (Base‘𝐾)
2 cvlexch.l . . . . . 6 = (le‘𝐾)
3 cvlexch.j . . . . . 6 = (join‘𝐾)
4 cvlexch.a . . . . . 6 𝐴 = (Atoms‘𝐾)
51, 2, 3, 4iscvlat 36501 . . . . 5 (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝𝐴𝑞𝐴𝑥𝐵 ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝))))
65simprbi 500 . . . 4 (𝐾 ∈ CvLat → ∀𝑝𝐴𝑞𝐴𝑥𝐵 ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝)))
7 breq1 5042 . . . . . . . 8 (𝑝 = 𝑃 → (𝑝 𝑥𝑃 𝑥))
87notbid 321 . . . . . . 7 (𝑝 = 𝑃 → (¬ 𝑝 𝑥 ↔ ¬ 𝑃 𝑥))
9 breq1 5042 . . . . . . 7 (𝑝 = 𝑃 → (𝑝 (𝑥 𝑞) ↔ 𝑃 (𝑥 𝑞)))
108, 9anbi12d 633 . . . . . 6 (𝑝 = 𝑃 → ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) ↔ (¬ 𝑃 𝑥𝑃 (𝑥 𝑞))))
11 oveq2 7138 . . . . . . 7 (𝑝 = 𝑃 → (𝑥 𝑝) = (𝑥 𝑃))
1211breq2d 5051 . . . . . 6 (𝑝 = 𝑃 → (𝑞 (𝑥 𝑝) ↔ 𝑞 (𝑥 𝑃)))
1310, 12imbi12d 348 . . . . 5 (𝑝 = 𝑃 → (((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝)) ↔ ((¬ 𝑃 𝑥𝑃 (𝑥 𝑞)) → 𝑞 (𝑥 𝑃))))
14 oveq2 7138 . . . . . . . 8 (𝑞 = 𝑄 → (𝑥 𝑞) = (𝑥 𝑄))
1514breq2d 5051 . . . . . . 7 (𝑞 = 𝑄 → (𝑃 (𝑥 𝑞) ↔ 𝑃 (𝑥 𝑄)))
1615anbi2d 631 . . . . . 6 (𝑞 = 𝑄 → ((¬ 𝑃 𝑥𝑃 (𝑥 𝑞)) ↔ (¬ 𝑃 𝑥𝑃 (𝑥 𝑄))))
17 breq1 5042 . . . . . 6 (𝑞 = 𝑄 → (𝑞 (𝑥 𝑃) ↔ 𝑄 (𝑥 𝑃)))
1816, 17imbi12d 348 . . . . 5 (𝑞 = 𝑄 → (((¬ 𝑃 𝑥𝑃 (𝑥 𝑞)) → 𝑞 (𝑥 𝑃)) ↔ ((¬ 𝑃 𝑥𝑃 (𝑥 𝑄)) → 𝑄 (𝑥 𝑃))))
19 breq2 5043 . . . . . . . 8 (𝑥 = 𝑋 → (𝑃 𝑥𝑃 𝑋))
2019notbid 321 . . . . . . 7 (𝑥 = 𝑋 → (¬ 𝑃 𝑥 ↔ ¬ 𝑃 𝑋))
21 oveq1 7137 . . . . . . . 8 (𝑥 = 𝑋 → (𝑥 𝑄) = (𝑋 𝑄))
2221breq2d 5051 . . . . . . 7 (𝑥 = 𝑋 → (𝑃 (𝑥 𝑄) ↔ 𝑃 (𝑋 𝑄)))
2320, 22anbi12d 633 . . . . . 6 (𝑥 = 𝑋 → ((¬ 𝑃 𝑥𝑃 (𝑥 𝑄)) ↔ (¬ 𝑃 𝑋𝑃 (𝑋 𝑄))))
24 oveq1 7137 . . . . . . 7 (𝑥 = 𝑋 → (𝑥 𝑃) = (𝑋 𝑃))
2524breq2d 5051 . . . . . 6 (𝑥 = 𝑋 → (𝑄 (𝑥 𝑃) ↔ 𝑄 (𝑋 𝑃)))
2623, 25imbi12d 348 . . . . 5 (𝑥 = 𝑋 → (((¬ 𝑃 𝑥𝑃 (𝑥 𝑄)) → 𝑄 (𝑥 𝑃)) ↔ ((¬ 𝑃 𝑋𝑃 (𝑋 𝑄)) → 𝑄 (𝑋 𝑃))))
2713, 18, 26rspc3v 3613 . . . 4 ((𝑃𝐴𝑄𝐴𝑋𝐵) → (∀𝑝𝐴𝑞𝐴𝑥𝐵 ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝)) → ((¬ 𝑃 𝑋𝑃 (𝑋 𝑄)) → 𝑄 (𝑋 𝑃))))
286, 27mpan9 510 . . 3 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑋𝐵)) → ((¬ 𝑃 𝑋𝑃 (𝑋 𝑄)) → 𝑄 (𝑋 𝑃)))
2928exp4b 434 . 2 (𝐾 ∈ CvLat → ((𝑃𝐴𝑄𝐴𝑋𝐵) → (¬ 𝑃 𝑋 → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))))
30293imp 1108 1 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  wral 3126   class class class wbr 5039  cfv 6328  (class class class)co 7130  Basecbs 16462  lecple 16551  joincjn 17533  Atomscatm 36441  AtLatcal 36442  CvLatclc 36443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-iota 6287  df-fv 6336  df-ov 7133  df-cvlat 36500
This theorem is referenced by:  cvlexch2  36507  cvlexchb1  36508  cvlexch3  36510  cvlcvr1  36517  hlexch1  36560
  Copyright terms: Public domain W3C validator