Metamath Proof Explorer

Theorem mremre

Description: The Moore collections of subsets of a space, viewed as a kind of subset of the power set, form a Moore collection in their own right on the power set. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mremre ⊢ X ∈ V → Moore ⁡ X ∈ Moore ⁡ 𝒫 X

Proof

Step Hyp Ref Expression
1 mresspw ⊢ a ∈ Moore ⁡ X → a ⊆ 𝒫 X
2 velpw ⊢ a ∈ 𝒫 𝒫 X ↔ a ⊆ 𝒫 X
3 1 2 sylibr ⊢ a ∈ Moore ⁡ X → a ∈ 𝒫 𝒫 X
4 3 ssriv ⊢ Moore ⁡ X ⊆ 𝒫 𝒫 X
5 4 a1i ⊢ X ∈ V → Moore ⁡ X ⊆ 𝒫 𝒫 X
6 ssidd ⊢ X ∈ V → 𝒫 X ⊆ 𝒫 X
7 pwidg ⊢ X ∈ V → X ∈ 𝒫 X
8 intssuni2 ⊢ a ⊆ 𝒫 X ∧ a ≠ ∅ → ⋂ a ⊆ ⋃ 𝒫 X
9 8 3adant1 ⊢ X ∈ V ∧ a ⊆ 𝒫 X ∧ a ≠ ∅ → ⋂ a ⊆ ⋃ 𝒫 X
10 unipw ⊢ ⋃ 𝒫 X = X
11 9 10 sseqtrdi ⊢ X ∈ V ∧ a ⊆ 𝒫 X ∧ a ≠ ∅ → ⋂ a ⊆ X
12 elpw2g ⊢ X ∈ V → ⋂ a ∈ 𝒫 X ↔ ⋂ a ⊆ X
13 12 3ad2ant1 ⊢ X ∈ V ∧ a ⊆ 𝒫 X ∧ a ≠ ∅ → ⋂ a ∈ 𝒫 X ↔ ⋂ a ⊆ X
14 11 13 mpbird ⊢ X ∈ V ∧ a ⊆ 𝒫 X ∧ a ≠ ∅ → ⋂ a ∈ 𝒫 X
15 6 7 14 ismred ⊢ X ∈ V → 𝒫 X ∈ Moore ⁡ X
16 n0 ⊢ a ≠ ∅ ↔ ∃ b b ∈ a
17 intss1 ⊢ b ∈ a → ⋂ a ⊆ b
18 17 adantl ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ b ∈ a → ⋂ a ⊆ b
19 simpr ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X → a ⊆ Moore ⁡ X
20 19 sselda ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ b ∈ a → b ∈ Moore ⁡ X
21 mresspw ⊢ b ∈ Moore ⁡ X → b ⊆ 𝒫 X
22 20 21 syl ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ b ∈ a → b ⊆ 𝒫 X
23 18 22 sstrd ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ b ∈ a → ⋂ a ⊆ 𝒫 X
24 23 ex ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X → b ∈ a → ⋂ a ⊆ 𝒫 X
25 24 exlimdv ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X → ∃ b b ∈ a → ⋂ a ⊆ 𝒫 X
26 16 25 biimtrid ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X → a ≠ ∅ → ⋂ a ⊆ 𝒫 X
27 26 3impia ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ → ⋂ a ⊆ 𝒫 X
28 simp2 ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ → a ⊆ Moore ⁡ X
29 28 sselda ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ∈ a → b ∈ Moore ⁡ X
30 mre1cl ⊢ b ∈ Moore ⁡ X → X ∈ b
31 29 30 syl ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ∈ a → X ∈ b
32 31 ralrimiva ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ → ∀ b ∈ a X ∈ b
33 elintg ⊢ X ∈ V → X ∈ ⋂ a ↔ ∀ b ∈ a X ∈ b
34 33 3ad2ant1 ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ → X ∈ ⋂ a ↔ ∀ b ∈ a X ∈ b
35 32 34 mpbird ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ → X ∈ ⋂ a
36 simp12 ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ → a ⊆ Moore ⁡ X
37 36 sselda ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ ∧ c ∈ a → c ∈ Moore ⁡ X
38 simpl2 ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ ∧ c ∈ a → b ⊆ ⋂ a
39 intss1 ⊢ c ∈ a → ⋂ a ⊆ c
40 39 adantl ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ ∧ c ∈ a → ⋂ a ⊆ c
41 38 40 sstrd ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ ∧ c ∈ a → b ⊆ c
42 simpl3 ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ ∧ c ∈ a → b ≠ ∅
43 mreintcl ⊢ c ∈ Moore ⁡ X ∧ b ⊆ c ∧ b ≠ ∅ → ⋂ b ∈ c
44 37 41 42 43 syl3anc ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ ∧ c ∈ a → ⋂ b ∈ c
45 44 ralrimiva ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ → ∀ c ∈ a ⋂ b ∈ c
46 intex ⊢ b ≠ ∅ ↔ ⋂ b ∈ V
47 elintg ⊢ ⋂ b ∈ V → ⋂ b ∈ ⋂ a ↔ ∀ c ∈ a ⋂ b ∈ c
48 46 47 sylbi ⊢ b ≠ ∅ → ⋂ b ∈ ⋂ a ↔ ∀ c ∈ a ⋂ b ∈ c
49 48 3ad2ant3 ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ → ⋂ b ∈ ⋂ a ↔ ∀ c ∈ a ⋂ b ∈ c
50 45 49 mpbird ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ ∧ b ⊆ ⋂ a ∧ b ≠ ∅ → ⋂ b ∈ ⋂ a
51 27 35 50 ismred ⊢ X ∈ V ∧ a ⊆ Moore ⁡ X ∧ a ≠ ∅ → ⋂ a ∈ Moore ⁡ X
52 5 15 51 ismred ⊢ X ∈ V → Moore ⁡ X ∈ Moore ⁡ 𝒫 X