# Metamath Proof Explorer

## Theorem acsfn2

Description: Algebraicity of a two-argument closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015)

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

### Proof

Step Hyp Ref Expression
1 elpwi ${⊢}{a}\in 𝒫{X}\to {a}\subseteq {X}$
2 ralss ${⊢}{a}\subseteq {X}\to \left(\forall {b}\in {a}\phantom{\rule{.4em}{0ex}}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}↔\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left({b}\in {a}\to \forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}\right)\right)$
3 ralss ${⊢}{a}\subseteq {X}\to \left(\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}\left({b}\in {a}\to {E}\in {a}\right)↔\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left({c}\in {a}\to \left({b}\in {a}\to {E}\in {a}\right)\right)\right)$
4 r19.21v ${⊢}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}\left({b}\in {a}\to {E}\in {a}\right)↔\left({b}\in {a}\to \forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}\right)$
5 impexp ${⊢}\left(\left({c}\in {a}\wedge {b}\in {a}\right)\to {E}\in {a}\right)↔\left({c}\in {a}\to \left({b}\in {a}\to {E}\in {a}\right)\right)$
6 vex ${⊢}{c}\in \mathrm{V}$
7 vex ${⊢}{b}\in \mathrm{V}$
8 6 7 prss ${⊢}\left({c}\in {a}\wedge {b}\in {a}\right)↔\left\{{c},{b}\right\}\subseteq {a}$
9 8 imbi1i ${⊢}\left(\left({c}\in {a}\wedge {b}\in {a}\right)\to {E}\in {a}\right)↔\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)$
10 5 9 bitr3i ${⊢}\left({c}\in {a}\to \left({b}\in {a}\to {E}\in {a}\right)\right)↔\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)$
11 10 ralbii ${⊢}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left({c}\in {a}\to \left({b}\in {a}\to {E}\in {a}\right)\right)↔\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)$
12 3 4 11 3bitr3g ${⊢}{a}\subseteq {X}\to \left(\left({b}\in {a}\to \forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}\right)↔\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right)$
13 12 ralbidv ${⊢}{a}\subseteq {X}\to \left(\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left({b}\in {a}\to \forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}\right)↔\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right)$
14 2 13 bitrd ${⊢}{a}\subseteq {X}\to \left(\forall {b}\in {a}\phantom{\rule{.4em}{0ex}}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}↔\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right)$
15 1 14 syl ${⊢}{a}\in 𝒫{X}\to \left(\forall {b}\in {a}\phantom{\rule{.4em}{0ex}}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}↔\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right)$
16 15 rabbiia ${⊢}\left\{{a}\in 𝒫{X}|\forall {b}\in {a}\phantom{\rule{.4em}{0ex}}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}\right\}=\left\{{a}\in 𝒫{X}|\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}$
17 riinrab ${⊢}𝒫{X}\cap \bigcap _{{b}\in {X}}\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}=\left\{{a}\in 𝒫{X}|\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}$
18 16 17 eqtr4i ${⊢}\left\{{a}\in 𝒫{X}|\forall {b}\in {a}\phantom{\rule{.4em}{0ex}}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}\right\}=𝒫{X}\cap \bigcap _{{b}\in {X}}\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}$
19 mreacs ${⊢}{X}\in {V}\to \mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)$
20 riinrab ${⊢}𝒫{X}\cap \bigcap _{{c}\in {X}}\left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}=\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}$
21 19 ad2antrr ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)$
22 simpll ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \left({c}\in {X}\wedge {E}\in {X}\right)\right)\to {X}\in {V}$
23 simprr ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \left({c}\in {X}\wedge {E}\in {X}\right)\right)\to {E}\in {X}$
24 prssi ${⊢}\left({c}\in {X}\wedge {b}\in {X}\right)\to \left\{{c},{b}\right\}\subseteq {X}$
25 24 ancoms ${⊢}\left({b}\in {X}\wedge {c}\in {X}\right)\to \left\{{c},{b}\right\}\subseteq {X}$
26 25 ad2ant2lr ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \left({c}\in {X}\wedge {E}\in {X}\right)\right)\to \left\{{c},{b}\right\}\subseteq {X}$
27 prfi ${⊢}\left\{{c},{b}\right\}\in \mathrm{Fin}$
28 27 a1i ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \left({c}\in {X}\wedge {E}\in {X}\right)\right)\to \left\{{c},{b}\right\}\in \mathrm{Fin}$
29 acsfn ${⊢}\left(\left({X}\in {V}\wedge {E}\in {X}\right)\wedge \left(\left\{{c},{b}\right\}\subseteq {X}\wedge \left\{{c},{b}\right\}\in \mathrm{Fin}\right)\right)\to \left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
30 22 23 26 28 29 syl22anc ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \left({c}\in {X}\wedge {E}\in {X}\right)\right)\to \left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
31 30 expr ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge {c}\in {X}\right)\to \left({E}\in {X}\to \left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)$
32 31 ralimdva ${⊢}\left({X}\in {V}\wedge {b}\in {X}\right)\to \left(\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\to \forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)$
33 32 imp ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
34 mreriincl ${⊢}\left(\mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)\wedge \forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)\to 𝒫{X}\cap \bigcap _{{c}\in {X}}\left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
35 21 33 34 syl2anc ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to 𝒫{X}\cap \bigcap _{{c}\in {X}}\left\{{a}\in 𝒫{X}|\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
36 20 35 eqeltrrid ${⊢}\left(\left({X}\in {V}\wedge {b}\in {X}\right)\wedge \forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
37 36 ex ${⊢}\left({X}\in {V}\wedge {b}\in {X}\right)\to \left(\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\to \left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)$
38 37 ralimdva ${⊢}{X}\in {V}\to \left(\forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\to \forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)$
39 38 imp ${⊢}\left({X}\in {V}\wedge \forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
40 mreriincl ${⊢}\left(\mathrm{ACS}\left({X}\right)\in \mathrm{Moore}\left(𝒫{X}\right)\wedge \forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)\right)\to 𝒫{X}\cap \bigcap _{{b}\in {X}}\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
41 19 39 40 syl2an2r ${⊢}\left({X}\in {V}\wedge \forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to 𝒫{X}\cap \bigcap _{{b}\in {X}}\left\{{a}\in 𝒫{X}|\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left\{{c},{b}\right\}\subseteq {a}\to {E}\in {a}\right)\right\}\in \mathrm{ACS}\left({X}\right)$
42 18 41 eqeltrid ${⊢}\left({X}\in {V}\wedge \forall {b}\in {X}\phantom{\rule{.4em}{0ex}}\forall {c}\in {X}\phantom{\rule{.4em}{0ex}}{E}\in {X}\right)\to \left\{{a}\in 𝒫{X}|\forall {b}\in {a}\phantom{\rule{.4em}{0ex}}\forall {c}\in {a}\phantom{\rule{.4em}{0ex}}{E}\in {a}\right\}\in \mathrm{ACS}\left({X}\right)$