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

Metamath Proof Explorer

Theorem mrcflem

Description: The domain and codomain of the function expression for Moore closures. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Assertion mrcflem ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 𝑋 ⟶ 𝐶 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
2 ssrab2 ⊢ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ⊆ 𝐶
3 2 a1i ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ⊆ 𝐶 )
4 sseq2 ⊢ ( 𝑠 = 𝑋 → ( 𝑥 ⊆ 𝑠 ↔ 𝑥 ⊆ 𝑋 ) )
5 mre1cl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
6 5 adantr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑋 ∈ 𝐶 )
7 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
8 7 adantl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑥 ⊆ 𝑋 )
9 4 6 8 elrabd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑋 ∈ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } )
10 9 ne0d ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ≠ ∅ )
11 mreintcl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ⊆ 𝐶 ∧ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ≠ ∅ ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ∈ 𝐶 )
12 1 3 10 11 syl3anc ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ∈ 𝐶 )
13 12 fmpttd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 𝑋 ⟶ 𝐶 )