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 “ 𝐴 ) ∩ ( inr “ 𝐵 ) ) = ∅

Proof

Step	Hyp	Ref	Expression
1		incom	⊢ ( ( inr “ 𝐵 ) ∩ ( inl “ 𝐴 ) ) = ( ( inl “ 𝐴 ) ∩ ( inr “ 𝐵 ) )
2		imassrn	⊢ ( inr “ 𝐵 ) ⊆ ran inr
3		djurf1o	⊢ inr : V –1-1-onto→ ( { 1o } × V )
4		f1of	⊢ ( inr : V –1-1-onto→ ( { 1o } × V ) → inr : V ⟶ ( { 1o } × V ) )
5		frn	⊢ ( inr : V ⟶ ( { 1o } × V ) → ran inr ⊆ ( { 1o } × V ) )
6	3 4 5	mp2b	⊢ ran inr ⊆ ( { 1o } × V )
7	2 6	sstri	⊢ ( inr “ 𝐵 ) ⊆ ( { 1o } × V )
8		incom	⊢ ( ( inl “ 𝐴 ) ∩ ( { 1o } × V ) ) = ( ( { 1o } × V ) ∩ ( inl “ 𝐴 ) )
9		imassrn	⊢ ( inl “ 𝐴 ) ⊆ ran inl
10		djulf1o	⊢ inl : V –1-1-onto→ ( { ∅ } × V )
11		f1of	⊢ ( inl : V –1-1-onto→ ( { ∅ } × V ) → inl : V ⟶ ( { ∅ } × V ) )
12		frn	⊢ ( inl : V ⟶ ( { ∅ } × V ) → ran inl ⊆ ( { ∅ } × V ) )
13	10 11 12	mp2b	⊢ ran inl ⊆ ( { ∅ } × V )
14	9 13	sstri	⊢ ( inl “ 𝐴 ) ⊆ ( { ∅ } × V )
15		1n0	⊢ 1o ≠ ∅
16	15	necomi	⊢ ∅ ≠ 1o
17		disjsn2	⊢ ( ∅ ≠ 1o → ( { ∅ } ∩ { 1o } ) = ∅ )
18		xpdisj1	⊢ ( ( { ∅ } ∩ { 1o } ) = ∅ → ( ( { ∅ } × V ) ∩ ( { 1o } × V ) ) = ∅ )
19	16 17 18	mp2b	⊢ ( ( { ∅ } × V ) ∩ ( { 1o } × V ) ) = ∅
20		ssdisj	⊢ ( ( ( inl “ 𝐴 ) ⊆ ( { ∅ } × V ) ∧ ( ( { ∅ } × V ) ∩ ( { 1o } × V ) ) = ∅ ) → ( ( inl “ 𝐴 ) ∩ ( { 1o } × V ) ) = ∅ )
21	14 19 20	mp2an	⊢ ( ( inl “ 𝐴 ) ∩ ( { 1o } × V ) ) = ∅
22	8 21	eqtr3i	⊢ ( ( { 1o } × V ) ∩ ( inl “ 𝐴 ) ) = ∅
23		ssdisj	⊢ ( ( ( inr “ 𝐵 ) ⊆ ( { 1o } × V ) ∧ ( ( { 1o } × V ) ∩ ( inl “ 𝐴 ) ) = ∅ ) → ( ( inr “ 𝐵 ) ∩ ( inl “ 𝐴 ) ) = ∅ )
24	7 22 23	mp2an	⊢ ( ( inr “ 𝐵 ) ∩ ( inl “ 𝐴 ) ) = ∅
25	1 24	eqtr3i	⊢ ( ( inl “ 𝐴 ) ∩ ( inr “ 𝐵 ) ) = ∅