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