Theorem bj-ismoored0

Description: Necessary condition to be a Moore collection. (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Assertion	bj-ismoored0	⊢ ( 𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bj-ismoore	⊢ ( 𝐴 ∈ Moore ↔ ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 )
2		0elpw	⊢ ∅ ∈ 𝒫 𝐴
3		rint0	⊢ ( 𝑥 = ∅ → ( ∪ 𝐴 ∩ ∩ 𝑥 ) = ∪ 𝐴 )
4	3	eleq1d	⊢ ( 𝑥 = ∅ → ( ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ↔ ∪ 𝐴 ∈ 𝐴 ) )
5	4	rspcv	⊢ ( ∅ ∈ 𝒫 𝐴 → ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 → ∪ 𝐴 ∈ 𝐴 ) )
6	2 5	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 → ∪ 𝐴 ∈ 𝐴 )
7	1 6	sylbi	⊢ ( 𝐴 ∈ Moore → ∪ 𝐴 ∈ 𝐴 )