Description: Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | shincl.1 | |- A e. SH |
|
| shincl.2 | |- B e. SH |
||
| Assertion | shincli | |- ( A i^i B ) e. SH |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | shincl.1 | |- A e. SH |
|
| 2 | shincl.2 | |- B e. SH |
|
| 3 | 1 | elexi | |- A e. _V |
| 4 | 2 | elexi | |- B e. _V |
| 5 | 3 4 | intpr | |- |^| { A , B } = ( A i^i B ) |
| 6 | 1 2 | pm3.2i | |- ( A e. SH /\ B e. SH ) |
| 7 | 3 4 | prss | |- ( ( A e. SH /\ B e. SH ) <-> { A , B } C_ SH ) |
| 8 | 6 7 | mpbi | |- { A , B } C_ SH |
| 9 | 3 | prnz | |- { A , B } =/= (/) |
| 10 | 8 9 | pm3.2i | |- ( { A , B } C_ SH /\ { A , B } =/= (/) ) |
| 11 | 10 | shintcli | |- |^| { A , B } e. SH |
| 12 | 5 11 | eqeltrri | |- ( A i^i B ) e. SH |