isnat

Description: Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

	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)$
	isnat.f	$⊢ φ \to F (C Func D) G$
	isnat.g	$⊢ φ \to K (C Func D) L$
Assertion	isnat	$⊢ φ \to (A \in (⟨F, G⟩ N ⟨K, L⟩) \leftrightarrow (A \in \underset{x \in B}{⨉} (F (x) J K (x)) \land \forall x \in B \forall y \in B \forall h \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (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		isnat.f	$⊢ φ \to F (C Func D) G$
7		isnat.g	$⊢ φ \to K (C Func D) L$
8	1 2 3 4 5	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)\})$
9	8	a1i	$⊢ φ \to 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)\})$
10		fvexd	$⊢ (φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \to 1^{st} (f) \in V$
11		simprl	$⊢ (φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \to f = ⟨F, G⟩$
12	11	fveq2d	$⊢ (φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \to 1^{st} (f) = 1^{st} (⟨F, G⟩)$
13		relfunc	$⊢ Rel (C Func D)$
14		brrelex12	$⊢ (Rel (C Func D) \land F (C Func D) G) \to (F \in V \land G \in V)$
15	13 6 14	sylancr	$⊢ φ \to (F \in V \land G \in V)$
16		op1stg	$⊢ (F \in V \land G \in V) \to 1^{st} (⟨F, G⟩) = F$
17	15 16	syl	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
18	17	adantr	$⊢ (φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \to 1^{st} (⟨F, G⟩) = F$
19	12 18	eqtrd	$⊢ (φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \to 1^{st} (f) = F$
20		fvexd	$⊢ ((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \to 1^{st} (g) \in V$
21		simplrr	$⊢ ((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \to g = ⟨K, L⟩$
22	21	fveq2d	$⊢ ((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \to 1^{st} (g) = 1^{st} (⟨K, L⟩)$
23		brrelex12	$⊢ (Rel (C Func D) \land K (C Func D) L) \to (K \in V \land L \in V)$
24	13 7 23	sylancr	$⊢ φ \to (K \in V \land L \in V)$
25		op1stg	$⊢ (K \in V \land L \in V) \to 1^{st} (⟨K, L⟩) = K$
26	24 25	syl	$⊢ φ \to 1^{st} (⟨K, L⟩) = K$
27	26	ad2antrr	$⊢ ((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \to 1^{st} (⟨K, L⟩) = K$
28	22 27	eqtrd	$⊢ ((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \to 1^{st} (g) = K$
29		simplr	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to r = F$
30	29	fveq1d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to r (x) = F (x)$
31		simpr	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to s = K$
32	31	fveq1d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to s (x) = K (x)$
33	30 32	oveq12d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to r (x) J s (x) = F (x) J K (x)$
34	33	ixpeq2dv	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to \underset{x \in B}{⨉} (r (x) J s (x)) = \underset{x \in B}{⨉} (F (x) J K (x))$
35	29	fveq1d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to r (y) = F (y)$
36	30 35	opeq12d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to ⟨r (x), r (y)⟩ = ⟨F (x), F (y)⟩$
37	31	fveq1d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to s (y) = K (y)$
38	36 37	oveq12d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to ⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y) = ⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)$
39		eqidd	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to a (y) = a (y)$
40	11	ad2antrr	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to f = ⟨F, G⟩$
41	40	fveq2d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to 2^{nd} (f) = 2^{nd} (⟨F, G⟩)$
42		op2ndg	$⊢ (F \in V \land G \in V) \to 2^{nd} (⟨F, G⟩) = G$
43	15 42	syl	$⊢ φ \to 2^{nd} (⟨F, G⟩) = G$
44	43	ad3antrrr	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to 2^{nd} (⟨F, G⟩) = G$
45	41 44	eqtrd	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to 2^{nd} (f) = G$
46	45	oveqd	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to x 2^{nd} (f) y = x G y$
47	46	fveq1d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to (x 2^{nd} (f) y) (h) = (x G y) (h)$
48	38 39 47	oveq123d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to a (y) (⟨r (x), r (y)⟩ \underset{˙}{\cdot} s (y)) (x 2^{nd} (f) y) (h) = a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h)$
49	30 32	opeq12d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to ⟨r (x), s (x)⟩ = ⟨F (x), K (x)⟩$
50	49 37	oveq12d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to ⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y) = ⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)$
51	21	adantr	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to g = ⟨K, L⟩$
52	51	fveq2d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to 2^{nd} (g) = 2^{nd} (⟨K, L⟩)$
53		op2ndg	$⊢ (K \in V \land L \in V) \to 2^{nd} (⟨K, L⟩) = L$
54	24 53	syl	$⊢ φ \to 2^{nd} (⟨K, L⟩) = L$
55	54	ad3antrrr	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to 2^{nd} (⟨K, L⟩) = L$
56	52 55	eqtrd	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to 2^{nd} (g) = L$
57	56	oveqd	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to x 2^{nd} (g) y = x L y$
58	57	fveq1d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to (x 2^{nd} (g) y) (h) = (x L y) (h)$
59		eqidd	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to a (x) = a (x)$
60	50 58 59	oveq123d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ \underset{˙}{\cdot} s (y)) a (x) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)$
61	48 60	eqeq12d	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to (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) \leftrightarrow a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x))$
62	61	ralbidv	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to (\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) \leftrightarrow \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x))$
63	62	2ralbidv	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to (\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) \leftrightarrow \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x))$
64	34 63	rabeqbidv	$⊢ (((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \land s = K) \to \{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)\} = \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\}$
65	20 28 64	csbied2	$⊢ ((φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \land r = F) \to ⦋ 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)\} = \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\}$
66	10 19 65	csbied2	$⊢ (φ \land (f = ⟨F, G⟩ \land g = ⟨K, L⟩)) \to ⦋ 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)\} = \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\}$
67		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
68	6 67	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
69		df-br	$⊢ K (C Func D) L \leftrightarrow ⟨K, L⟩ \in (C Func D)$
70	7 69	sylib	$⊢ φ \to ⟨K, L⟩ \in (C Func D)$
71		ovex	$⊢ F (x) J K (x) \in V$
72	71	rgenw	$⊢ \forall x \in B F (x) J K (x) \in V$
73		ixpexg	$⊢ \forall x \in B F (x) J K (x) \in V \to \underset{x \in B}{⨉} (F (x) J K (x)) \in V$
74	72 73	ax-mp	$⊢ \underset{x \in B}{⨉} (F (x) J K (x)) \in V$
75	74	rabex	$⊢ \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\} \in V$
76	75	a1i	$⊢ φ \to \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\} \in V$
77	9 66 68 70 76	ovmpod	$⊢ φ \to ⟨F, G⟩ N ⟨K, L⟩ = \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\}$
78	77	eleq2d	$⊢ φ \to (A \in (⟨F, G⟩ N ⟨K, L⟩) \leftrightarrow A \in \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\})$
79		fveq1	$⊢ a = A \to a (y) = A (y)$
80	79	oveq1d	$⊢ a = A \to a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h)$
81		fveq1	$⊢ a = A \to a (x) = A (x)$
82	81	oveq2d	$⊢ a = A \to (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x)$
83	80 82	eqeq12d	$⊢ a = A \to (a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x) \leftrightarrow A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x))$
84	83	ralbidv	$⊢ a = A \to (\forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x) \leftrightarrow \forall h \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x))$
85	84	2ralbidv	$⊢ a = A \to (\forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x) \leftrightarrow \forall x \in B \forall y \in B \forall h \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x))$
86	85	elrab	$⊢ A \in \{a \in \underset{x \in B}{⨉} (F (x) J K (x)) \| \forall x \in B \forall y \in B \forall h \in (x H y) a (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) a (x)\} \leftrightarrow (A \in \underset{x \in B}{⨉} (F (x) J K (x)) \land \forall x \in B \forall y \in B \forall h \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x))$
87	78 86	bitrdi	$⊢ φ \to (A \in (⟨F, G⟩ N ⟨K, L⟩) \leftrightarrow (A \in \underset{x \in B}{⨉} (F (x) J K (x)) \land \forall x \in B \forall y \in B \forall h \in (x H y) A (y) (⟨F (x), F (y)⟩ \underset{˙}{\cdot} K (y)) (x G y) (h) = (x L y) (h) (⟨F (x), K (x)⟩ \underset{˙}{\cdot} K (y)) A (x)))$

Metamath Proof Explorer

Theorem isnat

Proof