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 \subseteq S_{ℋ} \land A \neq \emptyset)$
	Assertion	shintcli	$⊢ ⋂ A \in S_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		shintcl.1	$⊢ (A \subseteq S_{ℋ} \land A \neq \emptyset)$
2	1	simpri	$⊢ A \neq \emptyset$
3		n0	$⊢ A \neq \emptyset \leftrightarrow \exists z z \in A$
4		intss1	$⊢ z \in A \to ⋂ A \subseteq z$
5	1	simpli	$⊢ A \subseteq S_{ℋ}$
6	5	sseli	$⊢ z \in A \to z \in S_{ℋ}$
7		shss	$⊢ z \in S_{ℋ} \to z \subseteq ℋ$
8	6 7	syl	$⊢ z \in A \to z \subseteq ℋ$
9	4 8	sstrd	$⊢ z \in A \to ⋂ A \subseteq ℋ$
10	9	exlimiv	$⊢ \exists z z \in A \to ⋂ A \subseteq ℋ$
11	3 10	sylbi	$⊢ A \neq \emptyset \to ⋂ A \subseteq ℋ$
12	2 11	ax-mp	$⊢ ⋂ A \subseteq ℋ$
13		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
14	13	elexi	$⊢ 0_{ℎ} \in V$
15	14	elint2	$⊢ 0_{ℎ} \in ⋂ A \leftrightarrow \forall z \in A 0_{ℎ} \in z$
16		sh0	$⊢ z \in S_{ℋ} \to 0_{ℎ} \in z$
17	6 16	syl	$⊢ z \in A \to 0_{ℎ} \in z$
18	15 17	mprgbir	$⊢ 0_{ℎ} \in ⋂ A$
19	12 18	pm3.2i	$⊢ (⋂ A \subseteq ℋ \land 0_{ℎ} \in ⋂ A)$
20		elinti	$⊢ x \in ⋂ A \to (z \in A \to x \in z)$
21	20	com12	$⊢ z \in A \to (x \in ⋂ A \to x \in z)$
22		elinti	$⊢ y \in ⋂ A \to (z \in A \to y \in z)$
23	22	com12	$⊢ z \in A \to (y \in ⋂ A \to y \in z)$
24		shaddcl	$⊢ (z \in S_{ℋ} \land x \in z \land y \in z) \to x +_{ℎ} y \in z$
25	6 24	syl3an1	$⊢ (z \in A \land x \in z \land y \in z) \to x +_{ℎ} y \in z$
26	25	3expib	$⊢ z \in A \to ((x \in z \land y \in z) \to x +_{ℎ} y \in z)$
27	21 23 26	syl2and	$⊢ z \in A \to ((x \in ⋂ A \land y \in ⋂ A) \to x +_{ℎ} y \in z)$
28	27	com12	$⊢ (x \in ⋂ A \land y \in ⋂ A) \to (z \in A \to x +_{ℎ} y \in z)$
29	28	ralrimiv	$⊢ (x \in ⋂ A \land y \in ⋂ A) \to \forall z \in A x +_{ℎ} y \in z$
30		ovex	$⊢ x +_{ℎ} y \in V$
31	30	elint2	$⊢ x +_{ℎ} y \in ⋂ A \leftrightarrow \forall z \in A x +_{ℎ} y \in z$
32	29 31	sylibr	$⊢ (x \in ⋂ A \land y \in ⋂ A) \to x +_{ℎ} y \in ⋂ A$
33	32	rgen2	$⊢ \forall x \in ⋂ A \forall y \in ⋂ A x +_{ℎ} y \in ⋂ A$
34		shmulcl	$⊢ (z \in S_{ℋ} \land x \in ℂ \land y \in z) \to x \cdot_{ℎ} y \in z$
35	6 34	syl3an1	$⊢ (z \in A \land x \in ℂ \land y \in z) \to x \cdot_{ℎ} y \in z$
36	35	3expib	$⊢ z \in A \to ((x \in ℂ \land y \in z) \to x \cdot_{ℎ} y \in z)$
37	23 36	sylan2d	$⊢ z \in A \to ((x \in ℂ \land y \in ⋂ A) \to x \cdot_{ℎ} y \in z)$
38	37	com12	$⊢ (x \in ℂ \land y \in ⋂ A) \to (z \in A \to x \cdot_{ℎ} y \in z)$
39	38	ralrimiv	$⊢ (x \in ℂ \land y \in ⋂ A) \to \forall z \in A x \cdot_{ℎ} y \in z$
40		ovex	$⊢ x \cdot_{ℎ} y \in V$
41	40	elint2	$⊢ x \cdot_{ℎ} y \in ⋂ A \leftrightarrow \forall z \in A x \cdot_{ℎ} y \in z$
42	39 41	sylibr	$⊢ (x \in ℂ \land y \in ⋂ A) \to x \cdot_{ℎ} y \in ⋂ A$
43	42	rgen2	$⊢ \forall x \in ℂ \forall y \in ⋂ A x \cdot_{ℎ} y \in ⋂ A$
44	33 43	pm3.2i	$⊢ (\forall x \in ⋂ A \forall y \in ⋂ A x +_{ℎ} y \in ⋂ A \land \forall x \in ℂ \forall y \in ⋂ A x \cdot_{ℎ} y \in ⋂ A)$
45		issh2	$⊢ ⋂ A \in S_{ℋ} \leftrightarrow ((⋂ A \subseteq ℋ \land 0_{ℎ} \in ⋂ A) \land (\forall x \in ⋂ A \forall y \in ⋂ A x +_{ℎ} y \in ⋂ A \land \forall x \in ℂ \forall y \in ⋂ A x \cdot_{ℎ} y \in ⋂ A))$
46	19 44 45	mpbir2an	$⊢ ⋂ A \in S_{ℋ}$

Metamath Proof Explorer

Theorem shintcli

Proof