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 ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) )