Metamath Proof Explorer
Description: If two classes are not disjoint, then the composition of their
cross-product with itself is idempotent. (Contributed by RP, 24-Dec-2019)
|
|
Ref |
Expression |
|
Hypothesis |
xpcoidgend.1 |
|
|
Assertion |
xpcoidgend |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
xpcoidgend.1 |
|
2 |
|
incom |
|
3 |
2 1
|
eqnetrrid |
|
4 |
3
|
xpcogend |
|