Theorem xp01disjl

Description: Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		1n0	$$⊢1_{𝑜}\ne \varnothing$$
2	1	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
3		disjsn2	$$⊢\varnothing \ne 1_{𝑜}\to \left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing$$
4		xpdisj1	$$⊢\left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing \to \left(\left\{\varnothing \right\}\times A\right)\cap \left(\left\{1_{𝑜}\right\}\times C\right)=\varnothing$$
5	2 3 4	mp2b	$$⊢\left(\left\{\varnothing \right\}\times A\right)\cap \left(\left\{1_{𝑜}\right\}\times C\right)=\varnothing$$