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	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	cosnopne.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	cosnopne.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
Assertion	cosnopne	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		cosnopne.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
2		cosnopne.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
3		cosnopne.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐷 )
4		dmsnopg	⊢ ( 𝐵 ∈ 𝑊 → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
5	1 4	syl	⊢ ( 𝜑 → dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 } )
6		rnsnopg	⊢ ( 𝐶 ∈ 𝑋 → ran { ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐷 } )
7	2 6	syl	⊢ ( 𝜑 → ran { ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐷 } )
8	5 7	ineq12d	⊢ ( 𝜑 → ( dom { ⟨ 𝐴 , 𝐵 ⟩ } ∩ ran { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( { 𝐴 } ∩ { 𝐷 } ) )
9		disjsn2	⊢ ( 𝐴 ≠ 𝐷 → ( { 𝐴 } ∩ { 𝐷 } ) = ∅ )
10	3 9	syl	⊢ ( 𝜑 → ( { 𝐴 } ∩ { 𝐷 } ) = ∅ )
11	8 10	eqtrd	⊢ ( 𝜑 → ( dom { ⟨ 𝐴 , 𝐵 ⟩ } ∩ ran { ⟨ 𝐶 , 𝐷 ⟩ } ) = ∅ )
12	11	coemptyd	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ∅ )