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 ⊢ ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ )
Assertion shintcli ∩ 𝐴 ∈ Sℋ

Proof

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