This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )