Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2polvalN Unicode version

Theorem 2polvalN 32995
Description: Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
2polval.u
2polval.a
2polval.m
2polval.p
Assertion
Ref Expression
2polvalN

Proof of Theorem 2polvalN
StepHypRef Expression
1 2polval.u . . . 4
2 eqid 2422 . . . 4
3 2polval.a . . . 4
4 2polval.m . . . 4
5 2polval.p . . . 4
61, 2, 3, 4, 5polval2N 32987 . . 3
76fveq2d 5665 . 2
8 hlop 32444 . . . . 5
98adantr 455 . . . 4
10 hlclat 32440 . . . . 5
11 eqid 2422 . . . . . . 7
1211, 3atssbase 32372 . . . . . 6
13 sstr 3341 . . . . . 6
1412, 13mpan2 656 . . . . 5
1511, 1clatlubcl 15222 . . . . 5
1610, 14, 15syl2an 467 . . . 4
1711, 2opoccl 32276 . . . 4
189, 16, 17syl2anc 646 . . 3
1911, 2, 4, 5polpmapN 32993 . . 3
2018, 19syldan 460 . 2
2111, 2opococ 32277 . . . 4
229, 16, 21syl2anc 646 . . 3
2322fveq2d 5665 . 2
247, 20, 233eqtrd 2458 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  =wceq 1687  e.wcel 1749  C_wss 3305  `cfv 5390   cbs 14114   coc 14186   club 15052   ccla 15217   cops 32254   catm 32345   chlt 32432   cpmap 32578   cpolN 32983
This theorem is referenced by:  2polssN  32996  3polN  32997  sspmaplubN  33006  2pmaplubN  33007  paddunN  33008  pnonsingN  33014  pmapidclN  33023  poml4N  33034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-riotaBAD 32041
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-iun 4148  df-iin 4149  df-br 4268  df-opab 4326  df-mpt 4327  df-id 4607  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-undef 6751  df-poset 15056  df-plt 15068  df-lub 15084  df-glb 15085  df-join 15086  df-meet 15087  df-p0 15149  df-p1 15150  df-lat 15156  df-clat 15218  df-oposet 32258  df-ol 32260  df-oml 32261  df-covers 32348  df-ats 32349  df-atl 32380  df-cvlat 32404  df-hlat 32433  df-pmap 32585  df-polarityN 32984
  Copyright terms: Public domain W3C validator