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=bA=B
disjord.2 φxAxBa=b
Assertion disjord φDisjaVA

Proof

Step Hyp Ref Expression
1 disjord.1 a=bA=B
2 disjord.2 φxAxBa=b
3 orc a=ba=bAB=
4 3 a1d a=bφa=bAB=
5 2 3expia φxAxBa=b
6 5 con3d φxA¬a=b¬xB
7 6 impancom φ¬a=bxA¬xB
8 7 ralrimiv φ¬a=bxA¬xB
9 disj AB=xA¬xB
10 8 9 sylibr φ¬a=bAB=
11 10 olcd φ¬a=ba=bAB=
12 11 expcom ¬a=bφa=bAB=
13 4 12 pm2.61i φa=bAB=
14 13 adantr φaVbVa=bAB=
15 14 ralrimivva φaVbVa=bAB=
16 1 disjor DisjaVAaVbVa=bAB=
17 15 16 sylibr φDisjaVA