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

Metamath Proof Explorer

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

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