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 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C → C ∩ 𝒫 A ∈ Moore ⁡ A

Proof

Step Hyp Ref Expression
1 inss2 ⊢ C ∩ 𝒫 A ⊆ 𝒫 A
2 1 a1i ⊢ C ∈ Moore ⁡ X ∧ A ∈ C → C ∩ 𝒫 A ⊆ 𝒫 A
3 simpr ⊢ C ∈ Moore ⁡ X ∧ A ∈ C → A ∈ C
4 pwidg ⊢ A ∈ C → A ∈ 𝒫 A
5 4 adantl ⊢ C ∈ Moore ⁡ X ∧ A ∈ C → A ∈ 𝒫 A
6 3 5 elind ⊢ C ∈ Moore ⁡ X ∧ A ∈ C → A ∈ C ∩ 𝒫 A
7 simp1l ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → C ∈ Moore ⁡ X
8 inss1 ⊢ C ∩ 𝒫 A ⊆ C
9 sstr ⊢ x ⊆ C ∩ 𝒫 A ∧ C ∩ 𝒫 A ⊆ C → x ⊆ C
10 8 9 mpan2 ⊢ x ⊆ C ∩ 𝒫 A → x ⊆ C
11 10 3ad2ant2 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → x ⊆ C
12 simp3 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → x ≠ ∅
13 mreintcl ⊢ C ∈ Moore ⁡ X ∧ x ⊆ C ∧ x ≠ ∅ → ⋂ x ∈ C
14 7 11 12 13 syl3anc ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → ⋂ x ∈ C
15 sstr ⊢ x ⊆ C ∩ 𝒫 A ∧ C ∩ 𝒫 A ⊆ 𝒫 A → x ⊆ 𝒫 A
16 1 15 mpan2 ⊢ x ⊆ C ∩ 𝒫 A → x ⊆ 𝒫 A
17 16 3ad2ant2 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → x ⊆ 𝒫 A
18 intssuni2 ⊢ x ⊆ 𝒫 A ∧ x ≠ ∅ → ⋂ x ⊆ ⋃ 𝒫 A
19 17 12 18 syl2anc ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → ⋂ x ⊆ ⋃ 𝒫 A
20 unipw ⊢ ⋃ 𝒫 A = A
21 19 20 sseqtrdi ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → ⋂ x ⊆ A
22 elpw2g ⊢ A ∈ C → ⋂ x ∈ 𝒫 A ↔ ⋂ x ⊆ A
23 22 adantl ⊢ C ∈ Moore ⁡ X ∧ A ∈ C → ⋂ x ∈ 𝒫 A ↔ ⋂ x ⊆ A
24 23 3ad2ant1 ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → ⋂ x ∈ 𝒫 A ↔ ⋂ x ⊆ A
25 21 24 mpbird ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → ⋂ x ∈ 𝒫 A
26 14 25 elind ⊢ C ∈ Moore ⁡ X ∧ A ∈ C ∧ x ⊆ C ∩ 𝒫 A ∧ x ≠ ∅ → ⋂ x ∈ C ∩ 𝒫 A
27 2 6 26 ismred ⊢ C ∈ Moore ⁡ X ∧ A ∈ C → C ∩ 𝒫 A ∈ Moore ⁡ A