Theorem coprprop

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

	Ref	Expression
Hypotheses	brprop.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	brprop.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	brprop.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	brprop.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
	mptprop.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
	coprprop.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑋 )
	coprprop.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
	coprprop.1	⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
Assertion	coprprop	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ , ⟨ 𝐹 , 𝐶 ⟩ } ) = { ⟨ 𝐸 , 𝐵 ⟩ , ⟨ 𝐹 , 𝐷 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		brprop.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		brprop.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		brprop.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		brprop.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5		mptprop.1	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
6		coprprop.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑋 )
7		coprprop.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
8		coprprop.1	⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
9		coundir	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ∪ ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) )
10	1 2 6	cosnop	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) = { ⟨ 𝐸 , 𝐵 ⟩ } )
11	5	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
12	4 6 11	cosnopne	⊢ ( 𝜑 → ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) = ∅ )
13	10 12	uneq12d	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ∪ ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ) = ( { ⟨ 𝐸 , 𝐵 ⟩ } ∪ ∅ ) )
14		un0	⊢ ( { ⟨ 𝐸 , 𝐵 ⟩ } ∪ ∅ ) = { ⟨ 𝐸 , 𝐵 ⟩ }
15	13 14	eqtrdi	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ∪ ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ) = { ⟨ 𝐸 , 𝐵 ⟩ } )
16	9 15	syl5eq	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) = { ⟨ 𝐸 , 𝐵 ⟩ } )
17		coundir	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) ∪ ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) )
18	2 7 5	cosnopne	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) = ∅ )
19	3 4 7	cosnop	⊢ ( 𝜑 → ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) = { ⟨ 𝐹 , 𝐷 ⟩ } )
20	18 19	uneq12d	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) ∪ ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) ) = ( ∅ ∪ { ⟨ 𝐹 , 𝐷 ⟩ } ) )
21		0un	⊢ ( ∅ ∪ { ⟨ 𝐹 , 𝐷 ⟩ } ) = { ⟨ 𝐹 , 𝐷 ⟩ }
22	20 21	eqtrdi	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) ∪ ( { ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) ) = { ⟨ 𝐹 , 𝐷 ⟩ } )
23	17 22	syl5eq	⊢ ( 𝜑 → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) = { ⟨ 𝐹 , 𝐷 ⟩ } )
24	16 23	uneq12d	⊢ ( 𝜑 → ( ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ∪ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) ) = ( { ⟨ 𝐸 , 𝐵 ⟩ } ∪ { ⟨ 𝐹 , 𝐷 ⟩ } ) )
25		df-pr	⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
26		df-pr	⊢ { ⟨ 𝐸 , 𝐴 ⟩ , ⟨ 𝐹 , 𝐶 ⟩ } = ( { ⟨ 𝐸 , 𝐴 ⟩ } ∪ { ⟨ 𝐹 , 𝐶 ⟩ } )
27	25 26	coeq12i	⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ , ⟨ 𝐹 , 𝐶 ⟩ } ) = ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ ( { ⟨ 𝐸 , 𝐴 ⟩ } ∪ { ⟨ 𝐹 , 𝐶 ⟩ } ) )
28		coundi	⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ ( { ⟨ 𝐸 , 𝐴 ⟩ } ∪ { ⟨ 𝐹 , 𝐶 ⟩ } ) ) = ( ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ∪ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) )
29	27 28	eqtri	⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ , ⟨ 𝐹 , 𝐶 ⟩ } ) = ( ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐸 , 𝐴 ⟩ } ) ∪ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ∘ { ⟨ 𝐹 , 𝐶 ⟩ } ) )
30		df-pr	⊢ { ⟨ 𝐸 , 𝐵 ⟩ , ⟨ 𝐹 , 𝐷 ⟩ } = ( { ⟨ 𝐸 , 𝐵 ⟩ } ∪ { ⟨ 𝐹 , 𝐷 ⟩ } )
31	24 29 30	3eqtr4g	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } ∘ { ⟨ 𝐸 , 𝐴 ⟩ , ⟨ 𝐹 , 𝐶 ⟩ } ) = { ⟨ 𝐸 , 𝐵 ⟩ , ⟨ 𝐹 , 𝐷 ⟩ } )