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 ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion mrcidb2 ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝑈 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑈 ) ⊆ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 mrcfval.f ⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2 1 mrcidb ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) )
3 2 adantr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝑈 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) )
4 eqss ⊢ ( ( 𝐹 ‘ 𝑈 ) = 𝑈 ↔ ( ( 𝐹 ‘ 𝑈 ) ⊆ 𝑈 ∧ 𝑈 ⊆ ( 𝐹 ‘ 𝑈 ) ) )
5 1 mrcssid ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ⊆ ( 𝐹 ‘ 𝑈 ) )
6 5 biantrud ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( ( 𝐹 ‘ 𝑈 ) ⊆ 𝑈 ↔ ( ( 𝐹 ‘ 𝑈 ) ⊆ 𝑈 ∧ 𝑈 ⊆ ( 𝐹 ‘ 𝑈 ) ) ) )
7 4 6 bitr4id ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( ( 𝐹 ‘ 𝑈 ) = 𝑈 ↔ ( 𝐹 ‘ 𝑈 ) ⊆ 𝑈 ) )
8 3 7 bitrd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝑈 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑈 ) ⊆ 𝑈 ) )