Theorem opropabco

Description: Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010)

	Ref	Expression
Hypotheses	opropabco.1	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑅 )
	opropabco.2	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑆 )
	opropabco.3	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ⟨ 𝐵 , 𝐶 ⟩ ) }
	opropabco.4	⊢ 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐵 𝑀 𝐶 ) ) }
Assertion	opropabco	⊢ ( 𝑀 Fn ( 𝑅 × 𝑆 ) → 𝐺 = ( 𝑀 ∘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		opropabco.1	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑅 )
2		opropabco.2	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑆 )
3		opropabco.3	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ⟨ 𝐵 , 𝐶 ⟩ ) }
4		opropabco.4	⊢ 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐵 𝑀 𝐶 ) ) }
5		opelxpi	⊢ ( ( 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆 ) → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅 × 𝑆 ) )
6	1 2 5	syl2anc	⊢ ( 𝑥 ∈ 𝐴 → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑅 × 𝑆 ) )
7		df-ov	⊢ ( 𝐵 𝑀 𝐶 ) = ( 𝑀 ‘ ⟨ 𝐵 , 𝐶 ⟩ )
8	7	eqeq2i	⊢ ( 𝑦 = ( 𝐵 𝑀 𝐶 ) ↔ 𝑦 = ( 𝑀 ‘ ⟨ 𝐵 , 𝐶 ⟩ ) )
9	8	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐵 𝑀 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑀 ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) )
10	9	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐵 𝑀 𝐶 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑀 ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) }
11	4 10	eqtri	⊢ 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑀 ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) }
12	6 3 11	fnopabco	⊢ ( 𝑀 Fn ( 𝑅 × 𝑆 ) → 𝐺 = ( 𝑀 ∘ 𝐹 ) )