Metamath Proof Explorer


Theorem disjecxrn

Description: Two ways of saying that ( R |X. S ) -cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020) (Revised by Peter Mazsa, 21-Aug-2023)

Ref Expression
Assertion disjecxrn A V B W A R S B R S = A R B R = A S B S =

Proof

Step Hyp Ref Expression
1 ecxrn A V A R S = y z | A R y A S z
2 ecxrn B W B R S = y z | B R y B S z
3 1 2 ineqan12d A V B W A R S B R S = y z | A R y A S z y z | B R y B S z
4 inopab y z | A R y A S z y z | B R y B S z = y z | A R y A S z B R y B S z
5 3 4 eqtrdi A V B W A R S B R S = y z | A R y A S z B R y B S z
6 an4 A R y A S z B R y B S z A R y B R y A S z B S z
7 6 opabbii y z | A R y A S z B R y B S z = y z | A R y B R y A S z B S z
8 5 7 eqtrdi A V B W A R S B R S = y z | A R y B R y A S z B S z
9 8 neeq1d A V B W A R S B R S y z | A R y B R y A S z B S z
10 opabn0 y z | A R y B R y A S z B S z y z A R y B R y A S z B S z
11 9 10 bitrdi A V B W A R S B R S y z A R y B R y A S z B S z
12 exdistrv y z A R y B R y A S z B S z y A R y B R y z A S z B S z
13 11 12 bitrdi A V B W A R S B R S y A R y B R y z A S z B S z
14 ecinn0 A V B W A R B R y A R y B R y
15 ecinn0 A V B W A S B S z A S z B S z
16 14 15 anbi12d A V B W A R B R A S B S y A R y B R y z A S z B S z
17 13 16 bitr4d A V B W A R S B R S A R B R A S B S
18 neanior A R B R A S B S ¬ A R B R = A S B S =
19 17 18 bitrdi A V B W A R S B R S ¬ A R B R = A S B S =
20 19 necon4abid A V B W A R S B R S = A R B R = A S B S =