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ℋ