isacs3lem

Description: An algebraic closure system satisfies isacs3 . (Contributed by Stefan O'Rear, 2-Apr-2015)

		Ref	Expression
	Assertion	isacs3lem	$⊢ C \in ACS (X) \to (C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C))$

Proof

Step	Hyp	Ref	Expression
1		acsmre	$⊢ C \in ACS (X) \to C \in Moore (X)$
2		mresspw	$⊢ C \in Moore (X) \to C \subseteq 𝒫 X$
3	1 2	syl	$⊢ C \in ACS (X) \to C \subseteq 𝒫 X$
4	3	sspwd	$⊢ C \in ACS (X) \to 𝒫 C \subseteq 𝒫 𝒫 X$
5	4	sselda	$⊢ (C \in ACS (X) \land s \in 𝒫 C) \to s \in 𝒫 𝒫 X$
6	5	elpwid	$⊢ (C \in ACS (X) \land s \in 𝒫 C) \to s \subseteq 𝒫 X$
7		sspwuni	$⊢ s \subseteq 𝒫 X \leftrightarrow ⋃ s \subseteq X$
8	6 7	sylib	$⊢ (C \in ACS (X) \land s \in 𝒫 C) \to ⋃ s \subseteq X$
9	8	adantr	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land toInc (s) \in Dirset) \to ⋃ s \subseteq X$
10		elinel1	$⊢ x \in (𝒫 ⋃ s \cap Fin) \to x \in 𝒫 ⋃ s$
11	10	elpwid	$⊢ x \in (𝒫 ⋃ s \cap Fin) \to x \subseteq ⋃ s$
12		elinel2	$⊢ x \in (𝒫 ⋃ s \cap Fin) \to x \in Fin$
13		fissuni	$⊢ (x \subseteq ⋃ s \land x \in Fin) \to \exists y \in (𝒫 s \cap Fin) x \subseteq ⋃ y$
14	11 12 13	syl2anc	$⊢ x \in (𝒫 ⋃ s \cap Fin) \to \exists y \in (𝒫 s \cap Fin) x \subseteq ⋃ y$
15	14	ad2antll	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \to \exists y \in (𝒫 s \cap Fin) x \subseteq ⋃ y$
16	1	ad3antrrr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to C \in Moore (X)$
17		eqid	$⊢ mrCls (C) = mrCls (C)$
18		simprr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to x \subseteq ⋃ y$
19		elinel1	$⊢ y \in (𝒫 s \cap Fin) \to y \in 𝒫 s$
20	19	elpwid	$⊢ y \in (𝒫 s \cap Fin) \to y \subseteq s$
21	20	unissd	$⊢ y \in (𝒫 s \cap Fin) \to ⋃ y \subseteq ⋃ s$
22	21	ad2antrl	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to ⋃ y \subseteq ⋃ s$
23	8	ad2antrr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to ⋃ s \subseteq X$
24	22 23	sstrd	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to ⋃ y \subseteq X$
25	16 17 18 24	mrcssd	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to mrCls (C) (x) \subseteq mrCls (C) (⋃ y)$
26		simpl	$⊢ (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin)) \to toInc (s) \in Dirset$
27	20	adantl	$⊢ (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin)) \to y \subseteq s$
28		elinel2	$⊢ y \in (𝒫 s \cap Fin) \to y \in Fin$
29	28	adantl	$⊢ (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin)) \to y \in Fin$
30		ipodrsfi	$⊢ (toInc (s) \in Dirset \land y \subseteq s \land y \in Fin) \to \exists x \in s ⋃ y \subseteq x$
31	26 27 29 30	syl3anc	$⊢ (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin)) \to \exists x \in s ⋃ y \subseteq x$
32	31	adantl	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \to \exists x \in s ⋃ y \subseteq x$
33	1	ad3antrrr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to C \in Moore (X)$
34		simprr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to ⋃ y \subseteq x$
35		elpwi	$⊢ s \in 𝒫 C \to s \subseteq C$
36	35	adantl	$⊢ (C \in ACS (X) \land s \in 𝒫 C) \to s \subseteq C$
37	36	ad2antrr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to s \subseteq C$
38		simprl	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to x \in s$
39	37 38	sseldd	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to x \in C$
40	17	mrcsscl	$⊢ (C \in Moore (X) \land ⋃ y \subseteq x \land x \in C) \to mrCls (C) (⋃ y) \subseteq x$
41	33 34 39 40	syl3anc	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to mrCls (C) (⋃ y) \subseteq x$
42		elssuni	$⊢ x \in s \to x \subseteq ⋃ s$
43	42	ad2antrl	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to x \subseteq ⋃ s$
44	41 43	sstrd	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \land (x \in s \land ⋃ y \subseteq x)) \to mrCls (C) (⋃ y) \subseteq ⋃ s$
45	32 44	rexlimddv	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land y \in (𝒫 s \cap Fin))) \to mrCls (C) (⋃ y) \subseteq ⋃ s$
46	45	anassrs	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land toInc (s) \in Dirset) \land y \in (𝒫 s \cap Fin)) \to mrCls (C) (⋃ y) \subseteq ⋃ s$
47	46	adantrr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land toInc (s) \in Dirset) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to mrCls (C) (⋃ y) \subseteq ⋃ s$
48	47	adantlrr	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to mrCls (C) (⋃ y) \subseteq ⋃ s$
49	25 48	sstrd	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \land (y \in (𝒫 s \cap Fin) \land x \subseteq ⋃ y)) \to mrCls (C) (x) \subseteq ⋃ s$
50	15 49	rexlimddv	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land (toInc (s) \in Dirset \land x \in (𝒫 ⋃ s \cap Fin))) \to mrCls (C) (x) \subseteq ⋃ s$
51	50	anassrs	$⊢ (((C \in ACS (X) \land s \in 𝒫 C) \land toInc (s) \in Dirset) \land x \in (𝒫 ⋃ s \cap Fin)) \to mrCls (C) (x) \subseteq ⋃ s$
52	51	ralrimiva	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land toInc (s) \in Dirset) \to \forall x \in (𝒫 ⋃ s \cap Fin) mrCls (C) (x) \subseteq ⋃ s$
53	17	acsfiel	$⊢ C \in ACS (X) \to (⋃ s \in C \leftrightarrow (⋃ s \subseteq X \land \forall x \in (𝒫 ⋃ s \cap Fin) mrCls (C) (x) \subseteq ⋃ s))$
54	53	ad2antrr	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land toInc (s) \in Dirset) \to (⋃ s \in C \leftrightarrow (⋃ s \subseteq X \land \forall x \in (𝒫 ⋃ s \cap Fin) mrCls (C) (x) \subseteq ⋃ s))$
55	9 52 54	mpbir2and	$⊢ ((C \in ACS (X) \land s \in 𝒫 C) \land toInc (s) \in Dirset) \to ⋃ s \in C$
56	55	ex	$⊢ (C \in ACS (X) \land s \in 𝒫 C) \to (toInc (s) \in Dirset \to ⋃ s \in C)$
57	56	ralrimiva	$⊢ C \in ACS (X) \to \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)$
58	1 57	jca	$⊢ C \in ACS (X) \to (C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C))$

Metamath Proof Explorer

Theorem isacs3lem

Proof