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 ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝑈 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑈 ) ⊆ 𝑈 ) )