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 ) )
24 shaddcl
 |-  ( ( 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