Theorem isacs1i

Description: A closure system determined by a function is a closure system and algebraic. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	isacs1i	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\in \mathrm{ACS}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\subseteq 𝒫X$$
2	1	a1i	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\subseteq 𝒫X$$
3		pweq	$$⊢s=X\cap \bigcap t\to 𝒫s=𝒫\left(X\cap \bigcap t\right)$$
4	3	ineq1d	$$⊢s=X\cap \bigcap t\to 𝒫s\cap \mathrm{Fin}=𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}$$
5	4	imaeq2d	$$⊢s=X\cap \bigcap t\to F\left[𝒫s\cap \mathrm{Fin}\right]=F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]$$
6	5	unieqd	$$⊢s=X\cap \bigcap t\to \bigcup F\left[𝒫s\cap \mathrm{Fin}\right]=\bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]$$
7		id	$$⊢s=X\cap \bigcap t\to s=X\cap \bigcap t$$
8	6 7	sseq12d	$$⊢s=X\cap \bigcap t\to \left(\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\leftrightarrow \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq X\cap \bigcap t\right)$$
9		inss1	$$⊢X\cap \bigcap t\subseteq X$$
10		elpw2g	$$⊢X\in V\to \left(X\cap \bigcap t\in 𝒫X\leftrightarrow X\cap \bigcap t\subseteq X\right)$$
11	9 10	mpbiri	$$⊢X\in V\to X\cap \bigcap t\in 𝒫X$$
12	11	ad2antrr	$$⊢\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\to X\cap \bigcap t\in 𝒫X$$
13		imassrn	$$⊢F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq \mathrm{ran}F$$
14		frn	$$⊢F:𝒫X⟶𝒫X\to \mathrm{ran}F\subseteq 𝒫X$$
15	14	adantl	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \mathrm{ran}F\subseteq 𝒫X$$
16	13 15	sstrid	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq 𝒫X$$
17	16	unissd	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq \bigcup 𝒫X$$
18		unipw	$$⊢\bigcup 𝒫X=X$$
19	17 18	sseqtrdi	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq X$$
20	19	adantr	$$⊢\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\to \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq X$$
21		inss2	$$⊢X\cap \bigcap t\subseteq \bigcap t$$
22		intss1	$$⊢a\in t\to \bigcap t\subseteq a$$
23	21 22	sstrid	$$⊢a\in t\to X\cap \bigcap t\subseteq a$$
24	23	adantl	$$⊢\left(\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\wedge a\in t\right)\to X\cap \bigcap t\subseteq a$$
25	24	sspwd	$$⊢\left(\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\wedge a\in t\right)\to 𝒫\left(X\cap \bigcap t\right)\subseteq 𝒫a$$
26	25	ssrind	$$⊢\left(\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\wedge a\in t\right)\to 𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\subseteq 𝒫a\cap \mathrm{Fin}$$
27		imass2	$$⊢𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\subseteq 𝒫a\cap \mathrm{Fin}\to F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq F\left[𝒫a\cap \mathrm{Fin}\right]$$
28	26 27	syl	$$⊢\left(\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\wedge a\in t\right)\to F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq F\left[𝒫a\cap \mathrm{Fin}\right]$$
29	28	unissd	$$⊢\left(\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\wedge a\in t\right)\to \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq \bigcup F\left[𝒫a\cap \mathrm{Fin}\right]$$
30		ssel2	$$⊢\left(t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\wedge a\in t\right)\to a\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}$$
31		pweq	$$⊢s=a\to 𝒫s=𝒫a$$
32	31	ineq1d	$$⊢s=a\to 𝒫s\cap \mathrm{Fin}=𝒫a\cap \mathrm{Fin}$$
33	32	imaeq2d	$$⊢s=a\to F\left[𝒫s\cap \mathrm{Fin}\right]=F\left[𝒫a\cap \mathrm{Fin}\right]$$
34	33	unieqd	$$⊢s=a\to \bigcup F\left[𝒫s\cap \mathrm{Fin}\right]=\bigcup F\left[𝒫a\cap \mathrm{Fin}\right]$$
35		id	$$⊢s=a\to s=a$$
36	34 35	sseq12d	$$⊢s=a\to \left(\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\leftrightarrow \bigcup F\left[𝒫a\cap \mathrm{Fin}\right]\subseteq a\right)$$
37	36	elrab	$$⊢a\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \left(a\in 𝒫X\wedge \bigcup F\left[𝒫a\cap \mathrm{Fin}\right]\subseteq a\right)$$
38	37	simprbi	$$⊢a\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\to \bigcup F\left[𝒫a\cap \mathrm{Fin}\right]\subseteq a$$
39	30 38	syl	$$⊢\left(t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\wedge a\in t\right)\to \bigcup F\left[𝒫a\cap \mathrm{Fin}\right]\subseteq a$$
40	39	adantll	$$⊢\left(\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\wedge a\in t\right)\to \bigcup F\left[𝒫a\cap \mathrm{Fin}\right]\subseteq a$$
41	29 40	sstrd	$$⊢\left(\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\wedge a\in t\right)\to \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq a$$
42	41	ralrimiva	$$⊢\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\to \forall a\in t\bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq a$$
43		ssint	$$⊢\bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq \bigcap t\leftrightarrow \forall a\in t\bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq a$$
44	42 43	sylibr	$$⊢\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\to \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq \bigcap t$$
45	20 44	ssind	$$⊢\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\to \bigcup F\left[𝒫\left(X\cap \bigcap t\right)\cap \mathrm{Fin}\right]\subseteq X\cap \bigcap t$$
46	8 12 45	elrabd	$$⊢\left(\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\wedge t\subseteq \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\right)\to X\cap \bigcap t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}$$
47	2 46	ismred2	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\in \mathrm{Moore}\left(X\right)$$
48		fssxp	$$⊢F:𝒫X⟶𝒫X\to F\subseteq 𝒫X\times 𝒫X$$
49		pwexg	$$⊢X\in V\to 𝒫X\in \mathrm{V}$$
50	49 49	xpexd	$$⊢X\in V\to 𝒫X\times 𝒫X\in \mathrm{V}$$
51		ssexg	$$⊢\left(F\subseteq 𝒫X\times 𝒫X\wedge 𝒫X\times 𝒫X\in \mathrm{V}\right)\to F\in \mathrm{V}$$
52	48 50 51	syl2anr	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to F\in \mathrm{V}$$
53		simpr	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to F:𝒫X⟶𝒫X$$
54		pweq	$$⊢s=t\to 𝒫s=𝒫t$$
55	54	ineq1d	$$⊢s=t\to 𝒫s\cap \mathrm{Fin}=𝒫t\cap \mathrm{Fin}$$
56	55	imaeq2d	$$⊢s=t\to F\left[𝒫s\cap \mathrm{Fin}\right]=F\left[𝒫t\cap \mathrm{Fin}\right]$$
57	56	unieqd	$$⊢s=t\to \bigcup F\left[𝒫s\cap \mathrm{Fin}\right]=\bigcup F\left[𝒫t\cap \mathrm{Fin}\right]$$
58		id	$$⊢s=t\to s=t$$
59	57 58	sseq12d	$$⊢s=t\to \left(\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)$$
60	59	elrab3	$$⊢t\in 𝒫X\to \left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)$$
61	60	rgen	$$⊢\forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)$$
62	53 61	jctir	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \left(F:𝒫X⟶𝒫X\wedge \forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\right)$$
63		feq1	$$⊢f=F\to \left(f:𝒫X⟶𝒫X\leftrightarrow F:𝒫X⟶𝒫X\right)$$
64		imaeq1	$$⊢f=F\to f\left[𝒫t\cap \mathrm{Fin}\right]=F\left[𝒫t\cap \mathrm{Fin}\right]$$
65	64	unieqd	$$⊢f=F\to \bigcup f\left[𝒫t\cap \mathrm{Fin}\right]=\bigcup F\left[𝒫t\cap \mathrm{Fin}\right]$$
66	65	sseq1d	$$⊢f=F\to \left(\bigcup f\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)$$
67	66	bibi2d	$$⊢f=F\to \left(\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup f\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\leftrightarrow \left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\right)$$
68	67	ralbidv	$$⊢f=F\to \left(\forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup f\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\leftrightarrow \forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\right)$$
69	63 68	anbi12d	$$⊢f=F\to \left(\left(f:𝒫X⟶𝒫X\wedge \forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup f\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\right)\leftrightarrow \left(F:𝒫X⟶𝒫X\wedge \forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup F\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\right)\right)$$
70	52 62 69	spcedv	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \exists f\left(f:𝒫X⟶𝒫X\wedge \forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup f\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\right)$$
71		isacs	$$⊢\left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\in \mathrm{ACS}\left(X\right)\leftrightarrow \left(\left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\in \mathrm{Moore}\left(X\right)\wedge \exists f\left(f:𝒫X⟶𝒫X\wedge \forall t\in 𝒫X\left(t\in \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\leftrightarrow \bigcup f\left[𝒫t\cap \mathrm{Fin}\right]\subseteq t\right)\right)\right)$$
72	47 70 71	sylanbrc	$$⊢\left(X\in V\wedge F:𝒫X⟶𝒫X\right)\to \left\{s\in 𝒫X|\bigcup F\left[𝒫s\cap \mathrm{Fin}\right]\subseteq s\right\}\in \mathrm{ACS}\left(X\right)$$