natfval

Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

	Ref	Expression
Hypotheses	natfval.1	$⊢ N = C Nat D$
	natfval.b	$⊢ B = {Base}_{C}$
	natfval.h	$⊢ H = Hom (C)$
	natfval.j	$⊢ J = Hom (D)$
	natfval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
Assertion	natfval	$⊢ N = (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\})$

Proof

Step	Hyp	Ref	Expression
1		natfval.1	$⊢ N = C Nat D$
2		natfval.b	$⊢ B = {Base}_{C}$
3		natfval.h	$⊢ H = Hom (C)$
4		natfval.j	$⊢ J = Hom (D)$
5		natfval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
6		oveq12	$⊢ (t = C \land u = D) \to t Func u = C Func D$
7		simpl	$⊢ (t = C \land u = D) \to t = C$
8	7	fveq2d	$⊢ (t = C \land u = D) \to {Base}_{t} = {Base}_{C}$
9	8 2	eqtr4di	$⊢ (t = C \land u = D) \to {Base}_{t} = B$
10	9	ixpeq1d	$⊢ (t = C \land u = D) \to \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) = \underset{x \in B}{⨉} (r (x) Hom (u) s (x))$
11		simpr	$⊢ (t = C \land u = D) \to u = D$
12	11	fveq2d	$⊢ (t = C \land u = D) \to Hom (u) = Hom (D)$
13	12 4	eqtr4di	$⊢ (t = C \land u = D) \to Hom (u) = J$
14	13	oveqd	$⊢ (t = C \land u = D) \to r (x) Hom (u) s (x) = r (x) J s (x)$
15	14	ixpeq2dv	$⊢ (t = C \land u = D) \to \underset{x \in B}{⨉} (r (x) Hom (u) s (x)) = \underset{x \in B}{⨉} (r (x) J s (x))$
16	10 15	eqtrd	$⊢ (t = C \land u = D) \to \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) = \underset{x \in B}{⨉} (r (x) J s (x))$
17	7	fveq2d	$⊢ (t = C \land u = D) \to Hom (t) = Hom (C)$
18	17 3	eqtr4di	$⊢ (t = C \land u = D) \to Hom (t) = H$
19	18	oveqd	$⊢ (t = C \land u = D) \to x Hom (t) y = x H y$
20	11	fveq2d	$⊢ (t = C \land u = D) \to comp (u) = comp (D)$
21	20 5	eqtr4di	$⊢ (t = C \land u = D) \to comp (u) = \underset{˙}{\cdot}$
22	21	oveqd	$⊢ (t = C \land u = D) \to ⟨r (x), r (y)⟩ comp (u) s (y) = ⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)$
23	22	oveqd	$⊢ (t = C \land u = D) \to a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h)$
24	21	oveqd	$⊢ (t = C \land u = D) \to ⟨r (x), s (x)⟩ comp (u) s (y) = ⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)$
25	24	oveqd	$⊢ (t = C \land u = D) \to (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)$
26	23 25	eqeq12d	$⊢ (t = C \land u = D) \to (a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x) \leftrightarrow a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x))$
27	19 26	raleqbidv	$⊢ (t = C \land u = D) \to (\forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x) \leftrightarrow \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x))$
28	9 27	raleqbidv	$⊢ (t = C \land u = D) \to (\forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x) \leftrightarrow \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x))$
29	9 28	raleqbidv	$⊢ (t = C \land u = D) \to (\forall x \in {Base}_{t} \forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x) \leftrightarrow \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x))$
30	16 29	rabeqbidv	$⊢ (t = C \land u = D) \to \{a \in \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) \| \forall x \in {Base}_{t} \forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x)\} = \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\}$
31	30	csbeq2dv	$⊢ (t = C \land u = D) \to ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) \| \forall x \in {Base}_{t} \forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x)\} = ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\}$
32	31	csbeq2dv	$⊢ (t = C \land u = D) \to ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) \| \forall x \in {Base}_{t} \forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x)\} = ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\}$
33	6 6 32	mpoeq123dv	$⊢ (t = C \land u = D) \to (f \in (t Func u), g \in (t Func u) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) \| \forall x \in {Base}_{t} \forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x)\}) = (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\})$
34		df-nat	$⊢ Nat = (t \in Cat, u \in Cat ⟼ (f \in (t Func u), g \in (t Func u) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{t}}{⨉} (r (x) Hom (u) s (x)) \| \forall x \in {Base}_{t} \forall y \in {Base}_{t} \forall h \in (x Hom (t) y) a (y) (⟨r (x), r (y)⟩ comp (u) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (u) s (y)) a (x)\}))$
35		ovex	$⊢ C Func D \in V$
36	35 35	mpoex	$⊢ (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\}) \in V$
37	33 34 36	ovmpoa	$⊢ (C \in Cat \land D \in Cat) \to C Nat D = (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\})$
38	34	mpondm0	$⊢ \neg (C \in Cat \land D \in Cat) \to C Nat D = \emptyset$
39		funcrcl	$⊢ f \in (C Func D) \to (C \in Cat \land D \in Cat)$
40	39	con3i	$⊢ \neg (C \in Cat \land D \in Cat) \to \neg f \in (C Func D)$
41	40	eq0rdv	$⊢ \neg (C \in Cat \land D \in Cat) \to C Func D = \emptyset$
42	41	olcd	$⊢ \neg (C \in Cat \land D \in Cat) \to (C Func D = \emptyset \lor C Func D = \emptyset)$
43		0mpo0	$⊢ (C Func D = \emptyset \lor C Func D = \emptyset) \to (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\}) = \emptyset$
44	42 43	syl	$⊢ \neg (C \in Cat \land D \in Cat) \to (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\}) = \emptyset$
45	38 44	eqtr4d	$⊢ \neg (C \in Cat \land D \in Cat) \to C Nat D = (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\})$
46	37 45	pm2.61i	$⊢ C Nat D = (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\})$
47	1 46	eqtri	$⊢ N = (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in B}{⨉} (r (x) J s (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x)\})$

Metamath Proof Explorer

Theorem natfval

Proof