fuco22nat

Description: The composed natural transformation is a natural transformation. (Contributed by Zhi Wang, 2-Oct-2025)

	Ref	Expression
Hypotheses	fuco22nat.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fuco22nat.a	$⊢ φ \to A \in (F (C Nat D) M)$
	fuco22nat.b	$⊢ φ \to B \in (K (D Nat E) R)$
	fuco22nat.u	$⊢ φ \to U = ⟨K, F⟩$
	fuco22nat.v	$⊢ φ \to V = ⟨R, M⟩$
Assertion	fuco22nat	$⊢ φ \to B (U P V) A \in (O (U) (C Nat E) O (V))$

Proof

Step	Hyp	Ref	Expression
1		fuco22nat.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
2		fuco22nat.a	$⊢ φ \to A \in (F (C Nat D) M)$
3		fuco22nat.b	$⊢ φ \to B \in (K (D Nat E) R)$
4		fuco22nat.u	$⊢ φ \to U = ⟨K, F⟩$
5		fuco22nat.v	$⊢ φ \to V = ⟨R, M⟩$
6		eqid	$⊢ C Nat D = C Nat D$
7	6 2	nat1st2nd	$⊢ φ \to A \in (⟨1^{st} (F), 2^{nd} (F)⟩ (C Nat D) ⟨1^{st} (M), 2^{nd} (M)⟩)$
8		eqid	$⊢ D Nat E = D Nat E$
9	8 3	nat1st2nd	$⊢ φ \to B \in (⟨1^{st} (K), 2^{nd} (K)⟩ (D Nat E) ⟨1^{st} (R), 2^{nd} (R)⟩)$
10		relfunc	$⊢ Rel (D Func E)$
11	8	natrcl	$⊢ B \in (K (D Nat E) R) \to (K \in (D Func E) \land R \in (D Func E))$
12	3 11	syl	$⊢ φ \to (K \in (D Func E) \land R \in (D Func E))$
13	12	simpld	$⊢ φ \to K \in (D Func E)$
14		1st2nd	$⊢ (Rel (D Func E) \land K \in (D Func E)) \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
15	10 13 14	sylancr	$⊢ φ \to K = ⟨1^{st} (K), 2^{nd} (K)⟩$
16		relfunc	$⊢ Rel (C Func D)$
17	6	natrcl	$⊢ A \in (F (C Nat D) M) \to (F \in (C Func D) \land M \in (C Func D))$
18	2 17	syl	$⊢ φ \to (F \in (C Func D) \land M \in (C Func D))$
19	18	simpld	$⊢ φ \to F \in (C Func D)$
20		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
21	16 19 20	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
22	15 21	opeq12d	$⊢ φ \to ⟨K, F⟩ = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (F), 2^{nd} (F)⟩⟩$
23	4 22	eqtrd	$⊢ φ \to U = ⟨⟨1^{st} (K), 2^{nd} (K)⟩, ⟨1^{st} (F), 2^{nd} (F)⟩⟩$
24	12	simprd	$⊢ φ \to R \in (D Func E)$
25		1st2nd	$⊢ (Rel (D Func E) \land R \in (D Func E)) \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
26	10 24 25	sylancr	$⊢ φ \to R = ⟨1^{st} (R), 2^{nd} (R)⟩$
27	18	simprd	$⊢ φ \to M \in (C Func D)$
28		1st2nd	$⊢ (Rel (C Func D) \land M \in (C Func D)) \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
29	16 27 28	sylancr	$⊢ φ \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
30	26 29	opeq12d	$⊢ φ \to ⟨R, M⟩ = ⟨⟨1^{st} (R), 2^{nd} (R)⟩, ⟨1^{st} (M), 2^{nd} (M)⟩⟩$
31	5 30	eqtrd	$⊢ φ \to V = ⟨⟨1^{st} (R), 2^{nd} (R)⟩, ⟨1^{st} (M), 2^{nd} (M)⟩⟩$
32	1 7 9 23 31	fuco22natlem	$⊢ φ \to B (U P V) A \in (O (U) (C Nat E) O (V))$

Metamath Proof Explorer

Theorem fuco22nat

Proof