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\left[A\right]\cap inr\left[B\right]=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		incom	$$⊢inr\left[B\right]\cap inl\left[A\right]=inl\left[A\right]\cap inr\left[B\right]$$
2		imassrn	$$⊢inr\left[B\right]\subseteq \mathrm{ran}inr$$
3		djurf1o	$$⊢inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}$$
4		f1of	$$⊢inr:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{1_{𝑜}\right\}\times \mathrm{V}\to inr:\mathrm{V}⟶\left\{1_{𝑜}\right\}\times \mathrm{V}$$
5		frn	$$⊢inr:\mathrm{V}⟶\left\{1_{𝑜}\right\}\times \mathrm{V}\to \mathrm{ran}inr\subseteq \left\{1_{𝑜}\right\}\times \mathrm{V}$$
6	3 4 5	mp2b	$$⊢\mathrm{ran}inr\subseteq \left\{1_{𝑜}\right\}\times \mathrm{V}$$
7	2 6	sstri	$$⊢inr\left[B\right]\subseteq \left\{1_{𝑜}\right\}\times \mathrm{V}$$
8		incom	$$⊢inl\left[A\right]\cap \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)=\left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\cap inl\left[A\right]$$
9		imassrn	$$⊢inl\left[A\right]\subseteq \mathrm{ran}inl$$
10		djulf1o	$$⊢inl:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\times \mathrm{V}$$
11		f1of	$$⊢inl:\mathrm{V}\underset{1-1\; onto}{⟶}\left\{\varnothing \right\}\times \mathrm{V}\to inl:\mathrm{V}⟶\left\{\varnothing \right\}\times \mathrm{V}$$
12		frn	$$⊢inl:\mathrm{V}⟶\left\{\varnothing \right\}\times \mathrm{V}\to \mathrm{ran}inl\subseteq \left\{\varnothing \right\}\times \mathrm{V}$$
13	10 11 12	mp2b	$$⊢\mathrm{ran}inl\subseteq \left\{\varnothing \right\}\times \mathrm{V}$$
14	9 13	sstri	$$⊢inl\left[A\right]\subseteq \left\{\varnothing \right\}\times \mathrm{V}$$
15		1n0	$$⊢1_{𝑜}\ne \varnothing$$
16	15	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
17		disjsn2	$$⊢\varnothing \ne 1_{𝑜}\to \left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing$$
18		xpdisj1	$$⊢\left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing \to \left(\left\{\varnothing \right\}\times \mathrm{V}\right)\cap \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)=\varnothing$$
19	16 17 18	mp2b	$$⊢\left(\left\{\varnothing \right\}\times \mathrm{V}\right)\cap \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)=\varnothing$$
20		ssdisj	$$⊢\left(inl\left[A\right]\subseteq \left\{\varnothing \right\}\times \mathrm{V}\wedge \left(\left\{\varnothing \right\}\times \mathrm{V}\right)\cap \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)=\varnothing \right)\to inl\left[A\right]\cap \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)=\varnothing$$
21	14 19 20	mp2an	$$⊢inl\left[A\right]\cap \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)=\varnothing$$
22	8 21	eqtr3i	$$⊢\left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\cap inl\left[A\right]=\varnothing$$
23		ssdisj	$$⊢\left(inr\left[B\right]\subseteq \left\{1_{𝑜}\right\}\times \mathrm{V}\wedge \left(\left\{1_{𝑜}\right\}\times \mathrm{V}\right)\cap inl\left[A\right]=\varnothing \right)\to inr\left[B\right]\cap inl\left[A\right]=\varnothing$$
24	7 22 23	mp2an	$$⊢inr\left[B\right]\cap inl\left[A\right]=\varnothing$$
25	1 24	eqtr3i	$$⊢inl\left[A\right]\cap inr\left[B\right]=\varnothing$$