Metamath Proof Explorer


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 = mrCls C
Assertion mrcidb2 C Moore X U X U C F U U

Proof

Step Hyp Ref Expression
1 mrcfval.f F = mrCls C
2 1 mrcidb C Moore X U C F U = U
3 2 adantr C Moore X U X U C F U = U
4 eqss F U = U F U U U F U
5 1 mrcssid C Moore X U X U F U
6 5 biantrud C Moore X U X F U U F U U U F U
7 4 6 bitr4id C Moore X U X F U = U F U U
8 3 7 bitrd C Moore X U X U C F U U