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

Metamath Proof Explorer

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 ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 )