Theorem disjord

Description: Conditions for a collection of sets A ( a ) for a e. V to be disjoint. (Contributed by AV, 9-Jan-2022)

	Ref	Expression
Hypotheses	disjord.1	$$⊢a=b\to A=B$$
	disjord.2	$$⊢\left(\phi \wedge x\in A\wedge x\in B\right)\to a=b$$
Assertion	disjord	$$⊢\phi \to \underset{a\in V}{Disj}A$$

Proof

Step	Hyp	Ref	Expression
1		disjord.1	$$⊢a=b\to A=B$$
2		disjord.2	$$⊢\left(\phi \wedge x\in A\wedge x\in B\right)\to a=b$$
3		orc	$$⊢a=b\to \left(a=b\vee A\cap B=\varnothing \right)$$
4	3	a1d	$$⊢a=b\to \left(\phi \to \left(a=b\vee A\cap B=\varnothing \right)\right)$$
5	2	3expia	$$⊢\left(\phi \wedge x\in A\right)\to \left(x\in B\to a=b\right)$$
6	5	con3d	$$⊢\left(\phi \wedge x\in A\right)\to \left(\neg a=b\to \neg x\in B\right)$$
7	6	impancom	$$⊢\left(\phi \wedge \neg a=b\right)\to \left(x\in A\to \neg x\in B\right)$$
8	7	ralrimiv	$$⊢\left(\phi \wedge \neg a=b\right)\to \forall x\in A\neg x\in B$$
9		disj	$$⊢A\cap B=\varnothing \leftrightarrow \forall x\in A\neg x\in B$$
10	8 9	sylibr	$$⊢\left(\phi \wedge \neg a=b\right)\to A\cap B=\varnothing$$
11	10	olcd	$$⊢\left(\phi \wedge \neg a=b\right)\to \left(a=b\vee A\cap B=\varnothing \right)$$
12	11	expcom	$$⊢\neg a=b\to \left(\phi \to \left(a=b\vee A\cap B=\varnothing \right)\right)$$
13	4 12	pm2.61i	$$⊢\phi \to \left(a=b\vee A\cap B=\varnothing \right)$$
14	13	adantr	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\right)\to \left(a=b\vee A\cap B=\varnothing \right)$$
15	14	ralrimivva	$$⊢\phi \to \forall a\in V\forall b\in V\left(a=b\vee A\cap B=\varnothing \right)$$
16	1	disjor	$$⊢\underset{a\in V}{Disj}A\leftrightarrow \forall a\in V\forall b\in V\left(a=b\vee A\cap B=\varnothing \right)$$
17	15 16	sylibr	$$⊢\phi \to \underset{a\in V}{Disj}A$$