Theorem cosnop

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

	Ref	Expression
Hypotheses	cosnop.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	cosnop.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	cosnop.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
Assertion	cosnop	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐶 , 𝐴 ⟩ } ) = { ⟨ 𝐶 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		cosnop.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		cosnop.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		cosnop.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
4		snnzg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≠ ∅ )
5		xpco	⊢ ( { 𝐴 } ≠ ∅ → ( ( { 𝐴 } × { 𝐵 } ) ∘ ( { 𝐶 } × { 𝐴 } ) ) = ( { 𝐶 } × { 𝐵 } ) )
6	1 4 5	3syl	⊢ ( 𝜑 → ( ( { 𝐴 } × { 𝐵 } ) ∘ ( { 𝐶 } × { 𝐴 } ) ) = ( { 𝐶 } × { 𝐵 } ) )
7		xpsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )
9		xpsng	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑉 ) → ( { 𝐶 } × { 𝐴 } ) = { ⟨ 𝐶 , 𝐴 ⟩ } )
10	3 1 9	syl2anc	⊢ ( 𝜑 → ( { 𝐶 } × { 𝐴 } ) = { ⟨ 𝐶 , 𝐴 ⟩ } )
11	8 10	coeq12d	⊢ ( 𝜑 → ( ( { 𝐴 } × { 𝐵 } ) ∘ ( { 𝐶 } × { 𝐴 } ) ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐶 , 𝐴 ⟩ } ) )
12		xpsng	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐶 } × { 𝐵 } ) = { ⟨ 𝐶 , 𝐵 ⟩ } )
13	3 2 12	syl2anc	⊢ ( 𝜑 → ( { 𝐶 } × { 𝐵 } ) = { ⟨ 𝐶 , 𝐵 ⟩ } )
14	6 11 13	3eqtr3d	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐶 , 𝐴 ⟩ } ) = { ⟨ 𝐶 , 𝐵 ⟩ } )