invfuc

Description: If V ( x ) is an inverse to U ( x ) for each x , and U is a natural transformation, then V is also a natural transformation, and they are inverse in the functor category. (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	fuciso.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fuciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	fuciso.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fuciso.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	fuciso.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
	fucinv.i	⊢ 𝐼 = ( Inv ‘ 𝑄 )
	fucinv.j	⊢ 𝐽 = ( Inv ‘ 𝐷 )
	invfuc.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) )
	invfuc.v	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑋 )
Assertion	invfuc	⊢ ( 𝜑 → 𝑈 ( 𝐹 𝐼 𝐺 ) ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fuciso.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fuciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		fuciso.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4		fuciso.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		fuciso.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
6		fucinv.i	⊢ 𝐼 = ( Inv ‘ 𝑄 )
7		fucinv.j	⊢ 𝐽 = ( Inv ‘ 𝐷 )
8		invfuc.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) )
9		invfuc.v	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑋 )
10		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
11		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
12	4 11	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
13	12	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ Cat )
15		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
16		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
17	15 4 16	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
18	2 10 17	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
19	18	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
20		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
21	15 5 20	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
22	2 10 21	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
23	22	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
24		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
25	10 7 14 19 23 24	invss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ⊆ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
26	25	ssbrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) 𝑋 → ( 𝑈 ‘ 𝑥 ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) 𝑋 ) )
27	9 26	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑥 ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) 𝑋 )
28		brxp	⊢ ( ( 𝑈 ‘ 𝑥 ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) 𝑋 ↔ ( ( 𝑈 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ∧ 𝑋 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
29	28	simprbi	⊢ ( ( 𝑈 ‘ 𝑥 ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) × ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) 𝑋 → 𝑋 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
30	27 29	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
31	30	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝑋 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
32	2	fvexi	⊢ 𝐵 ∈ V
33		mptelixpg	⊢ ( 𝐵 ∈ V → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 𝑋 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
34	32 33	ax-mp	⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐵 𝑋 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
35	31 34	sylibr	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
36		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) )
37		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) )
38	36 37	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
39	38	cbvixpv	⊢ X 𝑥 ∈ 𝐵 ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = X 𝑦 ∈ 𝐵 ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) )
40	35 39	eleqtrdi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ X 𝑦 ∈ 𝐵 ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
41		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
42		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
43		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) = ( 𝑥 ∈ 𝐵 ↦ 𝑋 )
44	43	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
45	42 30 44	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
46	9 45	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) )
47	46	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) )
48	47	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) )
49		nfcv	⊢ Ⅎ 𝑥 ( 𝑈 ‘ 𝑧 )
50		nfcv	⊢ Ⅎ 𝑥 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) )
51		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 )
52	49 50 51	nfbr	⊢ Ⅎ 𝑥 ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 )
53		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑈 ‘ 𝑥 ) = ( 𝑈 ‘ 𝑧 ) )
54		fveq2	⊢ ( 𝑥 = 𝑧 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
55		fveq2	⊢ ( 𝑥 = 𝑧 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) )
56	54 55	oveq12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
57		fveq2	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) )
58	53 56 57	breq123d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ↔ ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ) )
59	52 58	rspc	⊢ ( 𝑧 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) → ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ) )
60	41 48 59	sylc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) )
61	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝐷 ∈ Cat )
62	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
63	62 41	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
64	22	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐺 ) : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
65	64 41	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
66		eqid	⊢ ( Sect ‘ 𝐷 ) = ( Sect ‘ 𝐷 )
67	10 7 61 63 65 66	isinv	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ↔ ( ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) ) )
68	60 67	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) )
69	68	simpld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) )
70		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
71		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
72	10 24 70 71 66 61 63 65	issect	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑧 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ↔ ( ( 𝑈 ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∧ ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ) ) )
73	69 72	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ∧ ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ) )
74	73	simp3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
75	74	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) = ( ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) )
76		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑦 ∈ 𝐵 )
77	62 76	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
78		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
79	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
80	2 78 24 79 76 41	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
81		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
82	80 81	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
83	10 24 71 61 77 70 63 82	catlid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) = ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) )
84	75 83	eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) = ( ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) )
85	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) )
86	3 85	nat1st2nd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → 𝑈 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
87	3 86 2 24 41	natcl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈 ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
88	73	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
89	10 24 70 61 77 63 65 82 87 63 88	catass	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑧 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑈 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) ) )
90	3 86 2 78 70 76 41 81	nati	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) )
91	90	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑈 ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ) )
92	84 89 91	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) = ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ) )
93	92	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) = ( ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) )
94	64 76	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
95		nfcv	⊢ Ⅎ 𝑥 ( 𝑈 ‘ 𝑦 )
96		nfcv	⊢ Ⅎ 𝑥 ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) )
97		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 )
98	95 96 97	nfbr	⊢ Ⅎ 𝑥 ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 )
99		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑈 ‘ 𝑥 ) = ( 𝑈 ‘ 𝑦 ) )
100	37 36	oveq12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
101		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) )
102	99 100 101	breq123d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ↔ ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) )
103	98 102	rspc	⊢ ( 𝑦 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) → ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) )
104	76 48 103	sylc	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) )
105	10 7 61 77 94 66	isinv	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ↔ ( ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( 𝑈 ‘ 𝑦 ) ) ) )
106	104 105	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( 𝑈 ‘ 𝑦 ) ) )
107	106	simprd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( 𝑈 ‘ 𝑦 ) )
108	10 24 70 71 66 61 94 77	issect	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Sect ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ( 𝑈 ‘ 𝑦 ) ↔ ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∧ ( 𝑈 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∧ ( ( 𝑈 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
109	107 108	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∧ ( 𝑈 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ∧ ( ( 𝑈 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
110	109	simp1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
111	109	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
112	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
113	2 78 24 112 76 41	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
114	113 81	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
115	10 24 70 61 77 94 65 111 114	catcocl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) )
116	10 24 70 61 94 77 65 110 115 63 88	catass	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) ) )
117	3 86 2 24 76	natcl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( 𝑈 ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
118	10 24 70 61 94 77 94 110 117 65 114	catass	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑈 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) ) )
119	109	simp3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( 𝑈 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) )
120	119	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑈 ‘ 𝑦 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
121	10 24 71 61 94 70 65 114	catrid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( Id ‘ 𝐷 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) )
122	118 120 121	3eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) )
123	122	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( 𝑈 ‘ 𝑦 ) ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ) )
124	93 116 123	3eqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) )
125	124	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) )
126	3 2 78 24 70 5 4	isnat2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ ( 𝐺 𝑁 𝐹 ) ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ X 𝑦 ∈ 𝐵 ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑧 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑦 ( 2^nd ‘ 𝐺 ) 𝑧 ) ‘ 𝑓 ) ) = ( ( ( 𝑦 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑓 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) ) ) )
127	40 125 126	mpbir2and	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ ( 𝐺 𝑁 𝐹 ) )
128		nfv	⊢ Ⅎ 𝑦 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 )
129	128 98 102	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑈 ‘ 𝑥 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) )
130	47 129	sylib	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) )
131	1 2 3 4 5 6 7	fucinv	⊢ ( 𝜑 → ( 𝑈 ( 𝐹 𝐼 𝐺 ) ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ↔ ( 𝑈 ∈ ( 𝐹 𝑁 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ∈ ( 𝐺 𝑁 𝐹 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑈 ‘ 𝑦 ) ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) 𝐽 ( ( 1^st ‘ 𝐺 ) ‘ 𝑦 ) ) ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑦 ) ) ) )
132	8 127 130 131	mpbir3and	⊢ ( 𝜑 → 𝑈 ( 𝐹 𝐼 𝐺 ) ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) )

Metamath Proof Explorer

Theorem invfuc

Proof