# Metamath Proof Explorer

## Theorem ismre

Description: Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion ismre ${⊢}{C}\in \mathrm{Moore}\left({X}\right)↔\left({C}\subseteq 𝒫{X}\wedge {X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 elfvex ${⊢}{C}\in \mathrm{Moore}\left({X}\right)\to {X}\in \mathrm{V}$
2 elex ${⊢}{X}\in {C}\to {X}\in \mathrm{V}$
3 2 3ad2ant2 ${⊢}\left({C}\subseteq 𝒫{X}\wedge {X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\to {X}\in \mathrm{V}$
4 pweq ${⊢}{x}={X}\to 𝒫{x}=𝒫{X}$
5 4 pweqd ${⊢}{x}={X}\to 𝒫𝒫{x}=𝒫𝒫{X}$
6 eleq1 ${⊢}{x}={X}\to \left({x}\in {c}↔{X}\in {c}\right)$
7 6 anbi1d ${⊢}{x}={X}\to \left(\left({x}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)↔\left({X}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right)$
8 5 7 rabeqbidv ${⊢}{x}={X}\to \left\{{c}\in 𝒫𝒫{x}|\left({x}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}=\left\{{c}\in 𝒫𝒫{X}|\left({X}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}$
9 df-mre ${⊢}\mathrm{Moore}=\left({x}\in \mathrm{V}⟼\left\{{c}\in 𝒫𝒫{x}|\left({x}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}\right)$
10 vpwex ${⊢}𝒫{x}\in \mathrm{V}$
11 10 pwex ${⊢}𝒫𝒫{x}\in \mathrm{V}$
12 11 rabex ${⊢}\left\{{c}\in 𝒫𝒫{x}|\left({x}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}\in \mathrm{V}$
13 8 9 12 fvmpt3i ${⊢}{X}\in \mathrm{V}\to \mathrm{Moore}\left({X}\right)=\left\{{c}\in 𝒫𝒫{X}|\left({X}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}$
14 13 eleq2d ${⊢}{X}\in \mathrm{V}\to \left({C}\in \mathrm{Moore}\left({X}\right)↔{C}\in \left\{{c}\in 𝒫𝒫{X}|\left({X}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}\right)$
15 eleq2 ${⊢}{c}={C}\to \left({X}\in {c}↔{X}\in {C}\right)$
16 pweq ${⊢}{c}={C}\to 𝒫{c}=𝒫{C}$
17 eleq2 ${⊢}{c}={C}\to \left(\bigcap {s}\in {c}↔\bigcap {s}\in {C}\right)$
18 17 imbi2d ${⊢}{c}={C}\to \left(\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)↔\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)$
19 16 18 raleqbidv ${⊢}{c}={C}\to \left(\forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)↔\forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)$
20 15 19 anbi12d ${⊢}{c}={C}\to \left(\left({X}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)↔\left({X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)$
21 20 elrab ${⊢}{C}\in \left\{{c}\in 𝒫𝒫{X}|\left({X}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}↔\left({C}\in 𝒫𝒫{X}\wedge \left({X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)$
22 21 a1i ${⊢}{X}\in \mathrm{V}\to \left({C}\in \left\{{c}\in 𝒫𝒫{X}|\left({X}\in {c}\wedge \forall {s}\in 𝒫{c}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {c}\right)\right)\right\}↔\left({C}\in 𝒫𝒫{X}\wedge \left({X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)\right)$
23 pwexg ${⊢}{X}\in \mathrm{V}\to 𝒫{X}\in \mathrm{V}$
24 elpw2g ${⊢}𝒫{X}\in \mathrm{V}\to \left({C}\in 𝒫𝒫{X}↔{C}\subseteq 𝒫{X}\right)$
25 23 24 syl ${⊢}{X}\in \mathrm{V}\to \left({C}\in 𝒫𝒫{X}↔{C}\subseteq 𝒫{X}\right)$
26 25 anbi1d ${⊢}{X}\in \mathrm{V}\to \left(\left({C}\in 𝒫𝒫{X}\wedge \left({X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)↔\left({C}\subseteq 𝒫{X}\wedge \left({X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)\right)$
27 3anass ${⊢}\left({C}\subseteq 𝒫{X}\wedge {X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)↔\left({C}\subseteq 𝒫{X}\wedge \left({X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)$
28 26 27 syl6bbr ${⊢}{X}\in \mathrm{V}\to \left(\left({C}\in 𝒫𝒫{X}\wedge \left({X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)↔\left({C}\subseteq 𝒫{X}\wedge {X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)$
29 14 22 28 3bitrd ${⊢}{X}\in \mathrm{V}\to \left({C}\in \mathrm{Moore}\left({X}\right)↔\left({C}\subseteq 𝒫{X}\wedge {X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)\right)$
30 1 3 29 pm5.21nii ${⊢}{C}\in \mathrm{Moore}\left({X}\right)↔\left({C}\subseteq 𝒫{X}\wedge {X}\in {C}\wedge \forall {s}\in 𝒫{C}\phantom{\rule{.4em}{0ex}}\left({s}\ne \varnothing \to \bigcap {s}\in {C}\right)\right)$