This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times C) = \emptyset$

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