# Metamath Proof Explorer

## Theorem shintcli

Description: Closure of intersection of a nonempty subset of SH . (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis shintcl.1
`|- ( A C_ SH /\ A =/= (/) )`
Assertion shintcli
`|- |^| A e. SH`

### Proof

Step Hyp Ref Expression
1 shintcl.1
` |-  ( A C_ SH /\ A =/= (/) )`
2 1 simpri
` |-  A =/= (/)`
3 n0
` |-  ( A =/= (/) <-> E. z z e. A )`
4 intss1
` |-  ( z e. A -> |^| A C_ z )`
5 1 simpli
` |-  A C_ SH`
6 5 sseli
` |-  ( z e. A -> z e. SH )`
7 shss
` |-  ( z e. SH -> z C_ ~H )`
8 6 7 syl
` |-  ( z e. A -> z C_ ~H )`
9 4 8 sstrd
` |-  ( z e. A -> |^| A C_ ~H )`
10 9 exlimiv
` |-  ( E. z z e. A -> |^| A C_ ~H )`
11 3 10 sylbi
` |-  ( A =/= (/) -> |^| A C_ ~H )`
12 2 11 ax-mp
` |-  |^| A C_ ~H`
13 ax-hv0cl
` |-  0h e. ~H`
14 13 elexi
` |-  0h e. _V`
15 14 elint2
` |-  ( 0h e. |^| A <-> A. z e. A 0h e. z )`
16 sh0
` |-  ( z e. SH -> 0h e. z )`
17 6 16 syl
` |-  ( z e. A -> 0h e. z )`
18 15 17 mprgbir
` |-  0h e. |^| A`
19 12 18 pm3.2i
` |-  ( |^| A C_ ~H /\ 0h e. |^| A )`
20 elinti
` |-  ( x e. |^| A -> ( z e. A -> x e. z ) )`
21 20 com12
` |-  ( z e. A -> ( x e. |^| A -> x e. z ) )`
22 elinti
` |-  ( y e. |^| A -> ( z e. A -> y e. z ) )`
23 22 com12
` |-  ( z e. A -> ( y e. |^| A -> y e. z ) )`
` |-  ( ( z e. SH /\ x e. z /\ y e. z ) -> ( x +h y ) e. z )`
25 6 24 syl3an1
` |-  ( ( z e. A /\ x e. z /\ y e. z ) -> ( x +h y ) e. z )`
26 25 3expib
` |-  ( z e. A -> ( ( x e. z /\ y e. z ) -> ( x +h y ) e. z ) )`
27 21 23 26 syl2and
` |-  ( z e. A -> ( ( x e. |^| A /\ y e. |^| A ) -> ( x +h y ) e. z ) )`
28 27 com12
` |-  ( ( x e. |^| A /\ y e. |^| A ) -> ( z e. A -> ( x +h y ) e. z ) )`
29 28 ralrimiv
` |-  ( ( x e. |^| A /\ y e. |^| A ) -> A. z e. A ( x +h y ) e. z )`
30 ovex
` |-  ( x +h y ) e. _V`
31 30 elint2
` |-  ( ( x +h y ) e. |^| A <-> A. z e. A ( x +h y ) e. z )`
32 29 31 sylibr
` |-  ( ( x e. |^| A /\ y e. |^| A ) -> ( x +h y ) e. |^| A )`
33 32 rgen2
` |-  A. x e. |^| A A. y e. |^| A ( x +h y ) e. |^| A`
34 shmulcl
` |-  ( ( z e. SH /\ x e. CC /\ y e. z ) -> ( x .h y ) e. z )`
35 6 34 syl3an1
` |-  ( ( z e. A /\ x e. CC /\ y e. z ) -> ( x .h y ) e. z )`
36 35 3expib
` |-  ( z e. A -> ( ( x e. CC /\ y e. z ) -> ( x .h y ) e. z ) )`
37 23 36 sylan2d
` |-  ( z e. A -> ( ( x e. CC /\ y e. |^| A ) -> ( x .h y ) e. z ) )`
38 37 com12
` |-  ( ( x e. CC /\ y e. |^| A ) -> ( z e. A -> ( x .h y ) e. z ) )`
39 38 ralrimiv
` |-  ( ( x e. CC /\ y e. |^| A ) -> A. z e. A ( x .h y ) e. z )`
40 ovex
` |-  ( x .h y ) e. _V`
41 40 elint2
` |-  ( ( x .h y ) e. |^| A <-> A. z e. A ( x .h y ) e. z )`
42 39 41 sylibr
` |-  ( ( x e. CC /\ y e. |^| A ) -> ( x .h y ) e. |^| A )`
43 42 rgen2
` |-  A. x e. CC A. y e. |^| A ( x .h y ) e. |^| A`
44 33 43 pm3.2i
` |-  ( A. x e. |^| A A. y e. |^| A ( x +h y ) e. |^| A /\ A. x e. CC A. y e. |^| A ( x .h y ) e. |^| A )`
45 issh2
` |-  ( |^| A e. SH <-> ( ( |^| A C_ ~H /\ 0h e. |^| A ) /\ ( A. x e. |^| A A. y e. |^| A ( x +h y ) e. |^| A /\ A. x e. CC A. y e. |^| A ( x .h y ) e. |^| A ) ) )`
46 19 44 45 mpbir2an
` |-  |^| A e. SH`