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 ‘ 𝐴 ) )