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	$⊢ (X \in V \land F : 𝒫 X ⟶ 𝒫 X) \to \{s \in 𝒫 X \| ⋃ F [𝒫 s \cap Fin] \subseteq s\} \in ACS (X)$

Proof

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

Metamath Proof Explorer

Theorem isacs1i

Proof