# 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 ‘ 𝒫 𝑋 ) )