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	$⊢ B = (D Func E) \times (C Func D)$
	fucofulem2.h	$⊢ H = Hom ((D FuncCat E) \times_{c} (C FuncCat D))$
Assertion	fucofulem2	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) (C Nat E) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G = (u \in B, v \in B ⟼ u G v) \land \forall m \in B \forall n \in B (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))))$

Proof

Step	Hyp	Ref	Expression
1		fucofulem2.b	$⊢ B = (D Func E) \times (C Func D)$
2		fucofulem2.h	$⊢ H = Hom ((D FuncCat E) \times_{c} (C FuncCat D))$
3		eqid	$⊢ (D FuncCat E) \times_{c} (C FuncCat D) = (D FuncCat E) \times_{c} (C FuncCat D)$
4		eqid	$⊢ D FuncCat E = D FuncCat E$
5	4	fucbas	$⊢ D Func E = {Base}_{(D FuncCat E)}$
6		eqid	$⊢ C FuncCat D = C FuncCat D$
7	6	fucbas	$⊢ C Func D = {Base}_{(C FuncCat D)}$
8	3 5 7	xpcbas	$⊢ (D Func E) \times (C Func D) = {Base}_{((D FuncCat E) \times_{c} (C FuncCat D))}$
9	1 8	eqtri	$⊢ B = {Base}_{((D FuncCat E) \times_{c} (C FuncCat D))}$
10	9	funcf2lem2	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) (C Nat E) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G Fn (B \times B) \land \forall m \in B \forall n \in B (m G n) : m H n ⟶ F (m) (C Nat E) F (n))$
11		fnov	$⊢ G Fn (B \times B) \leftrightarrow G = (u \in B, v \in B ⟼ u G v)$
12		ffnfv	$⊢ (m G n) : m H n ⟶ F (m) (C Nat E) F (n) \leftrightarrow ((m G n) Fn (m H n) \land \forall r \in (m H n) (m G n) (r) \in (F (m) (C Nat E) F (n)))$
13		eqid	$⊢ D Nat E = D Nat E$
14	4 13	fuchom	$⊢ D Nat E = Hom (D FuncCat E)$
15		eqid	$⊢ C Nat D = C Nat D$
16	6 15	fuchom	$⊢ C Nat D = Hom (C FuncCat D)$
17		simpl	$⊢ (m \in B \land n \in B) \to m \in B$
18		simpr	$⊢ (m \in B \land n \in B) \to n \in B$
19	3 9 14 16 2 17 18	xpchom	$⊢ (m \in B \land n \in B) \to m H n = (1^{st} (m) (D Nat E) 1^{st} (n)) \times (2^{nd} (m) (C Nat D) 2^{nd} (n))$
20	19	fneq2d	$⊢ (m \in B \land n \in B) \to ((m G n) Fn (m H n) \leftrightarrow (m G n) Fn ((1^{st} (m) (D Nat E) 1^{st} (n)) \times (2^{nd} (m) (C Nat D) 2^{nd} (n))))$
21		fnov	$⊢ (m G n) Fn ((1^{st} (m) (D Nat E) 1^{st} (n)) \times (2^{nd} (m) (C Nat D) 2^{nd} (n))) \leftrightarrow m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a)$
22	20 21	bitrdi	$⊢ (m \in B \land n \in B) \to ((m G n) Fn (m H n) \leftrightarrow m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a))$
23	19	raleqdv	$⊢ (m \in B \land n \in B) \to (\forall r \in (m H n) (m G n) (r) \in (F (m) (C Nat E) F (n)) \leftrightarrow \forall r \in ((1^{st} (m) (D Nat E) 1^{st} (n)) \times (2^{nd} (m) (C Nat D) 2^{nd} (n))) (m G n) (r) \in (F (m) (C Nat E) F (n)))$
24		fveq2	$⊢ r = ⟨p, q⟩ \to (m G n) (r) = (m G n) (⟨p, q⟩)$
25		df-ov	$⊢ p (m G n) q = (m G n) (⟨p, q⟩)$
26	24 25	eqtr4di	$⊢ r = ⟨p, q⟩ \to (m G n) (r) = p (m G n) q$
27	26	eleq1d	$⊢ r = ⟨p, q⟩ \to ((m G n) (r) \in (F (m) (C Nat E) F (n)) \leftrightarrow p (m G n) q \in (F (m) (C Nat E) F (n)))$
28	27	ralxp	$⊢ \forall r \in ((1^{st} (m) (D Nat E) 1^{st} (n)) \times (2^{nd} (m) (C Nat D) 2^{nd} (n))) (m G n) (r) \in (F (m) (C Nat E) F (n)) \leftrightarrow \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))$
29	23 28	bitrdi	$⊢ (m \in B \land n \in B) \to (\forall r \in (m H n) (m G n) (r) \in (F (m) (C Nat E) F (n)) \leftrightarrow \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n)))$
30	22 29	anbi12d	$⊢ (m \in B \land n \in B) \to (((m G n) Fn (m H n) \land \forall r \in (m H n) (m G n) (r) \in (F (m) (C Nat E) F (n))) \leftrightarrow (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))))$
31	12 30	bitrid	$⊢ (m \in B \land n \in B) \to ((m G n) : m H n ⟶ F (m) (C Nat E) F (n) \leftrightarrow (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))))$
32	31	adantl	$⊢ (⊤ \land (m \in B \land n \in B)) \to ((m G n) : m H n ⟶ F (m) (C Nat E) F (n) \leftrightarrow (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))))$
33	32	2ralbidva	$⊢ ⊤ \to (\forall m \in B \forall n \in B (m G n) : m H n ⟶ F (m) (C Nat E) F (n) \leftrightarrow \forall m \in B \forall n \in B (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))))$
34	33	mptru	$⊢ \forall m \in B \forall n \in B (m G n) : m H n ⟶ F (m) (C Nat E) F (n) \leftrightarrow \forall m \in B \forall n \in B (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n)))$
35	11 34	anbi12i	$⊢ (G Fn (B \times B) \land \forall m \in B \forall n \in B (m G n) : m H n ⟶ F (m) (C Nat E) F (n)) \leftrightarrow (G = (u \in B, v \in B ⟼ u G v) \land \forall m \in B \forall n \in B (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))))$
36	10 35	bitri	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) (C Nat E) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G = (u \in B, v \in B ⟼ u G v) \land \forall m \in B \forall n \in B (m G n = (b \in (1^{st} (m) (D Nat E) 1^{st} (n)), a \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) ⟼ b (m G n) a) \land \forall p \in (1^{st} (m) (D Nat E) 1^{st} (n)) \forall q \in (2^{nd} (m) (C Nat D) 2^{nd} (n)) p (m G n) q \in (F (m) (C Nat E) F (n))))$

Metamath Proof Explorer

Theorem fucofulem2

Proof