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	⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐶 ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2	1	necomi	⊢ ∅ ≠ 1o
3		disjsn2	⊢ ( ∅ ≠ 1o → ( { ∅ } ∩ { 1o } ) = ∅ )
4		xpdisj1	⊢ ( ( { ∅ } ∩ { 1o } ) = ∅ → ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐶 ) ) = ∅ )
5	2 3 4	mp2b	⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 𝐶 ) ) = ∅