Theorem fuco22nat

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

	Ref	Expression
Hypotheses	fuco22nat.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fuco22nat.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝑀 ) )
	fuco22nat.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑅 ) )
	fuco22nat.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐾 , 𝐹 ⟩ )
	fuco22nat.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝑅 , 𝑀 ⟩ )
Assertion	fuco22nat	⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ∈ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco22nat.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fuco22nat.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝑀 ) )
3		fuco22nat.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑅 ) )
4		fuco22nat.u	⊢ ( 𝜑 → 𝑈 = ⟨ 𝐾 , 𝐹 ⟩ )
5		fuco22nat.v	⊢ ( 𝜑 → 𝑉 = ⟨ 𝑅 , 𝑀 ⟩ )
6		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
7	6 2	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ ) )
8		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
9	8 3	nat1st2nd	⊢ ( 𝜑 → 𝐵 ∈ ( ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ ) )
10		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
11	8	natrcl	⊢ ( 𝐵 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑅 ) → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑅 ∈ ( 𝐷 Func 𝐸 ) ) )
12	3 11	syl	⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑅 ∈ ( 𝐷 Func 𝐸 ) ) )
13	12	simpld	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
14		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐾 = ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ )
15	10 13 14	sylancr	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ )
16		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
17	6	natrcl	⊢ ( 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝑀 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑀 ∈ ( 𝐶 Func 𝐷 ) ) )
18	2 17	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑀 ∈ ( 𝐶 Func 𝐷 ) ) )
19	18	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
20		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
21	16 19 20	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
22	15 21	opeq12d	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐹 ⟩ = ⟨ ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ , ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ⟩ )
23	4 22	eqtrd	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ , ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ⟩ )
24	12	simprd	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐷 Func 𝐸 ) )
25		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝑅 ∈ ( 𝐷 Func 𝐸 ) ) → 𝑅 = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ )
26	10 24 25	sylancr	⊢ ( 𝜑 → 𝑅 = ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ )
27	18	simprd	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐶 Func 𝐷 ) )
28		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑀 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑀 = ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ )
29	16 27 28	sylancr	⊢ ( 𝜑 → 𝑀 = ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ )
30	26 29	opeq12d	⊢ ( 𝜑 → ⟨ 𝑅 , 𝑀 ⟩ = ⟨ ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ , ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ ⟩ )
31	5 30	eqtrd	⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ ( 1st ‘ 𝑅 ) , ( 2nd ‘ 𝑅 ) ⟩ , ⟨ ( 1st ‘ 𝑀 ) , ( 2nd ‘ 𝑀 ) ⟩ ⟩ )
32	1 7 9 23 31	fuco22natlem	⊢ ( 𝜑 → ( 𝐵 ( 𝑈 𝑃 𝑉 ) 𝐴 ) ∈ ( ( 𝑂 ‘ 𝑈 ) ( 𝐶 Nat 𝐸 ) ( 𝑂 ‘ 𝑉 ) ) )