fucof21

Description: The morphism part of the functor composition bifunctor maps a hom-set of the product category into a set of natural transformations. (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fucof21.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fucof21.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucof21.j	⊢ 𝐽 = ( Hom ‘ 𝑇 )
	fucof21.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
	fucof21.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
	fucof21.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
Assertion	fucof21	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) : ( 𝑈 𝐽 𝑉 ) ⟶ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucof21.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fucof21.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
3		fucof21.j	⊢ 𝐽 = ( Hom ‘ 𝑇 )
4		fucof21.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
5		fucof21.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
6		fucof21.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
7		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
8		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
9	4 5 7 8	fuco2eld3	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ∧ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ) )
10	9	simprd	⊢ ( 𝜑 → ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) )
11	9	simpld	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
12	4 5 7 8	fuco2eld2	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ )
13	4 6 7 8	fuco2eld3	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ∧ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ) )
14	13	simprd	⊢ ( 𝜑 → ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) )
15	13	simpld	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) )
16	4 6 7 8	fuco2eld2	⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ⟩ )
17	1 10 11 12 14 15 16	fuco21	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) = ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) , 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ‘ 𝑥 ) ) , ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ‘ 𝑥 ) ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
18	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
19	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → 𝑈 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ )
20	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → 𝑉 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ⟩ )
21		simprr	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) )
22		simprl	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) )
23	18 19 20 21 22	fuco22	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → ( 𝑏 ( 𝑈 𝑃 𝑉 ) 𝑎 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ‘ 𝑥 ) ) , ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ‘ 𝑥 ) ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
24	18 21 22 19 20	fuco22nat	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → ( 𝑏 ( 𝑈 𝑃 𝑉 ) 𝑎 ) ∈ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )
25	23 24	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) ∧ 𝑎 ∈ ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ‘ 𝑥 ) ) , ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) ‘ ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ‘ 𝑥 ) ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ( ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ∈ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )
26	2	xpcfucbas	⊢ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( Base ‘ 𝑇 )
27	5 4	eleqtrd	⊢ ( 𝜑 → 𝑈 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
28	6 4	eleqtrd	⊢ ( 𝜑 → 𝑉 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
29	2 26 3 27 28	xpcfuchom	⊢ ( 𝜑 → ( 𝑈 𝐽 𝑉 ) = ( ( ( 1^st ‘ 𝑈 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑉 ) ) × ( ( 2^nd ‘ 𝑈 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑉 ) ) ) )
30	12	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝑈 ) = ( 1^st ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ ) )
31		opex	⊢ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ∈ V
32		opex	⊢ ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ∈ V
33	31 32	op1st	⊢ ( 1^st ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩
34	30 33	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ )
35	16	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝑉 ) = ( 1^st ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ⟩ ) )
36		opex	⊢ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ∈ V
37		opex	⊢ ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ∈ V
38	36 37	op1st	⊢ ( 1^st ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ⟩ ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩
39	35 38	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ 𝑉 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ )
40	34 39	oveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑈 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑉 ) ) = ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) )
41	12	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ 𝑈 ) = ( 2^nd ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ ) )
42	31 32	op2nd	⊢ ( 2^nd ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ ) = ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩
43	41 42	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ )
44	16	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ 𝑉 ) = ( 2^nd ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ⟩ ) )
45	36 37	op2nd	⊢ ( 2^nd ‘ ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ⟩ ) = ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩
46	44 45	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ 𝑉 ) = ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ )
47	43 46	oveq12d	⊢ ( 𝜑 → ( ( 2^nd ‘ 𝑈 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑉 ) ) = ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) )
48	40 47	xpeq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝑈 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑉 ) ) × ( ( 2^nd ‘ 𝑈 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑉 ) ) ) = ( ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) × ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) )
49	29 48	eqtrd	⊢ ( 𝜑 → ( 𝑈 𝐽 𝑉 ) = ( ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ( 1^st ‘ 𝑉 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑉 ) ) ⟩ ) × ( ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑉 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑉 ) ) ⟩ ) ) )
50	17 25 49	fmpodg	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) : ( 𝑈 𝐽 𝑉 ) ⟶ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )

Metamath Proof Explorer

Theorem fucof21

Proof