Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dochss Structured version   Unicode version

Theorem dochss 34845
 Description: Subset law for orthocomplement. (Contributed by NM, 16-Apr-2014.)
Hypotheses
Ref Expression
dochss.h
dochss.u
dochss.v
dochss.o
Assertion
Ref Expression
dochss

Proof of Theorem dochss
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp1l 1029 . . . . . 6
2 hlclat 32836 . . . . . 6
31, 2syl 17 . . . . 5
4 ssrab2 3489 . . . . . 6
54a1i 11 . . . . 5
6 simpll3 1046 . . . . . . . 8
7 simpr 462 . . . . . . . 8
86, 7sstrd 3417 . . . . . . 7
98ex 435 . . . . . 6
109ss2rabdv 3485 . . . . 5
11 eqid 2428 . . . . . 6
12 eqid 2428 . . . . . 6
13 eqid 2428 . . . . . 6
1411, 12, 13clatglbss 16316 . . . . 5
153, 5, 10, 14syl3anc 1264 . . . 4
16 hlop 32840 . . . . . 6
171, 16syl 17 . . . . 5
1811, 13clatglbcl 16303 . . . . . 6
193, 4, 18sylancl 666 . . . . 5
20 ssrab2 3489 . . . . . 6
2111, 13clatglbcl 16303 . . . . . 6
223, 20, 21sylancl 666 . . . . 5
23 eqid 2428 . . . . . 6
2411, 12, 23oplecon3b 32678 . . . . 5
2517, 19, 22, 24syl3anc 1264 . . . 4
2615, 25mpbid 213 . . 3
27 simp1 1005 . . . 4
2811, 23opoccl 32672 . . . . 5
2917, 22, 28syl2anc 665 . . . 4
3011, 23opoccl 32672 . . . . 5
3117, 19, 30syl2anc 665 . . . 4
32 dochss.h . . . . 5
33 eqid 2428 . . . . 5
3411, 12, 32, 33dihord 34744 . . . 4
3527, 29, 31, 34syl3anc 1264 . . 3
3626, 35mpbird 235 . 2
37 dochss.u . . . 4
38 dochss.v . . . 4
39 dochss.o . . . 4
4011, 13, 23, 32, 33, 37, 38, 39dochval 34831 . . 3