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 ) ) = (/) |
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 ) ) = (/) |