Description: Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pjocin.1 | |
|
pjocin.2 | |
||
Assertion | pjocini | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjocin.1 | |
|
2 | pjocin.2 | |
|
3 | 1 2 | chincli | |
4 | 3 | choccli | |
5 | 4 | cheli | |
6 | pjpo | |
|
7 | 1 5 6 | sylancr | |
8 | inss1 | |
|
9 | 3 1 | chsscon3i | |
10 | 8 9 | mpbi | |
11 | 1 | choccli | |
12 | 11 | pjcli | |
13 | 5 12 | syl | |
14 | 10 13 | sselid | |
15 | 4 | chshii | |
16 | shsubcl | |
|
17 | 15 16 | mp3an1 | |
18 | 14 17 | mpdan | |
19 | 7 18 | eqeltrd | |