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

Theorem cvlexch1 34418
 Description: An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)
Hypotheses
Ref Expression
cvlexch.b
cvlexch.l
cvlexch.j
cvlexch.a
Assertion
Ref Expression
cvlexch1

Proof of Theorem cvlexch1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvlexch.b . . . . . 6
2 cvlexch.l . . . . . 6
3 cvlexch.j . . . . . 6
4 cvlexch.a . . . . . 6
51, 2, 3, 4iscvlat 34413 . . . . 5
65simprbi 464 . . . 4
7 breq1 4455 . . . . . . . 8
87notbid 294 . . . . . . 7
9 breq1 4455 . . . . . . 7
108, 9anbi12d 710 . . . . . 6
11 oveq2 6302 . . . . . . 7
1211breq2d 4464 . . . . . 6
1310, 12imbi12d 320 . . . . 5
14 oveq2 6302 . . . . . . . 8
1514breq2d 4464 . . . . . . 7
1615anbi2d 703 . . . . . 6
17 breq1 4455 . . . . . 6
1816, 17imbi12d 320 . . . . 5
19 breq2 4456 . . . . . . . 8
2019notbid 294 . . . . . . 7
21 oveq1 6301 . . . . . . . 8
2221breq2d 4464 . . . . . . 7
2320, 22anbi12d 710 . . . . . 6
24 oveq1 6301 . . . . . . 7
2524breq2d 4464 . . . . . 6
2623, 25imbi12d 320 . . . . 5
2713, 18, 26rspc3v 3231 . . . 4
286, 27mpan9 469 . . 3
2928exp4b 607 . 2
30293imp 1190 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 369   w3a 973   wceq 1379   wcel 1767  wral 2817   class class class wbr 4452  cfv 5593  (class class class)co 6294  cbs 14502  cple 14574  cjn 15443  catm 34353  cal 34354  clc 34355 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6297  df-cvlat 34412 This theorem is referenced by:  cvlexch2  34419  cvlexchb1  34420  cvlexch3  34422  cvlcvr1  34429  hlexch1  34471
 Copyright terms: Public domain W3C validator