# Metamath Proof Explorer

## Theorem isacs3lem

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

Ref Expression
Assertion isacs3lem ${⊢}{C}\in \mathrm{ACS}\left({X}\right)\to \left({C}\in \mathrm{Moore}\left({X}\right)\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left(\mathrm{toInc}\left({s}\right)\in \mathrm{Dirset}\to \bigcup {s}\in {C}\right)\right)$

### Proof

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