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