|   | Mathbox for Norm Megill | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > opoccl | Structured version Visualization version GIF version | ||
| Description: Closure of orthocomplement operation. (choccl 31325 analog.) (Contributed by NM, 20-Oct-2011.) | 
| Ref | Expression | 
|---|---|
| opoccl.b | ⊢ 𝐵 = (Base‘𝐾) | 
| opoccl.o | ⊢ ⊥ = (oc‘𝐾) | 
| Ref | Expression | 
|---|---|
| opoccl | ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | opoccl.b | . . . . 5 ⊢ 𝐵 = (Base‘𝐾) | |
| 2 | eqid 2737 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
| 3 | opoccl.o | . . . . 5 ⊢ ⊥ = (oc‘𝐾) | |
| 4 | eqid 2737 | . . . . 5 ⊢ (join‘𝐾) = (join‘𝐾) | |
| 5 | eqid 2737 | . . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
| 6 | eqid 2737 | . . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
| 7 | eqid 2737 | . . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
| 8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 39183 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) | 
| 9 | 8 | 3anidm23 1423 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) | 
| 10 | 9 | simp1d 1143 | . 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋)))) | 
| 11 | 10 | simp1d 1143 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 class class class wbr 5143 ‘cfv 6561 (class class class)co 7431 Basecbs 17247 lecple 17304 occoc 17305 joincjn 18357 meetcmee 18358 0.cp0 18468 1.cp1 18469 OPcops 39173 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-nul 5306 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-dm 5695 df-iota 6514 df-fv 6569 df-ov 7434 df-oposet 39177 | 
| This theorem is referenced by: opcon2b 39198 oplecon3b 39201 oplecon1b 39202 opoc1 39203 opltcon3b 39205 opltcon1b 39206 opltcon2b 39207 riotaocN 39210 oldmm1 39218 oldmm2 39219 oldmm3N 39220 oldmm4 39221 oldmj1 39222 oldmj2 39223 oldmj3 39224 oldmj4 39225 olm11 39228 latmassOLD 39230 omllaw2N 39245 omllaw4 39247 cmtcomlemN 39249 cmt2N 39251 cmt3N 39252 cmt4N 39253 cmtbr2N 39254 cmtbr3N 39255 cmtbr4N 39256 lecmtN 39257 omlfh1N 39259 omlfh3N 39260 omlspjN 39262 cvrcon3b 39278 cvrcmp2 39285 atlatmstc 39320 glbconN 39378 glbconNOLD 39379 glbconxN 39380 cvrexch 39422 1cvrco 39474 1cvratex 39475 1cvrjat 39477 polval2N 39908 polsubN 39909 2polpmapN 39915 2polvalN 39916 poldmj1N 39930 pmapj2N 39931 polatN 39933 2polatN 39934 pnonsingN 39935 ispsubcl2N 39949 polsubclN 39954 poml4N 39955 pmapojoinN 39970 pl42lem1N 39981 lhpoc2N 40017 lhpocnle 40018 lhpmod2i2 40040 lhpmod6i1 40041 lhprelat3N 40042 trlcl 40166 trlle 40186 docaclN 41126 doca2N 41128 djajN 41139 dih1 41288 dih1dimatlem 41331 dochcl 41355 dochvalr3 41365 doch2val2 41366 dochss 41367 dochocss 41368 dochoc 41369 dochnoncon 41393 djhlj 41403 | 
| Copyright terms: Public domain | W3C validator |