Metamath Proof Explorer

Theorem mrcidb

Description: A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypothesis mrcfval.f ⊢ F = mrCls ⁡ C
Assertion mrcidb ⊢ C ∈ Moore ⁡ X → U ∈ C ↔ F ⁡ U = U

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢ F = mrCls ⁡ C
2 1 mrcid ⊢ C ∈ Moore ⁡ X ∧ U ∈ C → F ⁡ U = U
3 simpr ⊢ C ∈ Moore ⁡ X ∧ F ⁡ U = U → F ⁡ U = U
4 1 mrcssv ⊢ C ∈ Moore ⁡ X → F ⁡ U ⊆ X
5 4 adantr ⊢ C ∈ Moore ⁡ X ∧ F ⁡ U = U → F ⁡ U ⊆ X
6 3 5 eqsstrrd ⊢ C ∈ Moore ⁡ X ∧ F ⁡ U = U → U ⊆ X
7 1 mrccl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X → F ⁡ U ∈ C
8 6 7 syldan ⊢ C ∈ Moore ⁡ X ∧ F ⁡ U = U → F ⁡ U ∈ C
9 3 8 eqeltrrd ⊢ C ∈ Moore ⁡ X ∧ F ⁡ U = U → U ∈ C
10 2 9 impbida ⊢ C ∈ Moore ⁡ X → U ∈ C ↔ F ⁡ U = U