fucoisfunc

Description: A characterization of functors with the object part of functor composition, in terms of an exact morphism function and compatible component functors. See fucoisfunc2 for the componentwise form. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucoisfunc.w	⊢ 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
	fucoisfunc.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucoisfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoisfunc.o	⊢ 𝑂 = ( ∘_func ↾ 𝑊 )
	fucoisfunc.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
	fucoisfunc.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
	fucoisfunc.j	⊢ 𝐽 = ( Id ‘ 𝑄 )
	fucoisfunc.x	⊢ · = ( comp ‘ 𝑇 )
	fucoisfunc.y	⊢ ⚬ = ( comp ‘ 𝑄 )
	fucoisfunc.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoisfunc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	fucoisfunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
Assertion	fucoisfunc	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	⊢ 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
2		fucoisfunc.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
3		fucoisfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
4		fucoisfunc.o	⊢ 𝑂 = ( ∘_func ↾ 𝑊 )
5		fucoisfunc.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
6		fucoisfunc.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
7		fucoisfunc.j	⊢ 𝐽 = ( Id ‘ 𝑄 )
8		fucoisfunc.x	⊢ · = ( comp ‘ 𝑇 )
9		fucoisfunc.y	⊢ ⚬ = ( comp ‘ 𝑄 )
10		fucoisfunc.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
11		fucoisfunc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
12		fucoisfunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
13	2	xpcfucbas	⊢ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( Base ‘ 𝑇 )
14	1 13	eqtri	⊢ 𝑊 = ( Base ‘ 𝑇 )
15	3	fucbas	⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ 𝑄 )
16		eqid	⊢ ( 𝐶 Nat 𝐸 ) = ( 𝐶 Nat 𝐸 )
17	3 16	fuchom	⊢ ( 𝐶 Nat 𝐸 ) = ( Hom ‘ 𝑄 )
18		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
19	18 11 12	fuccat	⊢ ( 𝜑 → ( 𝐷 FuncCat 𝐸 ) ∈ Cat )
20		eqid	⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 )
21	20 10 11	fuccat	⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐷 ) ∈ Cat )
22	2 19 21	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
23	3 10 12	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
24	14 15 5 17 6 7 8 9 22 23	isfunc	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) ∧ 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
25		rescofuf	⊢ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 )
26	1	reseq2i	⊢ ( ∘_func ↾ 𝑊 ) = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
27	4 26	eqtri	⊢ 𝑂 = ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
28	27 1	feq12i	⊢ ( 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) ↔ ( ∘_func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 ) )
29	25 28	mpbir	⊢ 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 )
30		3anass	⊢ ( ( 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) ∧ 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) ∧ ( 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
31	29 30	mpbiran	⊢ ( ( 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) ∧ 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) )
32	24 31	bitrdi	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
33	2	fveq2i	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
34	5 33	eqtri	⊢ 𝐻 = ( Hom ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
35	1 34	fucofulem2	⊢ ( 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) )
36	35	anbi1i	⊢ ( ( 𝑃 ∈ X 𝑧 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) )
37	32 36	bitrdi	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fucoisfunc

Proof