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