# Metamath Proof Explorer

## Theorem djuin

Description: The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022)

Ref Expression
Assertion djuin
`|- ( ( inl " A ) i^i ( inr " B ) ) = (/)`

### Proof

Step Hyp Ref Expression
1 incom
` |-  ( ( inr " B ) i^i ( inl " A ) ) = ( ( inl " A ) i^i ( inr " B ) )`
2 imassrn
` |-  ( inr " B ) C_ ran inr`
3 djurf1o
` |-  inr : _V -1-1-onto-> ( { 1o } X. _V )`
4 f1of
` |-  ( inr : _V -1-1-onto-> ( { 1o } X. _V ) -> inr : _V --> ( { 1o } X. _V ) )`
5 frn
` |-  ( inr : _V --> ( { 1o } X. _V ) -> ran inr C_ ( { 1o } X. _V ) )`
6 3 4 5 mp2b
` |-  ran inr C_ ( { 1o } X. _V )`
7 2 6 sstri
` |-  ( inr " B ) C_ ( { 1o } X. _V )`
8 incom
` |-  ( ( inl " A ) i^i ( { 1o } X. _V ) ) = ( ( { 1o } X. _V ) i^i ( inl " A ) )`
9 imassrn
` |-  ( inl " A ) C_ ran inl`
10 djulf1o
` |-  inl : _V -1-1-onto-> ( { (/) } X. _V )`
11 f1of
` |-  ( inl : _V -1-1-onto-> ( { (/) } X. _V ) -> inl : _V --> ( { (/) } X. _V ) )`
12 frn
` |-  ( inl : _V --> ( { (/) } X. _V ) -> ran inl C_ ( { (/) } X. _V ) )`
13 10 11 12 mp2b
` |-  ran inl C_ ( { (/) } X. _V )`
14 9 13 sstri
` |-  ( inl " A ) C_ ( { (/) } X. _V )`
15 1n0
` |-  1o =/= (/)`
16 15 necomi
` |-  (/) =/= 1o`
17 disjsn2
` |-  ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) )`
18 xpdisj1
` |-  ( ( { (/) } i^i { 1o } ) = (/) -> ( ( { (/) } X. _V ) i^i ( { 1o } X. _V ) ) = (/) )`
19 16 17 18 mp2b
` |-  ( ( { (/) } X. _V ) i^i ( { 1o } X. _V ) ) = (/)`
20 ssdisj
` |-  ( ( ( inl " A ) C_ ( { (/) } X. _V ) /\ ( ( { (/) } X. _V ) i^i ( { 1o } X. _V ) ) = (/) ) -> ( ( inl " A ) i^i ( { 1o } X. _V ) ) = (/) )`
21 14 19 20 mp2an
` |-  ( ( inl " A ) i^i ( { 1o } X. _V ) ) = (/)`
22 8 21 eqtr3i
` |-  ( ( { 1o } X. _V ) i^i ( inl " A ) ) = (/)`
23 ssdisj
` |-  ( ( ( inr " B ) C_ ( { 1o } X. _V ) /\ ( ( { 1o } X. _V ) i^i ( inl " A ) ) = (/) ) -> ( ( inr " B ) i^i ( inl " A ) ) = (/) )`
24 7 22 23 mp2an
` |-  ( ( inr " B ) i^i ( inl " A ) ) = (/)`
25 1 24 eqtr3i
` |-  ( ( inl " A ) i^i ( inr " B ) ) = (/)`