nat1st2nd

Description: Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017)

Step	Hyp	Ref	Expression
1		natrcl.1	$⊢ N = C Nat D$
2		nat1st2nd.2	$⊢ φ \to A \in (F N G)$
3		relfunc	$⊢ Rel (C Func D)$
4	1	natrcl	$⊢ A \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$
5	2 4	syl	$⊢ φ \to (F \in (C Func D) \land G \in (C Func D))$
6	5	simpld	$⊢ φ \to F \in (C Func D)$
7		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
8	3 6 7	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
9	5	simprd	$⊢ φ \to G \in (C Func D)$
10		1st2nd	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
11	3 9 10	sylancr	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
12	8 11	oveq12d	$⊢ φ \to F N G = ⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩$
13	2 12	eleqtrd	$⊢ φ \to A \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$

Metamath Proof Explorer