# Metamath Proof Explorer

## Theorem acsfn1p

Description: Construction of a closure rule from a one-parameterpartial operation. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Assertion acsfn1p ${⊢}\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \left\{{a}\in 𝒫{X}|\forall {b}\in \left({a}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {a}\right\}\in \mathrm{ACS}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 riinrab ${⊢}𝒫{X}\cap \bigcap _{{b}\in {X}\cap {Y}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}=\left\{{a}\in 𝒫{X}|\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}$
2 elpwi ${⊢}{a}\in 𝒫{X}\to {a}\subseteq {X}$
3 2 ssrind ${⊢}{a}\in 𝒫{X}\to {a}\cap {Y}\subseteq {X}\cap {Y}$
4 3 adantl ${⊢}\left(\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\wedge {a}\in 𝒫{X}\right)\to {a}\cap {Y}\subseteq {X}\cap {Y}$
5 ralss ${⊢}{a}\cap {Y}\subseteq {X}\cap {Y}\to \left(\forall {b}\in \left({a}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {a}↔\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left({b}\in \left({a}\cap {Y}\right)\to {E}\in {a}\right)\right)$
6 4 5 syl ${⊢}\left(\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\wedge {a}\in 𝒫{X}\right)\to \left(\forall {b}\in \left({a}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {a}↔\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left({b}\in \left({a}\cap {Y}\right)\to {E}\in {a}\right)\right)$
7 inss2 ${⊢}{X}\cap {Y}\subseteq {Y}$
8 7 sseli ${⊢}{b}\in \left({X}\cap {Y}\right)\to {b}\in {Y}$
9 8 biantrud ${⊢}{b}\in \left({X}\cap {Y}\right)\to \left({b}\in {a}↔\left({b}\in {a}\wedge {b}\in {Y}\right)\right)$
10 vex ${⊢}{b}\in \mathrm{V}$
11 10 snss ${⊢}{b}\in {a}↔\left\{{b}\right\}\subseteq {a}$
12 11 bicomi ${⊢}\left\{{b}\right\}\subseteq {a}↔{b}\in {a}$
13 elin ${⊢}{b}\in \left({a}\cap {Y}\right)↔\left({b}\in {a}\wedge {b}\in {Y}\right)$
14 9 12 13 3bitr4g ${⊢}{b}\in \left({X}\cap {Y}\right)\to \left(\left\{{b}\right\}\subseteq {a}↔{b}\in \left({a}\cap {Y}\right)\right)$
15 14 imbi1d ${⊢}{b}\in \left({X}\cap {Y}\right)\to \left(\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)↔\left({b}\in \left({a}\cap {Y}\right)\to {E}\in {a}\right)\right)$
16 15 ralbiia ${⊢}\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)↔\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left({b}\in \left({a}\cap {Y}\right)\to {E}\in {a}\right)$
17 6 16 syl6rbbr ${⊢}\left(\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\wedge {a}\in 𝒫{X}\right)\to \left(\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)↔\forall {b}\in \left({a}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {a}\right)$
18 17 rabbidva ${⊢}\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \left\{{a}\in 𝒫{X}|\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}=\left\{{a}\in 𝒫{X}|\forall {b}\in \left({a}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {a}\right\}$
19 1 18 syl5eq ${⊢}\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to 𝒫{X}\cap \bigcap _{{b}\in {X}\cap {Y}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}=\left\{{a}\in 𝒫{X}|\forall {b}\in \left({a}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {a}\right\}$
20 mreacs ${⊢}{X}\in {V}\to \mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)$
21 20 adantr ${⊢}\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)$
22 ssralv ${⊢}{X}\cap {Y}\subseteq {Y}\to \left(\forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\to \forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)$
23 7 22 ax-mp ${⊢}\forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\to \forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {X}$
24 simpll ${⊢}\left(\left({X}\in {V}\wedge {b}\in \left({X}\cap {Y}\right)\right)\wedge {E}\in {X}\right)\to {X}\in {V}$
25 simpr ${⊢}\left(\left({X}\in {V}\wedge {b}\in \left({X}\cap {Y}\right)\right)\wedge {E}\in {X}\right)\to {E}\in {X}$
26 inss1 ${⊢}{X}\cap {Y}\subseteq {X}$
27 26 sseli ${⊢}{b}\in \left({X}\cap {Y}\right)\to {b}\in {X}$
28 27 ad2antlr ${⊢}\left(\left({X}\in {V}\wedge {b}\in \left({X}\cap {Y}\right)\right)\wedge {E}\in {X}\right)\to {b}\in {X}$
29 28 snssd ${⊢}\left(\left({X}\in {V}\wedge {b}\in \left({X}\cap {Y}\right)\right)\wedge {E}\in {X}\right)\to \left\{{b}\right\}\subseteq {X}$
30 snfi ${⊢}\left\{{b}\right\}\in \mathrm{Fin}$
31 30 a1i ${⊢}\left(\left({X}\in {V}\wedge {b}\in \left({X}\cap {Y}\right)\right)\wedge {E}\in {X}\right)\to \left\{{b}\right\}\in \mathrm{Fin}$
32 acsfn ${⊢}\left(\left({X}\in {V}\wedge {E}\in {X}\right)\wedge \left(\left\{{b}\right\}\subseteq {X}\wedge \left\{{b}\right\}\in \mathrm{Fin}\right)\right)\to \left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
33 24 25 29 31 32 syl22anc ${⊢}\left(\left({X}\in {V}\wedge {b}\in \left({X}\cap {Y}\right)\right)\wedge {E}\in {X}\right)\to \left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
34 33 ex ${⊢}\left({X}\in {V}\wedge {b}\in \left({X}\cap {Y}\right)\right)\to \left({E}\in {X}\to \left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)$
35 34 ralimdva ${⊢}{X}\in {V}\to \left(\forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {X}\to \forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)$
36 23 35 syl5 ${⊢}{X}\in {V}\to \left(\forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\to \forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)$
37 36 imp ${⊢}\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
38 mreriincl ${⊢}\left(\mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)\wedge \forall {b}\in \left({X}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)\to 𝒫{X}\cap \bigcap _{{b}\in {X}\cap {Y}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
39 21 37 38 syl2anc ${⊢}\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to 𝒫{X}\cap \bigcap _{{b}\in {X}\cap {Y}}\left\{{a}\in 𝒫{X}|\left(\left\{{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
40 19 39 eqeltrrd ${⊢}\left({X}\in {V}\wedge \forall {b}\in {Y}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \left\{{a}\in 𝒫{X}|\forall {b}\in \left({a}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}{E}\in {a}\right\}\in \mathrm{ACS}\left({X}\right)$