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 1 mrcssid ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X → U ⊆ F ⁡ U
5 4 biantrud ⊢ C ∈ Moore ⁡ X ∧ U ⊆ X → F ⁡ U ⊆ U ↔ F ⁡ U ⊆ U ∧ U ⊆ F ⁡ U
6 eqss ⊢ F ⁡ U = U ↔ F ⁡ U ⊆ U ∧ U ⊆ F ⁡ U
7 5 6 syl6rbbr ⊢ 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