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 -> A = B )
	disjord.2	|- ( ( ph /\ x e. A /\ x e. B ) -> a = b )
Assertion	disjord	|- ( ph -> Disj_ a e. V A )

Proof

Step	Hyp	Ref	Expression
1		disjord.1	|- ( a = b -> A = B )
2		disjord.2	|- ( ( ph /\ x e. A /\ x e. B ) -> a = b )
3		orc	|- ( a = b -> ( a = b \/ ( A i^i B ) = (/) ) )
4	3	a1d	|- ( a = b -> ( ph -> ( a = b \/ ( A i^i B ) = (/) ) ) )
5	2	3expia	|- ( ( ph /\ x e. A ) -> ( x e. B -> a = b ) )
6	5	con3d	|- ( ( ph /\ x e. A ) -> ( -. a = b -> -. x e. B ) )
7	6	impancom	|- ( ( ph /\ -. a = b ) -> ( x e. A -> -. x e. B ) )
8	7	ralrimiv	|- ( ( ph /\ -. a = b ) -> A. x e. A -. x e. B )
9		disj	|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )
10	8 9	sylibr	|- ( ( ph /\ -. a = b ) -> ( A i^i B ) = (/) )
11	10	olcd	|- ( ( ph /\ -. a = b ) -> ( a = b \/ ( A i^i B ) = (/) ) )
12	11	expcom	|- ( -. a = b -> ( ph -> ( a = b \/ ( A i^i B ) = (/) ) ) )
13	4 12	pm2.61i	|- ( ph -> ( a = b \/ ( A i^i B ) = (/) ) )
14	13	adantr	|- ( ( ph /\ ( a e. V /\ b e. V ) ) -> ( a = b \/ ( A i^i B ) = (/) ) )
15	14	ralrimivva	|- ( ph -> A. a e. V A. b e. V ( a = b \/ ( A i^i B ) = (/) ) )
16	1	disjor	|- ( Disj_ a e. V A <-> A. a e. V A. b e. V ( a = b \/ ( A i^i B ) = (/) ) )
17	15 16	sylibr	|- ( ph -> Disj_ a e. V A )