This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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