Metamath Proof Explorer


Theorem disjxp1

Description: The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis disjxp1.1 φ Disj x A B
Assertion disjxp1 φ Disj x A B × C

Proof

Step Hyp Ref Expression
1 disjxp1.1 φ Disj x A B
2 animorrl φ y A z A y = z y = z y / x B × C z / x B × C =
3 csbxp y / x B × C = y / x B × y / x C
4 csbxp z / x B × C = z / x B × z / x C
5 3 4 ineq12i y / x B × C z / x B × C = y / x B × y / x C z / x B × z / x C
6 simpll φ y A z A y z φ
7 simplrl φ y A z A y z y A
8 simplrr φ y A z A y z z A
9 6 7 8 jca31 φ y A z A y z φ y A z A
10 simpr φ y A z A y z y z
11 10 neneqd φ y A z A y z ¬ y = z
12 disjors Disj x A B y A z A y = z y / x B z / x B =
13 1 12 sylib φ y A z A y = z y / x B z / x B =
14 13 r19.21bi φ y A z A y = z y / x B z / x B =
15 14 r19.21bi φ y A z A y = z y / x B z / x B =
16 15 ord φ y A z A ¬ y = z y / x B z / x B =
17 9 11 16 sylc φ y A z A y z y / x B z / x B =
18 xpdisj1 y / x B z / x B = y / x B × y / x C z / x B × z / x C =
19 17 18 syl φ y A z A y z y / x B × y / x C z / x B × z / x C =
20 5 19 syl5eq φ y A z A y z y / x B × C z / x B × C =
21 20 olcd φ y A z A y z y = z y / x B × C z / x B × C =
22 2 21 pm2.61dane φ y A z A y = z y / x B × C z / x B × C =
23 22 ralrimivva φ y A z A y = z y / x B × C z / x B × C =
24 disjors Disj x A B × C y A z A y = z y / x B × C z / x B × C =
25 23 24 sylibr φ Disj x A B × C