Metamath Proof Explorer


Theorem mrcidm

Description: The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypothesis mrcfval.f F = mrCls C
Assertion mrcidm C Moore X U X F F U = F U

Proof

Step Hyp Ref Expression
1 mrcfval.f F = mrCls C
2 1 mrccl C Moore X U X F U C
3 1 mrcid C Moore X F U C F F U = F U
4 2 3 syldan C Moore X U X F F U = F U