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 ( 𝑋 ∈ 𝑉 → ( Moore ‘ 𝑋 ) ∈ ( Moore ‘ 𝒫 𝑋 ) )

Proof

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