Theorem bj-ismoored2

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-ismoored.1	⊢ ( 𝜑 → 𝐴 ∈ Moore )
2		bj-ismoored.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3		bj-ismoored2.3	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
4		intssuni2	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) → ∩ 𝐵 ⊆ ∪ 𝐴 )
5	2 3 4	syl2anc	⊢ ( 𝜑 → ∩ 𝐵 ⊆ ∪ 𝐴 )
6		sseqin2	⊢ ( ∩ 𝐵 ⊆ ∪ 𝐴 ↔ ( ∪ 𝐴 ∩ ∩ 𝐵 ) = ∩ 𝐵 )
7	5 6	sylib	⊢ ( 𝜑 → ( ∪ 𝐴 ∩ ∩ 𝐵 ) = ∩ 𝐵 )
8	1 2	bj-ismoored	⊢ ( 𝜑 → ( ∪ 𝐴 ∩ ∩ 𝐵 ) ∈ 𝐴 )
9	7 8	eqeltrrd	⊢ ( 𝜑 → ∩ 𝐵 ∈ 𝐴 )