cofu2nd

Description: Value of the morphism part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
	cofu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cofu2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	cofu2nd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		cofuval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		cofuval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4		cofu2nd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		cofu2nd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6	1 2 3	cofuval	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ )
7	6	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ) )
8		fvex	⊢ ( 1^st ‘ 𝐺 ) ∈ V
9		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
10	8 9	coex	⊢ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) ∈ V
11	1	fvexi	⊢ 𝐵 ∈ V
12	11 11	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ∈ V
13	10 12	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) ⟩ ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
14	7 13	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) )
15		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
16	15	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) )
19	16 18	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
20	15 17	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) = ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) )
21	19 20	coeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) )
22		ovex	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∈ V
23		ovex	⊢ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ∈ V
24	22 23	coex	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) ∈ V
25	24	a1i	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) ∈ V )
26	14 21 4 5 25	ovmpod	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) )

Metamath Proof Explorer

Theorem cofu2nd

Proof