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

Theorem lhprelat3N 33575
 Description: The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 32947. (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
lhprelat3.b
lhprelat3.l
lhprelat3.s
lhprelat3.m
lhprelat3.c
lhprelat3.h
Assertion
Ref Expression
lhprelat3N
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem lhprelat3N
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpr 462 . . . . 5
2 simpll1 1044 . . . . . 6
3 lhprelat3.b . . . . . . . 8
4 eqid 2422 . . . . . . . 8
53, 4atbase 32825 . . . . . . 7
65adantl 467 . . . . . 6
7 eqid 2422 . . . . . . 7
8 lhprelat3.h . . . . . . 7
93, 7, 4, 8lhpoc2N 33550 . . . . . 6
102, 6, 9syl2anc 665 . . . . 5
111, 10mpbid 213 . . . 4
13 hlop 32898 . . . . . . . . 9
142, 13syl 17 . . . . . . . 8
15 hllat 32899 . . . . . . . . . 10
162, 15syl 17 . . . . . . . . 9
17 simpll3 1046 . . . . . . . . 9
183, 7opoccl 32730 . . . . . . . . . 10
1914, 6, 18syl2anc 665 . . . . . . . . 9
20 lhprelat3.m . . . . . . . . . 10
213, 20latmcl 16298 . . . . . . . . 9
2216, 17, 19, 21syl3anc 1264 . . . . . . . 8
23 lhprelat3.c . . . . . . . . 9
243, 7, 23cvrcon3b 32813 . . . . . . . 8
2514, 22, 17, 24syl3anc 1264 . . . . . . 7
26 hlol 32897 . . . . . . . . . 10
272, 26syl 17 . . . . . . . . 9
28 eqid 2422 . . . . . . . . . 10
293, 28, 20, 7oldmm3N 32755 . . . . . . . . 9
3027, 17, 6, 29syl3anc 1264 . . . . . . . 8
3130breq2d 4435 . . . . . . 7
3225, 31bitr2d 257 . . . . . 6
33 simpll2 1045 . . . . . . . 8
34 lhprelat3.l . . . . . . . . 9
353, 34, 7oplecon3b 32736 . . . . . . . 8
3614, 33, 22, 35syl3anc 1264 . . . . . . 7
3730breq1d 4433 . . . . . . 7
3836, 37bitr2d 257 . . . . . 6
3932, 38anbi12d 715 . . . . 5
4039biimpa 486 . . . 4
4140ancomd 452 . . 3
42 oveq2 6314 . . . . . 6
4342breq2d 4435 . . . . 5
4442breq1d 4433 . . . . 5
4543, 44anbi12d 715 . . . 4
4645rspcev 3182 . . 3
4712, 41, 46syl2anc 665 . 2
48 simpl1 1008 . . 3
4948, 13syl 17 . . . 4
50 simpl3 1010 . . . 4
513, 7opoccl 32730 . . . 4
5249, 50, 51syl2anc 665 . . 3
53 simpl2 1009 . . . 4
543, 7opoccl 32730 . . . 4
5549, 53, 54syl2anc 665 . . 3
56 simpr 462 . . . 4
57 lhprelat3.s . . . . . 6
583, 57, 7opltcon3b 32740 . . . . 5
5949, 53, 50, 58syl3anc 1264 . . . 4
6056, 59mpbid 213 . . 3
613, 34, 57, 28, 23, 4hlrelat3 32947 . . 3
6248, 52, 55, 60, 61syl31anc 1267 . 2
6347, 62r19.29a 2967 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  wrex 2772   class class class wbr 4423  cfv 5601  (class class class)co 6306  cbs 15121  cple 15197  coc 15198  cplt 16186  cjn 16189  cmee 16190  clat 16291  cops 32708  col 32710   ccvr 32798  catm 32799  chlt 32886  clh 33519 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-preset 16173  df-poset 16191  df-plt 16204  df-lub 16220  df-glb 16221  df-join 16222  df-meet 16223  df-p0 16285  df-p1 16286  df-lat 16292  df-clat 16354  df-oposet 32712  df-ol 32714  df-oml 32715  df-covers 32802  df-ats 32803  df-atl 32834  df-cvlat 32858  df-hlat 32887  df-lhyp 33523 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator