isnat2

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)$
	isnat2.f	$⊢ φ \to F \in (C Func D)$
	isnat2.g	$⊢ φ \to G \in (C Func D)$
Assertion	isnat2	$⊢ φ \to (A \in (F N G) \leftrightarrow (A \in \underset{x \in B}{⨉} (1^{st} (F) (x) J 1^{st} (G) (x)) \land \forall x \in B \forall y \in B \forall h \in (x H y) A (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ \underset{˙}{\cdot} 1^{st} (G) (y)) (x 2^{nd} (F) y) (h) = (x 2^{nd} (G) y) (h) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (G) (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		isnat2.f	$⊢ φ \to F \in (C Func D)$
7		isnat2.g	$⊢ φ \to G \in (C Func D)$
8		relfunc	$⊢ Rel (C Func D)$
9		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
10	8 6 9	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
11		1st2nd	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
12	8 7 11	sylancr	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
13	10 12	oveq12d	$⊢ φ \to F N G = ⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩$
14	13	eleq2d	$⊢ φ \to (A \in (F N G) \leftrightarrow A \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩))$
15		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
16	8 6 15	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
17		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
18	8 7 17	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
19	1 2 3 4 5 16 18	isnat	$⊢ φ \to (A \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩) \leftrightarrow (A \in \underset{x \in B}{⨉} (1^{st} (F) (x) J 1^{st} (G) (x)) \land \forall x \in B \forall y \in B \forall h \in (x H y) A (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ \underset{˙}{\cdot} 1^{st} (G) (y)) (x 2^{nd} (F) y) (h) = (x 2^{nd} (G) y) (h) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (G) (y)) A (x)))$
20	14 19	bitrd	$⊢ φ \to (A \in (F N G) \leftrightarrow (A \in \underset{x \in B}{⨉} (1^{st} (F) (x) J 1^{st} (G) (x)) \land \forall x \in B \forall y \in B \forall h \in (x H y) A (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ \underset{˙}{\cdot} 1^{st} (G) (y)) (x 2^{nd} (F) y) (h) = (x 2^{nd} (G) y) (h) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \underset{˙}{\cdot} 1^{st} (G) (y)) A (x)))$

Metamath Proof Explorer

Theorem isnat2

Proof