Theorem shintcl 5294

Description: Closure of intersection of a non-empty subset of S_ℋ.

Hypothesis

Ref	Expression
shintcl.1	⊢ (A ⊆ Sℋ ∧ ¬ A = ∅)

Assertion

Ref	Expression
shintcl	⊢ ∩A ∈ Sℋ

Proof of Theorem shintcl

Step	Hyp	Ref	Expression
1		shintcl.1	. . . . . 6 ⊢ (A ⊆ Sℋ ∧ ¬ A = ∅)
2	1	pm3.27i 261	. . . . 5 ⊢ ¬ A = ∅
3		n0 1714	. . . . . 6 ⊢ (¬ A = ∅ ↔ ∃z z ∈ A)
4		intss1 1979	. . . . . . . 8 ⊢ (z ∈ A → ∩A ⊆ z)
5	1	pm3.26i 257	. . . . . . . . . 10 ⊢ A ⊆ Sℋ
6	5	sseli 1504	. . . . . . . . 9 ⊢ (z ∈ A → z ∈ Sℋ )
7		shss 5117	. . . . . . . . 9 ⊢ (z ∈ Sℋ → z ⊆ ℋ )
8	6, 7	syl 12	. . . . . . . 8 ⊢ (z ∈ A → z ⊆ ℋ )
9	4, 8	sstrd 1513	. . . . . . 7 ⊢ (z ∈ A → ∩A ⊆ ℋ )
10	9	19.23aiv 952	. . . . . 6 ⊢ (∃z z ∈ A → ∩A ⊆ ℋ )
11	3, 10	sylbi 174	. . . . 5 ⊢ (¬ A = ∅ → ∩A ⊆ ℋ )
12	2, 11	ax-mp 6	. . . 4 ⊢ ∩A ⊆ ℋ
13		ax-hvzercl 4987	. . . . . . 7 ⊢ 0v ∈ ℋ
14	13	elisseti 1355	. . . . . 6 ⊢ 0v ∈ V
15	14	elint2 1972	. . . . 5 ⊢ (0v ∈ ∩A ↔ ∀z ∈ A 0v ∈ z)
16		sh0 5122	. . . . . 6 ⊢ (z ∈ Sℋ → 0v ∈ z)
17	6, 16	syl 12	. . . . 5 ⊢ (z ∈ A → 0v ∈ z)
18	15, 17	mprgbir 1250	. . . 4 ⊢ 0v ∈ ∩A
19	12, 18	pm3.2i 234	. . 3 ⊢ (∩A ⊆ ℋ ∧ 0v ∈ ∩A)
20		elinti 1974	. . . . . . . . . . 11 ⊢ (x ∈ ∩A → (z ∈ A → x ∈ z))
21	20	com12 13	. . . . . . . . . 10 ⊢ (z ∈ A → (x ∈ ∩A → x ∈ z))
22		elinti 1974	. . . . . . . . . . 11 ⊢ (y ∈ ∩A → (z ∈ A → y ∈ z))
23	22	com12 13	. . . . . . . . . 10 ⊢ (z ∈ A → (y ∈ ∩A → y ∈ z))
24	21, 23	anim12d 431	. . . . . . . . 9 ⊢ (z ∈ A → ((x ∈ ∩A ∧ y ∈ ∩A) → (x ∈ z ∧ y ∈ z)))
25		shaddclt 5123	. . . . . . . . . 10 ⊢ (z ∈ Sℋ → ((x ∈ z ∧ y ∈ z) → (x +v y) ∈ z))
26	6, 25	syl 12	. . . . . . . . 9 ⊢ (z ∈ A → ((x ∈ z ∧ y ∈ z) → (x +v y) ∈ z))
27	24, 26	syld 27	. . . . . . . 8 ⊢ (z ∈ A → ((x ∈ ∩A ∧ y ∈ ∩A) → (x +v y) ∈ z))
28	27	com12 13	. . . . . . 7 ⊢ ((x ∈ ∩A ∧ y ∈ ∩A) → (z ∈ A → (x +v y) ∈ z))
29	28	r19.21aiv 1259	. . . . . 6 ⊢ ((x ∈ ∩A ∧ y ∈ ∩A) → ∀z ∈ A (x +v y) ∈ z)
30		oprex 3018	. . . . . . 7 ⊢ (x +v y) ∈ V
31	30	elint2 1972	. . . . . 6 ⊢ ((x +v y) ∈ ∩A ↔ ∀z ∈ A (x +v y) ∈ z)
32	29, 31	sylibr 175	. . . . 5 ⊢ ((x ∈ ∩A ∧ y ∈ ∩A) → (x +v y) ∈ ∩A)
33	32	rgen2 1248	. . . 4 ⊢ ∀x ∈ ∩ A∀y ∈ ∩ A(x +v y) ∈ ∩A
34	23	anim2d 433	. . . . . . . . 9 ⊢ (z ∈ A → ((x ∈ ℂ ∧ y ∈ ∩A) → (x ∈ ℂ ∧ y ∈ z)))
35		shmulclt 5124	. . . . . . . . . 10 ⊢ (z ∈ Sℋ → ((x ∈ ℂ ∧ y ∈ z) → (x ·s y) ∈ z))
36	6, 35	syl 12	. . . . . . . . 9 ⊢ (z ∈ A → ((x ∈ ℂ ∧ y ∈ z) → (x ·s y) ∈ z))
37	34, 36	syld 27	. . . . . . . 8 ⊢ (z ∈ A → ((x ∈ ℂ ∧ y ∈ ∩A) → (x ·s y) ∈ z))
38	37	com12 13	. . . . . . 7 ⊢ ((x ∈ ℂ ∧ y ∈ ∩A) → (z ∈ A → (x ·s y) ∈ z))
39	38	r19.21aiv 1259	. . . . . 6 ⊢ ((x ∈ ℂ ∧ y ∈ ∩A) → ∀z ∈ A (x ·s y) ∈ z)
40		oprex 3018	. . . . . . 7 ⊢ (x ·s y) ∈ V
41	40	elint2 1972	. . . . . 6 ⊢ ((x ·s y) ∈ ∩A ↔ ∀z ∈ A (x ·s y) ∈ z)
42	39, 41	sylibr 175	. . . . 5 ⊢ ((x ∈ ℂ ∧ y ∈ ∩A) → (x ·s y) ∈ ∩A)
43	42	rgen2a 1264	. . . 4 ⊢ ∀x ∈ ℂ ∀y ∈ ∩ A(x ·s y) ∈ ∩A
44	33, 43	pm3.2i 234	. . 3 ⊢ (∀x ∈ ∩ A∀y ∈ ∩ A(x +v y) ∈ ∩A ∧ ∀x ∈ ℂ ∀y ∈ ∩ A(x ·s y) ∈ ∩A)
45	19, 44	pm3.2i 234	. 2 ⊢ ((∩A ⊆ ℋ ∧ 0v ∈ ∩A) ∧ (∀x ∈ ∩ A∀y ∈ ∩ A(x +v y) ∈ ∩A ∧ ∀x ∈ ℂ ∀y ∈ ∩ A(x ·s y) ∈ ∩A))
46		sh 5116	. 2 ⊢ (∩A ∈ Sℋ ↔ ((∩A ⊆ ℋ ∧ 0v ∈ ∩A) ∧ (∀x ∈ ∩ A∀y ∈ ∩ A(x +v y) ∈ ∩A ∧ ∀x ∈ ℂ ∀y ∈ ∩ A(x ·s y) ∈ ∩A)))
47	45, 46	mpbir 165	1 ⊢ ∩A ∈ Sℋ

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∃wex 678   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201   ⊆ wss 1487  ∅c0 1707  ∩cint 1965  (class class class)co 3001  ℂcc 4026   ℋ chil 4958   +_v cva 4959   ·_s csm 4960  0_vc0v 4961   S_ℋ csh 4967

This theorem is referenced by:  shintclt 5295  chintcl 5296  shincl 5332

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-hilex 4983  ax-hvzercl 4987

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-int 1966  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438  df-opr 3003  df-sh 5114

metamath.org