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	$$⊢\phi \to \bigcup A\in A$$
	bj-ismooredr2.2	$$⊢\left(\phi \wedge \left(x\subseteq A\wedge x\ne \varnothing \right)\right)\to \bigcap x\in A$$
Assertion	bj-ismooredr2	$$⊢\phi \to A\in \underset{\_}{\mathrm{Moore}}$$

Proof

Step	Hyp	Ref	Expression
1		bj-ismooredr2.1	$$⊢\phi \to \bigcup A\in A$$
2		bj-ismooredr2.2	$$⊢\left(\phi \wedge \left(x\subseteq A\wedge x\ne \varnothing \right)\right)\to \bigcap x\in A$$
3	2	anassrs	$$⊢\left(\left(\phi \wedge x\subseteq A\right)\wedge x\ne \varnothing \right)\to \bigcap x\in A$$
4		intssuni2	$$⊢\left(x\subseteq A\wedge x\ne \varnothing \right)\to \bigcap x\subseteq \bigcup A$$
5		dfss	$$⊢\bigcap x\subseteq \bigcup A\leftrightarrow \bigcap x=\bigcap x\cap \bigcup A$$
6		incom	$$⊢\bigcap x\cap \bigcup A=\bigcup A\cap \bigcap x$$
7	6	eqeq2i	$$⊢\bigcap x=\bigcap x\cap \bigcup A\leftrightarrow \bigcap x=\bigcup A\cap \bigcap x$$
8		eleq1	$$⊢\bigcap x=\bigcup A\cap \bigcap x\to \left(\bigcap x\in A\leftrightarrow \bigcup A\cap \bigcap x\in A\right)$$
9	7 8	sylbi	$$⊢\bigcap x=\bigcap x\cap \bigcup A\to \left(\bigcap x\in A\leftrightarrow \bigcup A\cap \bigcap x\in A\right)$$
10	9	biimpd	$$⊢\bigcap x=\bigcap x\cap \bigcup A\to \left(\bigcap x\in A\to \bigcup A\cap \bigcap x\in A\right)$$
11	5 10	sylbi	$$⊢\bigcap x\subseteq \bigcup A\to \left(\bigcap x\in A\to \bigcup A\cap \bigcap x\in A\right)$$
12	4 11	syl	$$⊢\left(x\subseteq A\wedge x\ne \varnothing \right)\to \left(\bigcap x\in A\to \bigcup A\cap \bigcap x\in A\right)$$
13	12	adantll	$$⊢\left(\left(\phi \wedge x\subseteq A\right)\wedge x\ne \varnothing \right)\to \left(\bigcap x\in A\to \bigcup A\cap \bigcap x\in A\right)$$
14	3 13	mpd	$$⊢\left(\left(\phi \wedge x\subseteq A\right)\wedge x\ne \varnothing \right)\to \bigcup A\cap \bigcap x\in A$$
15	14	ex	$$⊢\left(\phi \wedge x\subseteq A\right)\to \left(x\ne \varnothing \to \bigcup A\cap \bigcap x\in A\right)$$
16		nne	$$⊢\neg x\ne \varnothing \leftrightarrow x=\varnothing$$
17		rint0	$$⊢x=\varnothing \to \bigcup A\cap \bigcap x=\bigcup A$$
18		eleq1a	$$⊢\bigcup A\in A\to \left(\bigcup A\cap \bigcap x=\bigcup A\to \bigcup A\cap \bigcap x\in A\right)$$
19	1 17 18	syl2im	$$⊢\phi \to \left(x=\varnothing \to \bigcup A\cap \bigcap x\in A\right)$$
20	16 19	biimtrid	$$⊢\phi \to \left(\neg x\ne \varnothing \to \bigcup A\cap \bigcap x\in A\right)$$
21	20	adantr	$$⊢\left(\phi \wedge x\subseteq A\right)\to \left(\neg x\ne \varnothing \to \bigcup A\cap \bigcap x\in A\right)$$
22	15 21	pm2.61d	$$⊢\left(\phi \wedge x\subseteq A\right)\to \bigcup A\cap \bigcap x\in A$$
23	22	bj-ismooredr	$$⊢\phi \to A\in \underset{\_}{\mathrm{Moore}}$$