fucoisfunc2lem2

Description: Lemma for fucoisfunc2 . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	⊢ 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
2		fucoisfunc2lem1.o	⊢ 𝑂 = ( ∘_func ↾ 𝑊 )
3		fucoisfunc2lem1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		fucoisfunc2lem1.r	⊢ 𝑅 = ( Hom ‘ 𝐶 )
5		fucoisfunc2lem1.s	⊢ 𝑆 = ( Hom ‘ 𝐸 )
6		fucoisfunc2lem1.v	⊢ ∙ = ( comp ‘ 𝐸 )
7		fucoisfunc2.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
8		fucoisfunc2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
9		fucoisfunc2.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
10		fucoisfunc2.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
11		fucoisfunc2.x	⊢ · = ( comp ‘ 𝑇 )
12		fucoisfunc2.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		fucoisfunc2.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
14		fucoisfunc2.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
15		fucoisfunc2.k	⊢ 𝐾 = ( Id ‘ 𝐸 )
16		fucoisfunc2lem2.j	⊢ 𝐽 = ( Id ‘ 𝑄 )
17		fucoisfunc2lem2.y	⊢ ⚬ = ( comp ‘ 𝑄 )
18	1 7 8 2 9 10 16 11 17 12 13 14	fucoisfunc	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
19	7	fveq2i	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
20	9 19	eqtri	⊢ 𝐻 = ( Hom ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
21	1 20	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 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) )
22	21	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 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) )
23	18 22	bitr4di	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
24	7	xpcfucbas	⊢ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( Base ‘ 𝑇 )
25	1 24	eqtri	⊢ 𝑊 = ( Base ‘ 𝑇 )
26		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
27	26 13 14	fuccat	⊢ ( 𝜑 → ( 𝐷 FuncCat 𝐸 ) ∈ Cat )
28		eqid	⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 )
29	28 12 13	fuccat	⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐷 ) ∈ Cat )
30	7 27 29	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ) → 𝑇 ∈ Cat )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ) → 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) )
33	25 8 3 9 10 16 15 11 17 6 31 32	fucidcobi	⊢ ( ( 𝜑 ∧ 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ) → ( ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ↔ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) )
34	33	pm5.32da	⊢ ( 𝜑 → ( ( 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐽 ‘ ( 𝑂 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ⚬ ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) ) ) ↔ ( 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) ) )
35	23 34	bitrd	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) ) )
36	1 2 3 4 5 6	fucoisfunc2lem1	⊢ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ∈ ( ( 𝑂 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑛 ) ) ) ) ↔ ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) )
37	21 36	bitri	⊢ ( 𝑃 ∈ 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 ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) )
38	37	anbi1i	⊢ ( ( 𝑃 ∈ X 𝑤 ∈ ( 𝑊 × 𝑊 ) ( ( ( 𝑂 ‘ ( 1^st ‘ 𝑤 ) ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ ( 2^nd ‘ 𝑤 ) ) ) ↑_m ( 𝐻 ‘ 𝑤 ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) )
39	35 38	bitrdi	⊢ ( 𝜑 → ( 𝑂 ( 𝑇 Func 𝑄 ) 𝑃 ↔ ( ( 𝑃 = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ( 𝑢 𝑃 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝑊 ∀ 𝑛 ∈ 𝑊 ( ( 𝑚 𝑃 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝑃 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) 𝑆 ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ ℎ ∈ ( 𝑥 𝑅 𝑦 ) ( ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑦 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑚 ) ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ ( 𝑂 ‘ 𝑛 ) ) 𝑦 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑚 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑥 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑛 ) ) ‘ 𝑦 ) ) ( ( 𝑝 ( 𝑚 𝑃 𝑛 ) 𝑞 ) ‘ 𝑥 ) ) ) ) ) ∧ ∀ 𝑥 ∈ 𝑊 ( ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑥 ) ‘ ( 𝐼 ‘ 𝑥 ) ) ‘ 𝑡 ) = ( 𝐾 ‘ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) ) ∧ ∀ 𝑦 ∈ 𝑊 ∀ 𝑧 ∈ 𝑊 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ∀ 𝑡 ∈ 𝐵 ( ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑚 ) ) ‘ 𝑡 ) = ( ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ‘ 𝑡 ) ( ⟨ ( ( 1^st ‘ ( 𝑂 ‘ 𝑥 ) ) ‘ 𝑡 ) , ( ( 1^st ‘ ( 𝑂 ‘ 𝑦 ) ) ‘ 𝑡 ) ⟩ ∙ ( ( 1^st ‘ ( 𝑂 ‘ 𝑧 ) ) ‘ 𝑡 ) ) ( ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ‘ 𝑡 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fucoisfunc2lem2

Proof