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 
|- ( ( { (/) } X. A ) i^i ( { 1o } X. C ) ) = (/)

Proof

Step Hyp Ref Expression
1 1n0 
 |-  1o =/= (/)
2 1 necomi 
 |-  (/) =/= 1o
3 disjsn2 
 |-  ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) )
4 xpdisj1 
 |-  ( ( { (/) } i^i { 1o } ) = (/) -> ( ( { (/) } X. A ) i^i ( { 1o } X. C ) ) = (/) )
5 2 3 4 mp2b 
 |-  ( ( { (/) } X. A ) i^i ( { 1o } X. C ) ) = (/)