Theorem mrcidb2

Description: A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015)

	Ref	Expression
Hypothesis	mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
Assertion	mrcidb2	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to \left(U\in C\leftrightarrow F\left(U\right)\subseteq U\right)$$

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	$$⊢F=\mathrm{mrCls}\left(C\right)$$
2	1	mrcidb	$$⊢C\in \mathrm{Moore}\left(X\right)\to \left(U\in C\leftrightarrow F\left(U\right)=U\right)$$
3	2	adantr	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to \left(U\in C\leftrightarrow F\left(U\right)=U\right)$$
4		eqss	$$⊢F\left(U\right)=U\leftrightarrow \left(F\left(U\right)\subseteq U\wedge U\subseteq F\left(U\right)\right)$$
5	1	mrcssid	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to U\subseteq F\left(U\right)$$
6	5	biantrud	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to \left(F\left(U\right)\subseteq U\leftrightarrow \left(F\left(U\right)\subseteq U\wedge U\subseteq F\left(U\right)\right)\right)$$
7	4 6	bitr4id	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to \left(F\left(U\right)=U\leftrightarrow F\left(U\right)\subseteq U\right)$$
8	3 7	bitrd	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq X\right)\to \left(U\in C\leftrightarrow F\left(U\right)\subseteq U\right)$$