Theorem choccli 31791

Description: Closure of C_ℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)

Hypothesis

Ref	Expression
choccl.1	⊢ 𝐴 ∈ Cℋ

Assertion

Ref	Expression
choccli	⊢ (⊥‘𝐴) ∈ Cℋ

Proof of Theorem choccli

Step	Hyp	Ref	Expression
1		choccl.1	. 2 ⊢ 𝐴 ∈ Cℋ
2		choccl 31790	. 2 ⊢ (𝐴 ∈ Cℋ → (⊥‘𝐴) ∈ Cℋ )
3	1, 2	ax-mp 5	1 ⊢ (⊥‘𝐴) ∈ Cℋ

This proof depends on syntax axioms:   ∈ wcel 2145  ‘cfv 6533   C_ℋ cch 31413  ⊥cort 31414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-inf2 9623  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205  ax-addf 11206  ax-mulf 11207  ax-hilex 31483  ax-hfvadd 31484  ax-hvcom 31485  ax-hvass 31486  ax-hv0cl 31487  ax-hvaddid 31488  ax-hfvmul 31489  ax-hvmulid 31490  ax-hvmulass 31491  ax-hvdistr1 31492  ax-hvdistr2 31493  ax-hvmul0 31494  ax-hfi 31563  ax-his1 31566  ax-his2 31567  ax-his3 31568  ax-his4 31569  ax-hcompl 31686

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7864  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8458  df-2o 8459  df-er 8699  df-map 8831  df-pm 8832  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9335  df-fi 9384  df-sup 9415  df-inf 9416  df-oi 9485  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-div 11899  df-nn 12261  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12532  df-z 12619  df-dec 12740  df-uz 12891  df-q 13001  df-rp 13046  df-xneg 13166  df-xadd 13167  df-xmul 13168  df-ioo 13405  df-icc 13408  df-fz 13565  df-fzo 13713  df-seq 14069  df-exp 14129  df-hash 14398  df-cj 15189  df-re 15190  df-im 15191  df-sqrt 15325  df-abs 15326  df-clim 15578  df-sum 15777  df-struct 17242  df-sets 17259  df-slot 17277  df-ndx 17289  df-base 17305  df-ress 17326  df-plusg 17358  df-mulr 17359  df-starv 17360  df-sca 17361  df-vsca 17362  df-ip 17363  df-tset 17364  df-ple 17365  df-ds 17367  df-unif 17368  df-hom 17369  df-cco 17370  df-rest 17510  df-topn 17511  df-0g 17529  df-gsum 17530  df-topgen 17531  df-pt 17532  df-prds 17535  df-xrs 17591  df-qtop 17596  df-imas 17597  df-xps 17599  df-mre 17673  df-mrc 17674  df-acs 17676  df-mgm 18733  df-sgrp 18824  df-mnd 18840  df-submnd 18895  df-mulg 19194  df-cntz 19447  df-cmn 19912  df-psmet 21580  df-xmet 21581  df-met 21582  df-bl 21583  df-mopn 21584  df-cnfld 21589  df-top 23122  df-topon 23139  df-topsp 23161  df-bases 23174  df-cn 23455  df-cnp 23456  df-lm 23457  df-haus 23543  df-tx 23791  df-hmeo 23984  df-xms 24549  df-ms 24550  df-tms 24551  df-cau 25487  df-grpo 30977  df-gid 30978  df-ginv 30979  df-gdiv 30980  df-ablo 31029  df-vc 31043  df-nv 31076  df-va 31079  df-ba 31080  df-sm 31081  df-0v 31082  df-vs 31083  df-nmcv 31084  df-ims 31085  df-dip 31185  df-hnorm 31452  df-hvsub 31455  df-hlim 31456  df-hcau 31457  df-sh 31691  df-ch 31705  df-oc 31736

This theorem is used by:  pjoc1i  31915  pjoc2i  31922  chsscon3i  31945  chsscon1i  31946  chdmm1i  31961  chdmm2i  31962  chdmm3i  31963  chdmm4i  31964  chdmj1i  31965  chdmj2i  31966  chdmj3i  31967  chdmj4i  31968  sshhococi  32030  h1de2bi  32038  h1de2ctlem  32039  h1de2ci  32040  spanunsni  32063  pjoml2i  32069  pjoml3i  32070  pjoml4i  32071  pjoml6i  32073  cmcmlem  32075  cmcm2i  32077  cmcm3i  32078  cmcm4i  32079  cmbr2i  32080  cmbr3i  32084  cmbr4i  32085  cm0  32093  fh3i  32107  fh4i  32108  cm2mi  32110  qlax5i  32115  qlaxr3i  32120  osumcori  32127  osumcor2i  32128  spansnji  32130  3oalem5  32150  3oalem6  32151  3oai  32152  pjcompi  32156  pjadjii  32158  pjaddii  32159  pjmulii  32161  pjss2i  32164  pjssmii  32165  pjssge0ii  32166  pjcji  32168  pjocini  32182  pjds3i  32197  pjnormi  32205  pjpythi  32206  pjneli  32207  mayetes3i  32213  riesz3i  32546  pjnormssi  32652  pjssdif2i  32658  pjssdif1i  32659  pjimai  32660  pjoccoi  32662  pjtoi  32663  pjoci  32664  pjclem1  32679  pjci  32684  hst0  32717  sto1i  32720  sto2i  32721  stlei  32724  stji1i  32726  golem1  32755  golem2  32756  goeqi  32757  stcltrlem1  32760  stcltrlem2  32761  mdsldmd1i  32815  hatomistici  32846  cvexchi  32853  atomli  32866  atordi  32868  chirredlem4  32877  chirredi  32878  mdsymi  32895  cmmdi  32900  cmdmdi  32901  mdoc1i  32909  mdoc2i  32910  dmdoc1i  32911  dmdoc2i  32912  mdcompli  32913  dmdcompli  32914  mddmdin0i  32915