# Metamath Proof Explorer

## Theorem ismre

Description: Property of being a Moore collection on some base set. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion ismre ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) )

### Proof

Step Hyp Ref Expression
1 elfvex ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ V )
2 elex ( 𝑋𝐶𝑋 ∈ V )
3 2 3ad2ant2 ( ( 𝐶 ⊆ 𝒫 𝑋𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) → 𝑋 ∈ V )
4 pweq ( 𝑥 = 𝑋 → 𝒫 𝑥 = 𝒫 𝑋 )
5 4 pweqd ( 𝑥 = 𝑋 → 𝒫 𝒫 𝑥 = 𝒫 𝒫 𝑋 )
6 eleq1 ( 𝑥 = 𝑋 → ( 𝑥𝑐𝑋𝑐 ) )
7 6 anbi1d ( 𝑥 = 𝑋 → ( ( 𝑥𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) ↔ ( 𝑋𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) ) )
8 5 7 rabeqbidv ( 𝑥 = 𝑋 → { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } = { 𝑐 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝑋𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } )
9 df-mre Moore = ( 𝑥 ∈ V ↦ { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } )
10 vpwex 𝒫 𝑥 ∈ V
11 10 pwex 𝒫 𝒫 𝑥 ∈ V
12 11 rabex { 𝑐 ∈ 𝒫 𝒫 𝑥 ∣ ( 𝑥𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } ∈ V
13 8 9 12 fvmpt3i ( 𝑋 ∈ V → ( Moore ‘ 𝑋 ) = { 𝑐 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝑋𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } )
14 13 eleq2d ( 𝑋 ∈ V → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ 𝐶 ∈ { 𝑐 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝑋𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } ) )
15 eleq2 ( 𝑐 = 𝐶 → ( 𝑋𝑐𝑋𝐶 ) )
16 pweq ( 𝑐 = 𝐶 → 𝒫 𝑐 = 𝒫 𝐶 )
17 eleq2 ( 𝑐 = 𝐶 → ( 𝑠𝑐 𝑠𝐶 ) )
18 17 imbi2d ( 𝑐 = 𝐶 → ( ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ↔ ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) )
19 16 18 raleqbidv ( 𝑐 = 𝐶 → ( ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ↔ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) )
20 15 19 anbi12d ( 𝑐 = 𝐶 → ( ( 𝑋𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) ↔ ( 𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) )
21 20 elrab ( 𝐶 ∈ { 𝑐 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝑋𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } ↔ ( 𝐶 ∈ 𝒫 𝒫 𝑋 ∧ ( 𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) )
22 21 a1i ( 𝑋 ∈ V → ( 𝐶 ∈ { 𝑐 ∈ 𝒫 𝒫 𝑋 ∣ ( 𝑋𝑐 ∧ ∀ 𝑠 ∈ 𝒫 𝑐 ( 𝑠 ≠ ∅ → 𝑠𝑐 ) ) } ↔ ( 𝐶 ∈ 𝒫 𝒫 𝑋 ∧ ( 𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) ) )
23 pwexg ( 𝑋 ∈ V → 𝒫 𝑋 ∈ V )
24 elpw2g ( 𝒫 𝑋 ∈ V → ( 𝐶 ∈ 𝒫 𝒫 𝑋𝐶 ⊆ 𝒫 𝑋 ) )
25 23 24 syl ( 𝑋 ∈ V → ( 𝐶 ∈ 𝒫 𝒫 𝑋𝐶 ⊆ 𝒫 𝑋 ) )
26 25 anbi1d ( 𝑋 ∈ V → ( ( 𝐶 ∈ 𝒫 𝒫 𝑋 ∧ ( 𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ ( 𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) ) )
27 3anass ( ( 𝐶 ⊆ 𝒫 𝑋𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ ( 𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) )
28 26 27 syl6bbr ( 𝑋 ∈ V → ( ( 𝐶 ∈ 𝒫 𝒫 𝑋 ∧ ( 𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) ↔ ( 𝐶 ⊆ 𝒫 𝑋𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) )
29 14 22 28 3bitrd ( 𝑋 ∈ V → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) ) )
30 1 3 29 pm5.21nii ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋𝑋𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → 𝑠𝐶 ) ) )