This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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