Theorem cosnopne

Description: Composition of two ordered pair singletons with non-matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023)

	Ref	Expression
Hypotheses	cosnopne.b	$$⊢\phi \to B\in W$$
	cosnopne.c	$$⊢\phi \to C\in X$$
	cosnopne.1	$$⊢\phi \to A\ne D$$
Assertion	cosnopne	$$⊢\phi \to \left\{⟨A,B⟩\right\}\circ \left\{⟨C,D⟩\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		cosnopne.b	$$⊢\phi \to B\in W$$
2		cosnopne.c	$$⊢\phi \to C\in X$$
3		cosnopne.1	$$⊢\phi \to A\ne D$$
4		dmsnopg	$$⊢B\in W\to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
5	1 4	syl	$$⊢\phi \to \mathrm{dom}\left\{⟨A,B⟩\right\}=\left\{A\right\}$$
6		rnsnopg	$$⊢C\in X\to \mathrm{ran}\left\{⟨C,D⟩\right\}=\left\{D\right\}$$
7	2 6	syl	$$⊢\phi \to \mathrm{ran}\left\{⟨C,D⟩\right\}=\left\{D\right\}$$
8	5 7	ineq12d	$$⊢\phi \to \mathrm{dom}\left\{⟨A,B⟩\right\}\cap \mathrm{ran}\left\{⟨C,D⟩\right\}=\left\{A\right\}\cap \left\{D\right\}$$
9		disjsn2	$$⊢A\ne D\to \left\{A\right\}\cap \left\{D\right\}=\varnothing$$
10	3 9	syl	$$⊢\phi \to \left\{A\right\}\cap \left\{D\right\}=\varnothing$$
11	8 10	eqtrd	$$⊢\phi \to \mathrm{dom}\left\{⟨A,B⟩\right\}\cap \mathrm{ran}\left\{⟨C,D⟩\right\}=\varnothing$$
12	11	coemptyd	$$⊢\phi \to \left\{⟨A,B⟩\right\}\circ \left\{⟨C,D⟩\right\}=\varnothing$$