# Metamath Proof Explorer

## Theorem submre

Description: The subcollection of a closed set system below a given closed set is itself a closed set system. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Assertion submre ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) → ( 𝐶 ∩ 𝒫 𝐴 ) ∈ ( Moore ‘ 𝐴 ) )

### Proof

Step Hyp Ref Expression
1 inss2 ( 𝐶 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴
2 1 a1i ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) → ( 𝐶 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 )
3 simpr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) → 𝐴𝐶 )
4 pwidg ( 𝐴𝐶𝐴 ∈ 𝒫 𝐴 )
5 4 adantl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) → 𝐴 ∈ 𝒫 𝐴 )
6 3 5 elind ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) → 𝐴 ∈ ( 𝐶 ∩ 𝒫 𝐴 ) )
7 simp1l ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
8 inss1 ( 𝐶 ∩ 𝒫 𝐴 ) ⊆ 𝐶
9 sstr ( ( 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ ( 𝐶 ∩ 𝒫 𝐴 ) ⊆ 𝐶 ) → 𝑥𝐶 )
10 8 9 mpan2 ( 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) → 𝑥𝐶 )
11 10 3ad2ant2 ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥𝐶 )
12 simp3 ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ≠ ∅ )
13 mreintcl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥𝐶𝑥 ≠ ∅ ) → 𝑥𝐶 )
14 7 11 12 13 syl3anc ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥𝐶 )
15 sstr ( ( 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ ( 𝐶 ∩ 𝒫 𝐴 ) ⊆ 𝒫 𝐴 ) → 𝑥 ⊆ 𝒫 𝐴 )
16 1 15 mpan2 ( 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) → 𝑥 ⊆ 𝒫 𝐴 )
17 16 3ad2ant2 ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ⊆ 𝒫 𝐴 )
18 intssuni2 ( ( 𝑥 ⊆ 𝒫 𝐴𝑥 ≠ ∅ ) → 𝑥 𝒫 𝐴 )
19 17 12 18 syl2anc ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥 𝒫 𝐴 )
20 unipw 𝒫 𝐴 = 𝐴
21 19 20 sseqtrdi ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥𝐴 )
22 elpw2g ( 𝐴𝐶 → ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴 ) )
23 22 adantl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) → ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴 ) )
24 23 3ad2ant1 ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴 ) )
25 21 24 mpbird ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ 𝒫 𝐴 )
26 14 25 elind ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝒫 𝐴 ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ( 𝐶 ∩ 𝒫 𝐴 ) )
27 2 6 26 ismred ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝐴𝐶 ) → ( 𝐶 ∩ 𝒫 𝐴 ) ∈ ( Moore ‘ 𝐴 ) )