Theorem mreincl

Description: Two closed sets have a closed intersection. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Assertion	mreincl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		intprg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
2	1	3adant1	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
3		simp1	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
4		prssi	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → { 𝐴 , 𝐵 } ⊆ 𝐶 )
5	4	3adant1	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → { 𝐴 , 𝐵 } ⊆ 𝐶 )
6		prnzg	⊢ ( 𝐴 ∈ 𝐶 → { 𝐴 , 𝐵 } ≠ ∅ )
7	6	3ad2ant2	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → { 𝐴 , 𝐵 } ≠ ∅ )
8		mreintcl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ { 𝐴 , 𝐵 } ⊆ 𝐶 ∧ { 𝐴 , 𝐵 } ≠ ∅ ) → ∩ { 𝐴 , 𝐵 } ∈ 𝐶 )
9	3 5 7 8	syl3anc	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ∩ { 𝐴 , 𝐵 } ∈ 𝐶 )
10	2 9	eqeltrrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 )