Theorem ismred

Description: Properties that determine a Moore collection. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	ismred.ss	⊢ ( 𝜑 → 𝐶 ⊆ 𝒫 𝑋 )
	ismred.ba	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
	ismred.in	⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅ ) → ∩ 𝑠 ∈ 𝐶 )
Assertion	ismred	⊢ ( 𝜑 → 𝐶 ∈ ( Moore ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ismred.ss	⊢ ( 𝜑 → 𝐶 ⊆ 𝒫 𝑋 )
2		ismred.ba	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
3		ismred.in	⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐶 ∧ 𝑠 ≠ ∅ ) → ∩ 𝑠 ∈ 𝐶 )
4		velpw	⊢ ( 𝑠 ∈ 𝒫 𝐶 ↔ 𝑠 ⊆ 𝐶 )
5	3	3expia	⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐶 ) → ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) )
6	4 5	sylan2b	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐶 ) → ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) )
8		ismre	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ↔ ( 𝐶 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( 𝑠 ≠ ∅ → ∩ 𝑠 ∈ 𝐶 ) ) )
9	1 2 7 8	syl3anbrc	⊢ ( 𝜑 → 𝐶 ∈ ( Moore ‘ 𝑋 ) )