Theorem shintcl 5294

Description: Closure of intersection of a non-empty subset of SH.

Hypothesis

Ref	Expression
shintcl.1	|- (A (_ SH /\ -. A = (/))

Assertion

Ref	Expression
shintcl	|- |^|A e. SH

Proof of Theorem shintcl

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

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196  E.wex 678   e. wel 803   = wceq 1091   e. wcel 1092  A.wral 1201   (_ wss 1487  (/)c0 1707  |^|cint 1965  (class class class)co 3001  CCcc 4026  H~chil 4958   +v cva 4959   .s csm 4960  0vc0v 4961  SHcsh 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