Theorem mrisval

Description: Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mrisval.1	$$⊢N=\mathrm{mrCls}\left(A\right)$$
	mrisval.2	$$⊢I=\mathrm{mrInd}\left(A\right)$$
Assertion	mrisval	$$⊢A\in \mathrm{Moore}\left(X\right)\to I=\left\{s\in 𝒫X|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mrisval.1	$$⊢N=\mathrm{mrCls}\left(A\right)$$
2		mrisval.2	$$⊢I=\mathrm{mrInd}\left(A\right)$$
3		fvssunirn	$$⊢\mathrm{Moore}\left(X\right)\subseteq \bigcup \mathrm{ran}\mathrm{Moore}$$
4	3	sseli	$$⊢A\in \mathrm{Moore}\left(X\right)\to A\in \bigcup \mathrm{ran}\mathrm{Moore}$$
5		unieq	$$⊢c=A\to \bigcup c=\bigcup A$$
6	5	pweqd	$$⊢c=A\to 𝒫\bigcup c=𝒫\bigcup A$$
7		fveq2	$$⊢c=A\to \mathrm{mrCls}\left(c\right)=\mathrm{mrCls}\left(A\right)$$
8	7 1	eqtr4di	$$⊢c=A\to \mathrm{mrCls}\left(c\right)=N$$
9	8	fveq1d	$$⊢c=A\to \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)=N\left(s\setminus \left\{x\right\}\right)$$
10	9	eleq2d	$$⊢c=A\to \left(x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\leftrightarrow x\in N\left(s\setminus \left\{x\right\}\right)\right)$$
11	10	notbid	$$⊢c=A\to \left(\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\leftrightarrow \neg x\in N\left(s\setminus \left\{x\right\}\right)\right)$$
12	11	ralbidv	$$⊢c=A\to \left(\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\leftrightarrow \forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right)$$
13	6 12	rabeqbidv	$$⊢c=A\to \left\{s\in 𝒫\bigcup c|\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\right\}=\left\{s\in 𝒫\bigcup A|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}$$
14		df-mri	$$⊢\mathrm{mrInd}=\left(c\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left\{s\in 𝒫\bigcup c|\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\right\}\right)$$
15		vuniex	$$⊢\bigcup c\in \mathrm{V}$$
16	15	pwex	$$⊢𝒫\bigcup c\in \mathrm{V}$$
17	16	rabex	$$⊢\left\{s\in 𝒫\bigcup c|\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\right\}\in \mathrm{V}$$
18	13 14 17	fvmpt3i	$$⊢A\in \bigcup \mathrm{ran}\mathrm{Moore}\to \mathrm{mrInd}\left(A\right)=\left\{s\in 𝒫\bigcup A|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}$$
19	4 18	syl	$$⊢A\in \mathrm{Moore}\left(X\right)\to \mathrm{mrInd}\left(A\right)=\left\{s\in 𝒫\bigcup A|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}$$
20	2 19	eqtrid	$$⊢A\in \mathrm{Moore}\left(X\right)\to I=\left\{s\in 𝒫\bigcup A|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}$$
21		mreuni	$$⊢A\in \mathrm{Moore}\left(X\right)\to \bigcup A=X$$
22	21	pweqd	$$⊢A\in \mathrm{Moore}\left(X\right)\to 𝒫\bigcup A=𝒫X$$
23	22	rabeqdv	$$⊢A\in \mathrm{Moore}\left(X\right)\to \left\{s\in 𝒫\bigcup A|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}=\left\{s\in 𝒫X|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}$$
24	20 23	eqtrd	$$⊢A\in \mathrm{Moore}\left(X\right)\to I=\left\{s\in 𝒫X|\forall x\in s\neg x\in N\left(s\setminus \left\{x\right\}\right)\right\}$$