| 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 31208 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 2729 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
| 3 | opoccl.o | . . . . 5 ⊢ ⊥ = (oc‘𝐾) | |
| 4 | eqid 2729 | . . . . 5 ⊢ (join‘𝐾) = (join‘𝐾) | |
| 5 | eqid 2729 | . . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
| 6 | eqid 2729 | . . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
| 7 | eqid 2729 | . . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
| 8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 39148 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
| 9 | 8 | 3anidm23 1423 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
| 10 | 9 | simp1d 1142 | . 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋)))) |
| 11 | 10 | simp1d 1142 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 Basecbs 17155 lecple 17203 occoc 17204 joincjn 18248 meetcmee 18249 0.cp0 18358 1.cp1 18359 OPcops 39138 |
| 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 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-nul 5256 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ne 2926 df-ral 3045 df-rab 3403 df-v 3446 df-dif 3914 df-un 3916 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-dm 5641 df-iota 6452 df-fv 6507 df-ov 7372 df-oposet 39142 |
| This theorem is referenced by: opcon2b 39163 oplecon3b 39166 oplecon1b 39167 opoc1 39168 opltcon3b 39170 opltcon1b 39171 opltcon2b 39172 riotaocN 39175 oldmm1 39183 oldmm2 39184 oldmm3N 39185 oldmm4 39186 oldmj1 39187 oldmj2 39188 oldmj3 39189 oldmj4 39190 olm11 39193 latmassOLD 39195 omllaw2N 39210 omllaw4 39212 cmtcomlemN 39214 cmt2N 39216 cmt3N 39217 cmt4N 39218 cmtbr2N 39219 cmtbr3N 39220 cmtbr4N 39221 lecmtN 39222 omlfh1N 39224 omlfh3N 39225 omlspjN 39227 cvrcon3b 39243 cvrcmp2 39250 atlatmstc 39285 glbconN 39343 glbconNOLD 39344 glbconxN 39345 cvrexch 39387 1cvrco 39439 1cvratex 39440 1cvrjat 39442 polval2N 39873 polsubN 39874 2polpmapN 39880 2polvalN 39881 poldmj1N 39895 pmapj2N 39896 polatN 39898 2polatN 39899 pnonsingN 39900 ispsubcl2N 39914 polsubclN 39919 poml4N 39920 pmapojoinN 39935 pl42lem1N 39946 lhpoc2N 39982 lhpocnle 39983 lhpmod2i2 40005 lhpmod6i1 40006 lhprelat3N 40007 trlcl 40131 trlle 40151 docaclN 41091 doca2N 41093 djajN 41104 dih1 41253 dih1dimatlem 41296 dochcl 41320 dochvalr3 41330 doch2val2 41331 dochss 41332 dochocss 41333 dochoc 41334 dochnoncon 41358 djhlj 41368 |
| Copyright terms: Public domain | W3C validator |