fucofulem2

Description: Lemma for proving functor theorems. Maybe consider eufnfv to prove the uniqueness of a functor. (Contributed by Zhi Wang, 25-Sep-2025)

	Ref	Expression
Hypotheses	fucofulem2.b	⊢ 𝐵 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
	fucofulem2.h	⊢ 𝐻 = ( Hom ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
Assertion	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 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucofulem2.b	⊢ 𝐵 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) )
2		fucofulem2.h	⊢ 𝐻 = ( Hom ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
3		eqid	⊢ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
4		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
5	4	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
6		eqid	⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 )
7	6	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ ( 𝐶 FuncCat 𝐷 ) )
8	3 5 7	xpcbas	⊢ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( Base ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
9	1 8	eqtri	⊢ 𝐵 = ( Base ‘ ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) ) )
10	9	funcf2lem2	⊢ ( 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ ( 2^nd ‘ 𝑧 ) ) ) ↑_m ( 𝐻 ‘ 𝑧 ) ) ↔ ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) )
11		fnov	⊢ ( 𝐺 Fn ( 𝐵 × 𝐵 ) ↔ 𝐺 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑢 𝐺 𝑣 ) ) )
12		ffnfv	⊢ ( ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝑚 𝐺 𝑛 ) Fn ( 𝑚 𝐻 𝑛 ) ∧ ∀ 𝑟 ∈ ( 𝑚 𝐻 𝑛 ) ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) )
13		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
14	4 13	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
15		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
16	6 15	fuchom	⊢ ( 𝐶 Nat 𝐷 ) = ( Hom ‘ ( 𝐶 FuncCat 𝐷 ) )
17		simpl	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → 𝑚 ∈ 𝐵 )
18		simpr	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ 𝐵 )
19	3 9 14 16 2 17 18	xpchom	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( 𝑚 𝐻 𝑛 ) = ( ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) × ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ) )
20	19	fneq2d	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( ( 𝑚 𝐺 𝑛 ) Fn ( 𝑚 𝐻 𝑛 ) ↔ ( 𝑚 𝐺 𝑛 ) Fn ( ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) × ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ) ) )
21		fnov	⊢ ( ( 𝑚 𝐺 𝑛 ) Fn ( ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) × ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ) ↔ ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) )
22	20 21	bitrdi	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( ( 𝑚 𝐺 𝑛 ) Fn ( 𝑚 𝐻 𝑛 ) ↔ ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) ) )
23	19	raleqdv	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( ∀ 𝑟 ∈ ( 𝑚 𝐻 𝑛 ) ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑟 ∈ ( ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) × ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ) ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) )
24		fveq2	⊢ ( 𝑟 = ⟨ 𝑝 , 𝑞 ⟩ → ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) = ( ( 𝑚 𝐺 𝑛 ) ‘ ⟨ 𝑝 , 𝑞 ⟩ ) )
25		df-ov	⊢ ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) = ( ( 𝑚 𝐺 𝑛 ) ‘ ⟨ 𝑝 , 𝑞 ⟩ )
26	24 25	eqtr4di	⊢ ( 𝑟 = ⟨ 𝑝 , 𝑞 ⟩ → ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) = ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) )
27	26	eleq1d	⊢ ( 𝑟 = ⟨ 𝑝 , 𝑞 ⟩ → ( ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) )
28	27	ralxp	⊢ ( ∀ 𝑟 ∈ ( ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) × ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ) ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) )
29	23 28	bitrdi	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( ∀ 𝑟 ∈ ( 𝑚 𝐻 𝑛 ) ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) )
30	22 29	anbi12d	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( ( ( 𝑚 𝐺 𝑛 ) Fn ( 𝑚 𝐻 𝑛 ) ∧ ∀ 𝑟 ∈ ( 𝑚 𝐻 𝑛 ) ( ( 𝑚 𝐺 𝑛 ) ‘ 𝑟 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ) )
31	12 30	bitrid	⊢ ( ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) → ( ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ) )
32	31	adantl	⊢ ( ( ⊤ ∧ ( 𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵 ) ) → ( ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ) )
33	32	2ralbidva	⊢ ( ⊤ → ( ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ) )
34	33	mptru	⊢ ( ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ↔ ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) )
35	11 34	anbi12i	⊢ ( ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( 𝑚 𝐺 𝑛 ) : ( 𝑚 𝐻 𝑛 ) ⟶ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( 𝐺 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑢 𝐺 𝑣 ) ) ∧ ∀ 𝑚 ∈ 𝐵 ∀ 𝑛 ∈ 𝐵 ( ( 𝑚 𝐺 𝑛 ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ↦ ( 𝑏 ( 𝑚 𝐺 𝑛 ) 𝑎 ) ) ∧ ∀ 𝑝 ∈ ( ( 1^st ‘ 𝑚 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑛 ) ) ∀ 𝑞 ∈ ( ( 2^nd ‘ 𝑚 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ) )
36	10 35	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 ‘ 𝑛 ) ) ( 𝑝 ( 𝑚 𝐺 𝑛 ) 𝑞 ) ∈ ( ( 𝐹 ‘ 𝑚 ) ( 𝐶 Nat 𝐸 ) ( 𝐹 ‘ 𝑛 ) ) ) ) )

Metamath Proof Explorer

Theorem fucofulem2

Proof