Theorem xp01disj

Description: Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007)

	Ref	Expression
Assertion	xp01disj	$$⊢\left(A\times \left\{\varnothing \right\}\right)\cap \left(C\times \left\{1_{𝑜}\right\}\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		1n0	$$⊢1_{𝑜}\ne \varnothing$$
2	1	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
3		xpsndisj	$$⊢\varnothing \ne 1_{𝑜}\to \left(A\times \left\{\varnothing \right\}\right)\cap \left(C\times \left\{1_{𝑜}\right\}\right)=\varnothing$$
4	2 3	ax-mp	$$⊢\left(A\times \left\{\varnothing \right\}\right)\cap \left(C\times \left\{1_{𝑜}\right\}\right)=\varnothing$$