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	|- ( ph -> B e. W )
	cosnopne.c	|- ( ph -> C e. X )
	cosnopne.1	|- ( ph -> A =/= D )
Assertion	cosnopne	|- ( ph -> ( { <. A , B >. } o. { <. C , D >. } ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		cosnopne.b	|- ( ph -> B e. W )
2		cosnopne.c	|- ( ph -> C e. X )
3		cosnopne.1	|- ( ph -> A =/= D )
4		dmsnopg	|- ( B e. W -> dom { <. A , B >. } = { A } )
5	1 4	syl	|- ( ph -> dom { <. A , B >. } = { A } )
6		rnsnopg	|- ( C e. X -> ran { <. C , D >. } = { D } )
7	2 6	syl	|- ( ph -> ran { <. C , D >. } = { D } )
8	5 7	ineq12d	|- ( ph -> ( dom { <. A , B >. } i^i ran { <. C , D >. } ) = ( { A } i^i { D } ) )
9		disjsn2	|- ( A =/= D -> ( { A } i^i { D } ) = (/) )
10	3 9	syl	|- ( ph -> ( { A } i^i { D } ) = (/) )
11	8 10	eqtrd	|- ( ph -> ( dom { <. A , B >. } i^i ran { <. C , D >. } ) = (/) )
12	11	coemptyd	|- ( ph -> ( { <. A , B >. } o. { <. C , D >. } ) = (/) )