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 ‘ 𝑋 ) → ( 𝑥 ∈ 𝒫 𝑋 ↦ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑥 ⊆ 𝑠 } ) : 𝒫 𝑋 ⟶ 𝐶 )