Theorem cofuval2

Description: Value of the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuval2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cofuval2.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	cofuval2.x	⊢ ( 𝜑 → 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 )
Assertion	cofuval2	⊢ ( 𝜑 → ( ⟨ 𝐻 , 𝐾 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐻 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		cofuval2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cofuval2.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3		cofuval2.x	⊢ ( 𝜑 → 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 )
4		df-br	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
5	2 4	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
6		df-br	⊢ ( 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 ↔ ⟨ 𝐻 , 𝐾 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
7	3 6	sylib	⊢ ( 𝜑 → ⟨ 𝐻 , 𝐾 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
8	1 5 7	cofuval	⊢ ( 𝜑 → ( ⟨ 𝐻 , 𝐾 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) ) ⟩ )
9		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
10		brrelex12	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐻 ( 𝐷 Func 𝐸 ) 𝐾 ) → ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) )
11	9 3 10	sylancr	⊢ ( 𝜑 → ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) )
12		op1stg	⊢ ( ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) → ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐻 )
13	11 12	syl	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐻 )
14		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
15		brrelex12	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ) → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
16	14 2 15	sylancr	⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
17		op1stg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
18	16 17	syl	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
19	13 18	coeq12d	⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝐻 ∘ 𝐹 ) )
20		op2ndg	⊢ ( ( 𝐻 ∈ V ∧ 𝐾 ∈ V ) → ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐾 )
21	11 20	syl	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐾 )
22	21	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) = 𝐾 )
23	18	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
24	23	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
25	23	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
26	22 24 25	oveq123d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
27		op2ndg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
28	16 27	syl	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
29	28	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
30	29	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
31	26 30	coeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) )
32	31	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) )
33	19 32	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1st ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ∘ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑥 ) ( 2nd ‘ ⟨ 𝐻 , 𝐾 ⟩ ) ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑦 ) ) ) ⟩ = ⟨ ( 𝐻 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )
34	8 33	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐻 , 𝐾 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐻 ∘ 𝐹 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) ⟩ )