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	3	xpcfucbas	$⊢ (D Func E) \times (C Func D) = {Base}_{((D FuncCat E) \times_{c} (C FuncCat D))}$
5	1 4	eqtri	$⊢ B = {Base}_{((D FuncCat E) \times_{c} (C FuncCat D))}$
6	5	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))$
7		fnov	$⊢ G Fn (B \times B) \leftrightarrow G = (u \in B, v \in B ⟼ u G v)$
8		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)))$
9		simpl	$⊢ (m \in B \land n \in B) \to m \in B$
10		simpr	$⊢ (m \in B \land n \in B) \to n \in B$
11	3 5 2 9 10	xpcfuchom	$⊢ (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))$
12	11	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))))$
13		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)$
14	12 13	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))$
15	11	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)))$
16		fveq2	$⊢ r = ⟨p, q⟩ \to (m G n) (r) = (m G n) (⟨p, q⟩)$
17		df-ov	$⊢ p (m G n) q = (m G n) (⟨p, q⟩)$
18	16 17	eqtr4di	$⊢ r = ⟨p, q⟩ \to (m G n) (r) = p (m G n) q$
19	18	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)))$
20	19	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))$
21	15 20	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)))$
22	14 21	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))))$
23	8 22	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))))$
24	23	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))))$
25	24	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))))$
26	25	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)))$
27	7 26	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))))$
28	6 27	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