Theorem bj-ismoored

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

	Ref	Expression
Hypotheses	bj-ismoored.1	⊢ ( 𝜑 → 𝐴 ∈ Moore )
	bj-ismoored.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	bj-ismoored	⊢ ( 𝜑 → ( ∪ 𝐴 ∩ ∩ 𝐵 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bj-ismoored.1	⊢ ( 𝜑 → 𝐴 ∈ Moore )
2		bj-ismoored.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3		inteq	⊢ ( 𝑥 = 𝐵 → ∩ 𝑥 = ∩ 𝐵 )
4	3	ineq2d	⊢ ( 𝑥 = 𝐵 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) = ( ∪ 𝐴 ∩ ∩ 𝐵 ) )
5	4	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ↔ ( ∪ 𝐴 ∩ ∩ 𝐵 ) ∈ 𝐴 ) )
6		bj-ismoore	⊢ ( 𝐴 ∈ Moore ↔ ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 )
7	1 6	sylib	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝒫 𝐴 ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 )
8	1 2	sselpwd	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐴 )
9	5 7 8	rspcdva	⊢ ( 𝜑 → ( ∪ 𝐴 ∩ ∩ 𝐵 ) ∈ 𝐴 )