fuco22a

Description: The morphism part of the functor composition bifunctor. See also fuco22 . (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	fuco22a.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fuco22a.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐾 , 𝐹 ⟩ )
	fuco22a.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝑅 , 𝑀 ⟩ )
	fuco22a.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝑀 ) )
	fuco22a.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑅 ) )
Assertion	fuco22a	⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑅 ) ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco22a.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fuco22a.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐾 , 𝐹 ⟩ )
3		fuco22a.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝑅 , 𝑀 ⟩ )
4		fuco22a.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝑀 ) )
5		fuco22a.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑅 ) )
6		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
7		df-rel	⊢ ( Rel ( 𝐷 Func 𝐸 ) ↔ ( 𝐷 Func 𝐸 ) ⊆ ( V × V ) )
8	6 7	mpbi	⊢ ( 𝐷 Func 𝐸 ) ⊆ ( V × V )
9		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
10	9	natrcl	⊢ ( 𝐵 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑅 ) → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑅 ∈ ( 𝐷 Func 𝐸 ) ) )
11	5 10	syl	⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑅 ∈ ( 𝐷 Func 𝐸 ) ) )
12	11	simpld	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
13	8 12	sselid	⊢ ( 𝜑 → 𝐾 ∈ ( V × V ) )
14		1st2ndb	⊢ ( 𝐾 ∈ ( V × V ) ↔ 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
15	13 14	sylib	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ )
16		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
17		df-rel	⊢ ( Rel ( 𝐶 Func 𝐷 ) ↔ ( 𝐶 Func 𝐷 ) ⊆ ( V × V ) )
18	16 17	mpbi	⊢ ( 𝐶 Func 𝐷 ) ⊆ ( V × V )
19		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
20	19	natrcl	⊢ ( 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝑀 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑀 ∈ ( 𝐶 Func 𝐷 ) ) )
21	4 20	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑀 ∈ ( 𝐶 Func 𝐷 ) ) )
22	21	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
23	18 22	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )
24		1st2ndb	⊢ ( 𝐹 ∈ ( V × V ) ↔ 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
25	23 24	sylib	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
26	15 25	opeq12d	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐹 ⟩ = ⟨ ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ , ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ⟩ )
27	2 26	eqtrd	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ , ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ⟩ )
28	11	simprd	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐷 Func 𝐸 ) )
29	8 28	sselid	⊢ ( 𝜑 → 𝑅 ∈ ( V × V ) )
30		1st2ndb	⊢ ( 𝑅 ∈ ( V × V ) ↔ 𝑅 = ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ )
31	29 30	sylib	⊢ ( 𝜑 → 𝑅 = ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ )
32	21	simprd	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐶 Func 𝐷 ) )
33	18 32	sselid	⊢ ( 𝜑 → 𝑀 ∈ ( V × V ) )
34		1st2ndb	⊢ ( 𝑀 ∈ ( V × V ) ↔ 𝑀 = ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ )
35	33 34	sylib	⊢ ( 𝜑 → 𝑀 = ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ )
36	31 35	opeq12d	⊢ ( 𝜑 → ⟨ 𝑅 , 𝑀 ⟩ = ⟨ ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ , ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ ⟩ )
37	3 36	eqtrd	⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ , ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ ⟩ )
38	19 4	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ ) )
39	9 5	nat1st2nd	⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝑅 ) , ( 2^nd ‘ 𝑅 ) ⟩ ) )
40	1 27 37 38 39	fuco22	⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝐵 ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑅 ) ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐾 ) ( ( 1^st ‘ 𝑀 ) ‘ 𝑥 ) ) ‘ ( 𝐴 ‘ 𝑥 ) ) ) ) )

Metamath Proof Explorer

Theorem fuco22a

Proof