This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitr4di ⊢ ( 𝑋 ∈ V → ( ( 𝐶 ∈ 𝒫 𝒫 𝑋 ∧ ( 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) ) )
29 14 22 28 3bitrd ⊢ ( 𝑋 ∈ V → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) ) )
30 1 3 29 pm5.21nii ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) )