Theorem bj-ismooredr2

Description: Sufficient condition to be a Moore collection (variant of bj-ismooredr singling out the empty intersection). Note that there is no sethood hypothesis on A : it is a consequence of the first hypothesis. (Contributed by BJ, 9-Dec-2021)

	Ref	Expression
Hypotheses	bj-ismooredr2.1	⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝐴 )
	bj-ismooredr2.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝐴 )
Assertion	bj-ismooredr2	⊢ ( 𝜑 → 𝐴 ∈ Moore )

Proof

Step	Hyp	Ref	Expression
1		bj-ismooredr2.1	⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝐴 )
2		bj-ismooredr2.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) ) → ∩ 𝑥 ∈ 𝐴 )
3	2	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐴 )
4		intssuni2	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ⊆ ∪ 𝐴 )
5		dfss	⊢ ( ∩ 𝑥 ⊆ ∪ 𝐴 ↔ ∩ 𝑥 = ( ∩ 𝑥 ∩ ∪ 𝐴 ) )
6		incom	⊢ ( ∩ 𝑥 ∩ ∪ 𝐴 ) = ( ∪ 𝐴 ∩ ∩ 𝑥 )
7	6	eqeq2i	⊢ ( ∩ 𝑥 = ( ∩ 𝑥 ∩ ∪ 𝐴 ) ↔ ∩ 𝑥 = ( ∪ 𝐴 ∩ ∩ 𝑥 ) )
8		eleq1	⊢ ( ∩ 𝑥 = ( ∪ 𝐴 ∩ ∩ 𝑥 ) → ( ∩ 𝑥 ∈ 𝐴 ↔ ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
9	7 8	sylbi	⊢ ( ∩ 𝑥 = ( ∩ 𝑥 ∩ ∪ 𝐴 ) → ( ∩ 𝑥 ∈ 𝐴 ↔ ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
10	9	biimpd	⊢ ( ∩ 𝑥 = ( ∩ 𝑥 ∩ ∪ 𝐴 ) → ( ∩ 𝑥 ∈ 𝐴 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
11	5 10	sylbi	⊢ ( ∩ 𝑥 ⊆ ∪ 𝐴 → ( ∩ 𝑥 ∈ 𝐴 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
12	4 11	syl	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ( ∩ 𝑥 ∈ 𝐴 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
13	12	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ( ∩ 𝑥 ∈ 𝐴 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
14	3 13	mpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑥 ≠ ∅ ) → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 )
15	14	ex	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 ≠ ∅ → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
16		nne	⊢ ( ¬ 𝑥 ≠ ∅ ↔ 𝑥 = ∅ )
17		rint0	⊢ ( 𝑥 = ∅ → ( ∪ 𝐴 ∩ ∩ 𝑥 ) = ∪ 𝐴 )
18		eleq1a	⊢ ( ∪ 𝐴 ∈ 𝐴 → ( ( ∪ 𝐴 ∩ ∩ 𝑥 ) = ∪ 𝐴 → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
19	1 17 18	syl2im	⊢ ( 𝜑 → ( 𝑥 = ∅ → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
20	16 19	biimtrid	⊢ ( 𝜑 → ( ¬ 𝑥 ≠ ∅ → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ¬ 𝑥 ≠ ∅ → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 ) )
22	15 21	pm2.61d	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → ( ∪ 𝐴 ∩ ∩ 𝑥 ) ∈ 𝐴 )
23	22	bj-ismooredr	⊢ ( 𝜑 → 𝐴 ∈ Moore )