fucidcl

Description: The identity natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucidcl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucidcl.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fucidcl.x	⊢ 1 = ( Id ‘ 𝐷 )
	fucidcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	fucidcl	⊢ ( 𝜑 → ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 𝑁 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fucidcl.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fucidcl.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		fucidcl.x	⊢ 1 = ( Id ‘ 𝐷 )
4		fucidcl.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
6	4 5	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
7	6	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
8		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
9	8 3	cidfn	⊢ ( 𝐷 ∈ Cat → 1 Fn ( Base ‘ 𝐷 ) )
10	7 9	syl	⊢ ( 𝜑 → 1 Fn ( Base ‘ 𝐷 ) )
11		dffn2	⊢ ( 1 Fn ( Base ‘ 𝐷 ) ↔ 1 : ( Base ‘ 𝐷 ) ⟶ V )
12	10 11	sylib	⊢ ( 𝜑 → 1 : ( Base ‘ 𝐷 ) ⟶ V )
13		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
14		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
15		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
16	14 4 15	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
17	13 8 16	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
18		fcompt	⊢ ( ( 1 : ( Base ‘ 𝐷 ) ⟶ V ∧ ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ) → ( 1 ∘ ( 1^st ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
19	12 17 18	syl2anc	⊢ ( 𝜑 → ( 1 ∘ ( 1^st ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
20		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
21	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
22	17	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
23	8 20 3 21 22	catidcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
24	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
25		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
26		mptelixpg	⊢ ( ( Base ‘ 𝐶 ) ∈ V → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
27	25 26	ax-mp	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
28	24 27	sylibr	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
29	19 28	eqeltrd	⊢ ( 𝜑 → ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
30	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝐷 ∈ Cat )
31		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
32	31 22	syldan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
33		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
34	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
35		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
36	34 35	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
37		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
38	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
39	13 37 20 38 31 35	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
40		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
41	39 40	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
42	8 20 3 30 32 33 36 41	catlid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) )
43	8 20 3 30 32 33 36 41	catrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) )
44	42 43	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
45		fvco3	⊢ ( ( ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑦 ) = ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
46	34 35 45	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑦 ) = ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
47	46	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
48		fvco3	⊢ ( ( ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) = ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
49	34 31 48	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) = ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
50	49	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( 1 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
51	44 47 50	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) ) → ( ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) )
52	51	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) )
53	2 13 37 20 33 4 4	isnat2	⊢ ( 𝜑 → ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 𝑁 𝐹 ) ↔ ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ∈ X 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ( ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) ) )
54	29 52 53	mpbir2and	⊢ ( 𝜑 → ( 1 ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 𝑁 𝐹 ) )

Metamath Proof Explorer

Theorem fucidcl

Proof