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 38104
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 38099 . . . . 5 (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝𝐴𝑞𝐴𝑥𝐵 ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝))))
65simprbi 498 . . . 4 (𝐾 ∈ CvLat → ∀𝑝𝐴𝑞𝐴𝑥𝐵 ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝)))
7 breq1 5147 . . . . . . . 8 (𝑝 = 𝑃 → (𝑝 𝑥𝑃 𝑥))
87notbid 318 . . . . . . 7 (𝑝 = 𝑃 → (¬ 𝑝 𝑥 ↔ ¬ 𝑃 𝑥))
9 breq1 5147 . . . . . . 7 (𝑝 = 𝑃 → (𝑝 (𝑥 𝑞) ↔ 𝑃 (𝑥 𝑞)))
108, 9anbi12d 632 . . . . . 6 (𝑝 = 𝑃 → ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) ↔ (¬ 𝑃 𝑥𝑃 (𝑥 𝑞))))
11 oveq2 7404 . . . . . . 7 (𝑝 = 𝑃 → (𝑥 𝑝) = (𝑥 𝑃))
1211breq2d 5156 . . . . . 6 (𝑝 = 𝑃 → (𝑞 (𝑥 𝑝) ↔ 𝑞 (𝑥 𝑃)))
1310, 12imbi12d 345 . . . . 5 (𝑝 = 𝑃 → (((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝)) ↔ ((¬ 𝑃 𝑥𝑃 (𝑥 𝑞)) → 𝑞 (𝑥 𝑃))))
14 oveq2 7404 . . . . . . . 8 (𝑞 = 𝑄 → (𝑥 𝑞) = (𝑥 𝑄))
1514breq2d 5156 . . . . . . 7 (𝑞 = 𝑄 → (𝑃 (𝑥 𝑞) ↔ 𝑃 (𝑥 𝑄)))
1615anbi2d 630 . . . . . 6 (𝑞 = 𝑄 → ((¬ 𝑃 𝑥𝑃 (𝑥 𝑞)) ↔ (¬ 𝑃 𝑥𝑃 (𝑥 𝑄))))
17 breq1 5147 . . . . . 6 (𝑞 = 𝑄 → (𝑞 (𝑥 𝑃) ↔ 𝑄 (𝑥 𝑃)))
1816, 17imbi12d 345 . . . . 5 (𝑞 = 𝑄 → (((¬ 𝑃 𝑥𝑃 (𝑥 𝑞)) → 𝑞 (𝑥 𝑃)) ↔ ((¬ 𝑃 𝑥𝑃 (𝑥 𝑄)) → 𝑄 (𝑥 𝑃))))
19 breq2 5148 . . . . . . . 8 (𝑥 = 𝑋 → (𝑃 𝑥𝑃 𝑋))
2019notbid 318 . . . . . . 7 (𝑥 = 𝑋 → (¬ 𝑃 𝑥 ↔ ¬ 𝑃 𝑋))
21 oveq1 7403 . . . . . . . 8 (𝑥 = 𝑋 → (𝑥 𝑄) = (𝑋 𝑄))
2221breq2d 5156 . . . . . . 7 (𝑥 = 𝑋 → (𝑃 (𝑥 𝑄) ↔ 𝑃 (𝑋 𝑄)))
2320, 22anbi12d 632 . . . . . 6 (𝑥 = 𝑋 → ((¬ 𝑃 𝑥𝑃 (𝑥 𝑄)) ↔ (¬ 𝑃 𝑋𝑃 (𝑋 𝑄))))
24 oveq1 7403 . . . . . . 7 (𝑥 = 𝑋 → (𝑥 𝑃) = (𝑋 𝑃))
2524breq2d 5156 . . . . . 6 (𝑥 = 𝑋 → (𝑄 (𝑥 𝑃) ↔ 𝑄 (𝑋 𝑃)))
2623, 25imbi12d 345 . . . . 5 (𝑥 = 𝑋 → (((¬ 𝑃 𝑥𝑃 (𝑥 𝑄)) → 𝑄 (𝑥 𝑃)) ↔ ((¬ 𝑃 𝑋𝑃 (𝑋 𝑄)) → 𝑄 (𝑋 𝑃))))
2713, 18, 26rspc3v 3625 . . . 4 ((𝑃𝐴𝑄𝐴𝑋𝐵) → (∀𝑝𝐴𝑞𝐴𝑥𝐵 ((¬ 𝑝 𝑥𝑝 (𝑥 𝑞)) → 𝑞 (𝑥 𝑝)) → ((¬ 𝑃 𝑋𝑃 (𝑋 𝑄)) → 𝑄 (𝑋 𝑃))))
286, 27mpan9 508 . . 3 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑋𝐵)) → ((¬ 𝑃 𝑋𝑃 (𝑋 𝑄)) → 𝑄 (𝑋 𝑃)))
2928exp4b 432 . 2 (𝐾 ∈ CvLat → ((𝑃𝐴𝑄𝐴𝑋𝐵) → (¬ 𝑃 𝑋 → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))))
30293imp 1112 1 ((𝐾 ∈ CvLat ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ ¬ 𝑃 𝑋) → (𝑃 (𝑋 𝑄) → 𝑄 (𝑋 𝑃)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3062   class class class wbr 5144  cfv 6535  (class class class)co 7396  Basecbs 17131  lecple 17191  joincjn 18251  Atomscatm 38039  AtLatcal 38040  CvLatclc 38041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-br 5145  df-iota 6487  df-fv 6543  df-ov 7399  df-cvlat 38098
This theorem is referenced by:  cvlexch2  38105  cvlexchb1  38106  cvlexch3  38108  cvlcvr1  38115  hlexch1  38159
  Copyright terms: Public domain W3C validator