fucoisfunc2lem1

Description: Lemma for fucoisfunc2lem2 . An equivalence that expands the transformation outputs of a composition-shaped hom-family into exact component functions, component typing, and naturality. The component values are arbitrary; no canonical value is imposed. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucoisfunc.w	$⊢ W = (D Func E) \times (C Func D)$
	fucoisfunc2lem1.o	$⊢ O = {\circ_{func} ↾}_{W}$
	fucoisfunc2lem1.b	$⊢ B = {Base}_{C}$
	fucoisfunc2lem1.r	$⊢ R = Hom (C)$
	fucoisfunc2lem1.s	$⊢ S = Hom (E)$
	fucoisfunc2lem1.v	$⊢ \underset{˙}{∙} = comp (E)$
Assertion	fucoisfunc2lem1	$⊢ (P = (u \in W, v \in W ⟼ u P v) \land \forall m \in W \forall n \in W (m P 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 P 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 P n) q \in (O (m) (C Nat E) O (n)))) \leftrightarrow (P = (u \in W, v \in W ⟼ u P v) \land \forall m \in W \forall n \in W (m P 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 P 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 P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x))))$

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	$⊢ W = (D Func E) \times (C Func D)$
2		fucoisfunc2lem1.o	$⊢ O = {\circ_{func} ↾}_{W}$
3		fucoisfunc2lem1.b	$⊢ B = {Base}_{C}$
4		fucoisfunc2lem1.r	$⊢ R = Hom (C)$
5		fucoisfunc2lem1.s	$⊢ S = Hom (E)$
6		fucoisfunc2lem1.v	$⊢ \underset{˙}{∙} = comp (E)$
7		eqid	$⊢ C Nat E = C Nat E$
8		rescofuf	$⊢ ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E$
9	1	reseq2i	$⊢ {\circ_{func} ↾}_{W} = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
10	2 9	eqtri	$⊢ O = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
11	10 1	feq12i	$⊢ O : W ⟶ C Func E \leftrightarrow ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E$
12	8 11	mpbir	$⊢ O : W ⟶ C Func E$
13	12	a1i	$⊢ ((⊤ \land m \in W) \land n \in W) \to O : W ⟶ C Func E$
14		simplr	$⊢ ((⊤ \land m \in W) \land n \in W) \to m \in W$
15	13 14	ffvelcdmd	$⊢ ((⊤ \land m \in W) \land n \in W) \to O (m) \in (C Func E)$
16		simpr	$⊢ ((⊤ \land m \in W) \land n \in W) \to n \in W$
17	13 16	ffvelcdmd	$⊢ ((⊤ \land m \in W) \land n \in W) \to O (n) \in (C Func E)$
18	7 3 4 5 6 15 17	isnat3	$⊢ ((⊤ \land m \in W) \land n \in W) \to (p (m P n) q \in (O (m) (C Nat E) O (n)) \leftrightarrow (p (m P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x)))$
19	18	2ralbidv	$⊢ ((⊤ \land m \in W) \land n \in W) \to (\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 P n) q \in (O (m) (C Nat E) O (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 P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x)))$
20	19	anbi2d	$⊢ ((⊤ \land m \in W) \land n \in W) \to ((m P 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 P 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 P n) q \in (O (m) (C Nat E) O (n))) \leftrightarrow (m P 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 P 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 P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x))))$
21	20	ralbidva	$⊢ (⊤ \land m \in W) \to (\forall n \in W (m P 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 P 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 P n) q \in (O (m) (C Nat E) O (n))) \leftrightarrow \forall n \in W (m P 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 P 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 P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x))))$
22	21	ralbidva	$⊢ ⊤ \to (\forall m \in W \forall n \in W (m P 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 P 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 P n) q \in (O (m) (C Nat E) O (n))) \leftrightarrow \forall m \in W \forall n \in W (m P 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 P 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 P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x))))$
23	22	anbi2d	$⊢ ⊤ \to ((P = (u \in W, v \in W ⟼ u P v) \land \forall m \in W \forall n \in W (m P 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 P 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 P n) q \in (O (m) (C Nat E) O (n)))) \leftrightarrow (P = (u \in W, v \in W ⟼ u P v) \land \forall m \in W \forall n \in W (m P 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 P 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 P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x)))))$
24	23	mptru	$⊢ (P = (u \in W, v \in W ⟼ u P v) \land \forall m \in W \forall n \in W (m P 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 P 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 P n) q \in (O (m) (C Nat E) O (n)))) \leftrightarrow (P = (u \in W, v \in W ⟼ u P v) \land \forall m \in W \forall n \in W (m P 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 P 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 P n) q = (x \in B ⟼ (p (m P n) q) (x)) \land \forall x \in B (p (m P n) q) (x) \in (1^{st} (O (m)) (x) S 1^{st} (O (n)) (x)) \land \forall x \in B \forall y \in B \forall h \in (x R y) (p (m P n) q) (y) (⟨1^{st} (O (m)) (x), 1^{st} (O (m)) (y)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (x 2^{nd} (O (m)) y) (h) = (x 2^{nd} (O (n)) y) (h) (⟨1^{st} (O (m)) (x), 1^{st} (O (n)) (x)⟩ \underset{˙}{∙} 1^{st} (O (n)) (y)) (p (m P n) q) (x))))$

Metamath Proof Explorer

Theorem fucoisfunc2lem1

Proof