![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > opoccl | Structured version Visualization version Unicode version |
Description: Closure of orthocomplement operation. (choccl 26959 analog.) (Contributed by NM, 20-Oct-2011.) |
Ref | Expression |
---|---|
opoccl.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
opoccl.o |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
opoccl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opoccl.b |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqid 2451 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | opoccl.o |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | eqid 2451 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqid 2451 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | eqid 2451 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | eqid 2451 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 32748 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8 | 3anidm23 1327 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | simp1d 1020 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 10 | simp1d 1020 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-nul 4534 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-sbc 3268 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-br 4403 df-dm 4844 df-iota 5546 df-fv 5590 df-ov 6293 df-oposet 32742 |
This theorem is referenced by: opcon2b 32763 oplecon3b 32766 oplecon1b 32767 opoc1 32768 opltcon3b 32770 opltcon1b 32771 opltcon2b 32772 riotaocN 32775 oldmm1 32783 oldmm2 32784 oldmm3N 32785 oldmm4 32786 oldmj1 32787 oldmj2 32788 oldmj3 32789 oldmj4 32790 olm11 32793 latmassOLD 32795 omllaw2N 32810 omllaw4 32812 cmtcomlemN 32814 cmt2N 32816 cmt3N 32817 cmt4N 32818 cmtbr2N 32819 cmtbr3N 32820 cmtbr4N 32821 lecmtN 32822 omlfh1N 32824 omlfh3N 32825 omlspjN 32827 cvrcon3b 32843 cvrcmp2 32850 atlatmstc 32885 glbconN 32942 glbconxN 32943 cvrexch 32985 1cvrco 33037 1cvratex 33038 1cvrjat 33040 polval2N 33471 polsubN 33472 2polpmapN 33478 2polvalN 33479 poldmj1N 33493 pmapj2N 33494 polatN 33496 2polatN 33497 pnonsingN 33498 ispsubcl2N 33512 polsubclN 33517 poml4N 33518 pmapojoinN 33533 pl42lem1N 33544 lhpoc2N 33580 lhpocnle 33581 lhpmod2i2 33603 lhpmod6i1 33604 lhprelat3N 33605 trlcl 33730 trlle 33750 docaclN 34692 doca2N 34694 djajN 34705 dih1 34854 dih1dimatlem 34897 dochcl 34921 dochvalr3 34931 doch2val2 34932 dochss 34933 dochocss 34934 dochoc 34935 dochnoncon 34959 djhlj 34969 |
Copyright terms: Public domain | W3C validator |