# 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 ⊆ S ℋ ∧ A ≠ ∅$
Assertion shintcli $⊢ ⋂ A ∈ S ℋ$

### Proof

Step Hyp Ref Expression
1 shintcl.1 $⊢ A ⊆ S ℋ ∧ A ≠ ∅$
2 1 simpri $⊢ A ≠ ∅$
3 n0 $⊢ A ≠ ∅ ↔ ∃ z z ∈ A$
4 intss1 $⊢ z ∈ A → ⋂ A ⊆ z$
5 1 simpli $⊢ A ⊆ S ℋ$
6 5 sseli $⊢ z ∈ A → z ∈ S ℋ$
7 shss $⊢ z ∈ S ℋ → z ⊆ ℋ$
8 6 7 syl $⊢ z ∈ A → z ⊆ ℋ$
9 4 8 sstrd $⊢ z ∈ A → ⋂ A ⊆ ℋ$
10 9 exlimiv $⊢ ∃ z z ∈ A → ⋂ A ⊆ ℋ$
11 3 10 sylbi $⊢ A ≠ ∅ → ⋂ A ⊆ ℋ$
12 2 11 ax-mp $⊢ ⋂ A ⊆ ℋ$
13 ax-hv0cl $⊢ 0 ℎ ∈ ℋ$
14 13 elexi $⊢ 0 ℎ ∈ V$
15 14 elint2 $⊢ 0 ℎ ∈ ⋂ A ↔ ∀ z ∈ A 0 ℎ ∈ z$
16 sh0 $⊢ z ∈ S ℋ → 0 ℎ ∈ z$
17 6 16 syl $⊢ z ∈ A → 0 ℎ ∈ z$
18 15 17 mprgbir $⊢ 0 ℎ ∈ ⋂ A$
19 12 18 pm3.2i $⊢ ⋂ A ⊆ ℋ ∧ 0 ℎ ∈ ⋂ A$
20 elinti $⊢ x ∈ ⋂ A → z ∈ A → x ∈ z$
21 20 com12 $⊢ z ∈ A → x ∈ ⋂ A → x ∈ z$
22 elinti $⊢ y ∈ ⋂ A → z ∈ A → y ∈ z$
23 22 com12 $⊢ z ∈ A → y ∈ ⋂ A → y ∈ z$
24 shaddcl $⊢ z ∈ S ℋ ∧ x ∈ z ∧ y ∈ z → x + ℎ y ∈ z$
25 6 24 syl3an1 $⊢ z ∈ A ∧ x ∈ z ∧ y ∈ z → x + ℎ y ∈ z$
26 25 3expib $⊢ z ∈ A → x ∈ z ∧ y ∈ z → x + ℎ y ∈ z$
27 21 23 26 syl2and $⊢ z ∈ A → x ∈ ⋂ A ∧ y ∈ ⋂ A → x + ℎ y ∈ z$
28 27 com12 $⊢ x ∈ ⋂ A ∧ y ∈ ⋂ A → z ∈ A → x + ℎ y ∈ z$
29 28 ralrimiv $⊢ x ∈ ⋂ A ∧ y ∈ ⋂ A → ∀ z ∈ A x + ℎ y ∈ z$
30 ovex $⊢ x + ℎ y ∈ V$
31 30 elint2 $⊢ x + ℎ y ∈ ⋂ A ↔ ∀ z ∈ A x + ℎ y ∈ z$
32 29 31 sylibr $⊢ x ∈ ⋂ A ∧ y ∈ ⋂ A → x + ℎ y ∈ ⋂ A$
33 32 rgen2 $⊢ ∀ x ∈ ⋂ A ∀ y ∈ ⋂ A x + ℎ y ∈ ⋂ A$
34 shmulcl $⊢ z ∈ S ℋ ∧ x ∈ ℂ ∧ y ∈ z → x ⋅ ℎ y ∈ z$
35 6 34 syl3an1 $⊢ z ∈ A ∧ x ∈ ℂ ∧ y ∈ z → x ⋅ ℎ y ∈ z$
36 35 3expib $⊢ z ∈ A → x ∈ ℂ ∧ y ∈ z → x ⋅ ℎ y ∈ z$
37 23 36 sylan2d $⊢ z ∈ A → x ∈ ℂ ∧ y ∈ ⋂ A → x ⋅ ℎ y ∈ z$
38 37 com12 $⊢ x ∈ ℂ ∧ y ∈ ⋂ A → z ∈ A → x ⋅ ℎ y ∈ z$
39 38 ralrimiv $⊢ x ∈ ℂ ∧ y ∈ ⋂ A → ∀ z ∈ A x ⋅ ℎ y ∈ z$
40 ovex $⊢ x ⋅ ℎ y ∈ V$
41 40 elint2 $⊢ x ⋅ ℎ y ∈ ⋂ A ↔ ∀ z ∈ A x ⋅ ℎ y ∈ z$
42 39 41 sylibr $⊢ x ∈ ℂ ∧ y ∈ ⋂ A → x ⋅ ℎ y ∈ ⋂ A$
43 42 rgen2 $⊢ ∀ x ∈ ℂ ∀ y ∈ ⋂ A x ⋅ ℎ y ∈ ⋂ A$
44 33 43 pm3.2i $⊢ ∀ x ∈ ⋂ A ∀ y ∈ ⋂ A x + ℎ y ∈ ⋂ A ∧ ∀ x ∈ ℂ ∀ y ∈ ⋂ A x ⋅ ℎ y ∈ ⋂ A$
45 issh2 $⊢ ⋂ A ∈ S ℋ ↔ ⋂ A ⊆ ℋ ∧ 0 ℎ ∈ ⋂ A ∧ ∀ x ∈ ⋂ A ∀ y ∈ ⋂ A x + ℎ y ∈ ⋂ A ∧ ∀ x ∈ ℂ ∀ y ∈ ⋂ A x ⋅ ℎ y ∈ ⋂ A$
46 19 44 45 mpbir2an $⊢ ⋂ A ∈ S ℋ$