invfuc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > invfuc		Structured version Visualization version GIF version

Theorem invfuc 18070

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
invfuc	⊢ (𝜑 → 𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋))

Distinct variable groups: 𝑥,𝐵 𝑥,𝐶 𝑥,𝐷 𝑥,𝐼 𝑥,𝐹 𝑥,𝐺 𝑥,𝐽 𝑥,𝑁 𝜑,𝑥 𝑥,𝑄 𝑥,𝑈 Allowed substitution hint: 𝑋(𝑥)

Proof of Theorem invfuc Dummy variables 𝑦 𝑓 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		invfuc.u	. 2 ⊢ (𝜑 → 𝑈 ∈ (𝐹𝑁𝐺))
2		invfuc.v	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))𝑋)
3		eqid 2762	. . . . . . . . . 10 ⊢ (Base‘𝐷) = (Base‘𝐷)
4		fucinv.j	. . . . . . . . . 10 ⊢ 𝐽 = (Inv‘𝐷)
5		fuciso.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
6		funcrcl 17956	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
7	5, 6	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
8	7	simprd 501	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ Cat)
9	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ Cat)
10		fuciso.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐶)
11		relfunc 17955	. . . . . . . . . . . . 13 ⊢ Rel (𝐶 Func 𝐷)
12		1st2ndbr 8042	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
13	11, 5, 12	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
14	10, 3, 13	funcf1 17959	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝐷))
15	14	ffvelcdmda 7080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1^st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
16		fuciso.g	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
17		1st2ndbr 8042	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝐺)(𝐶 Func 𝐷)(2^nd ‘𝐺))
18	11, 16, 17	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝐺)(𝐶 Func 𝐷)(2^nd ‘𝐺))
19	10, 3, 18	funcf1 17959	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘𝐺):𝐵⟶(Base‘𝐷))
20	19	ffvelcdmda 7080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1^st ‘𝐺)‘𝑥) ∈ (Base‘𝐷))
21		eqid 2762	. . . . . . . . . 10 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
22	3, 4, 9, 15, 20, 21	invss 17854	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥)) ⊆ ((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥))))
23	22	ssbrd 5152	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))𝑋 → (𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋))
24	2, 23	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋)
25		brxp 5708	. . . . . . . 8 ⊢ ((𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋 ↔ ((𝑈‘𝑥) ∈ (((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) ∧ 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥))))
26	25	simprbi 503	. . . . . . 7 ⊢ ((𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋 → 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
27	24, 26	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
28	27	ralrimiva 3156	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
29	10	fvexi 6896	. . . . . 6 ⊢ 𝐵 ∈ V
30		mptelixpg 8945	. . . . . 6 ⊢ (𝐵 ∈ V → ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥))))
31	29, 30	ax-mp 5	. . . . 5 ⊢ ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
32	28, 31	sylibr 237	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
33		fveq2 6882	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝐺)‘𝑥) = ((1^st ‘𝐺)‘𝑦))
34		fveq2 6882	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝐹)‘𝑥) = ((1^st ‘𝐹)‘𝑦))
35	33, 34	oveq12d 7434	. . . . 5 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)) = (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦)))
36	35	cbvixpv 8925	. . . 4 ⊢ X𝑥 ∈ 𝐵 (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)) = X𝑦 ∈ 𝐵 (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦))
37	32, 36	eleqtrdi 2872	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑦 ∈ 𝐵 (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦)))
38		simpr2 1214	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ 𝐵)
39		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
40		eqid 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐵 ↦ 𝑋) = (𝑥 ∈ 𝐵 ↦ 𝑋)
41	40	fvmpt2 7002	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋)
42	39, 27, 41	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋)
43	2, 42	breqtrrd 5137	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))
44	43	ralrimiva 3156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))
45	44	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))
46		nfcv 2924	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑈‘𝑧)
47		nfcv 2924	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))
48		nffvmpt1 6893	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)
49	46, 47, 48	nfbr 5156	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)
50		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝑈‘𝑥) = (𝑈‘𝑧))
51		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((1^st ‘𝐹)‘𝑥) = ((1^st ‘𝐹)‘𝑧))
52		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((1^st ‘𝐺)‘𝑥) = ((1^st ‘𝐺)‘𝑧))
53	51, 52	oveq12d 7434	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥)) = (((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧)))
54		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))
55	50, 53, 54	breq123d 5121	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)))
56	49, 55	rspc 3567	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)))
57	38, 45, 56	sylc 66	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))
58	8	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐷 ∈ Cat)
59	14	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐹):𝐵⟶(Base‘𝐷))
60	59, 38	ffvelcdmd 7081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐹)‘𝑧) ∈ (Base‘𝐷))
61	19	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐺):𝐵⟶(Base‘𝐷))
62	61, 38	ffvelcdmd 7081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐺)‘𝑧) ∈ (Base‘𝐷))
63		eqid 2762	. . . . . . . . . . . . . 14 ⊢ (Sect‘𝐷) = (Sect‘𝐷)
64	3, 4, 58, 60, 62, 63	isinv 17853	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ↔ ((𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)(Sect‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1^st ‘𝐺)‘𝑧)(Sect‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧))))
65	57, 64	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)(Sect‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1^st ‘𝐺)‘𝑧)(Sect‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧)))
66	65	simpld 500	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)(Sect‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))
67		eqid 2762	. . . . . . . . . . . 12 ⊢ (comp‘𝐷) = (comp‘𝐷)
68		eqid 2762	. . . . . . . . . . . 12 ⊢ (Id‘𝐷) = (Id‘𝐷)
69	3, 21, 67, 68, 63, 58, 60, 62	issect 17846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐹)‘𝑧)))))
70	66, 69	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧) ∈ (((1^st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1^st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑧)) ∧ (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐹)‘𝑧), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1^st ‘𝐹)‘𝑧))))
71	70	simp3d 1162	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐹)‘𝑧), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1^st ‘𝐹)‘𝑧)))
72	71	oveq1d 7431	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐹)𝑧)‘𝑓)))
73		simpr1 1213	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ 𝐵)
74	59, 73	ffvelcdmd 7081	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
75		eqid 2762	. . . . . . . . . . 11 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
76	13	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
77	10, 75, 21, 76, 73, 38	funcf2 17961	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2^nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑧)))
78		simpr3 1215	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))
79	77, 78	ffvelcdmd 7081	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2^nd ‘𝐹)𝑧)‘𝑓) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑧)))
80	3, 21, 68, 58, 74, 67, 60, 79	catlid 17775	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((Id‘𝐷)‘((1^st ‘𝐹)‘𝑧))(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐹)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)) = ((𝑦(2^nd ‘𝐹)𝑧)‘𝑓))
81	72, 80	eqtr2d 2798	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2^nd ‘𝐹)𝑧)‘𝑓) = ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐹)‘𝑧), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧))(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐹)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)))
82		fuciso.n	. . . . . . . . 9 ⊢ 𝑁 = (𝐶 Nat 𝐷)
83	1	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (𝐹𝑁𝐺))
84	82, 83	nat1st2nd 18047	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩𝑁⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩))
85	82, 84, 10, 21, 38	natcl 18049	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧) ∈ (((1^st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)))
86	70	simp2d 1161	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1^st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑧)))
87	3, 21, 67, 58, 74, 60, 62, 79, 85, 60, 86	catass 17778	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐹)𝑧)‘𝑓))))
88	82, 84, 10, 75, 67, 73, 38, 78	nati 18051	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐹)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)) = (((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))(𝑈‘𝑦)))
89	88	oveq2d 7432	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐺)‘𝑧))(𝑈‘𝑦))))
90	81, 87, 89	3eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2^nd ‘𝐹)𝑧)‘𝑓) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))(((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))(𝑈‘𝑦))))
91	90	oveq1d 7431	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
92	61, 73	ffvelcdmd 7081	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐺)‘𝑦) ∈ (Base‘𝐷))
93		nfcv 2924	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑈‘𝑦)
94		nfcv 2924	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))
95		nffvmpt1 6893	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)
96	93, 94, 95	nfbr 5156	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)
97		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑈‘𝑥) = (𝑈‘𝑦))
98	34, 33	oveq12d 7434	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥)) = (((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦)))
99		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
100	97, 98, 99	breq123d 5121	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
101	96, 100	rspc 3567	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
102	73, 45, 101	sylc 66	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
103	3, 4, 58, 74, 92, 63	isinv 17853	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ↔ ((𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)(Sect‘𝐷)((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1^st ‘𝐺)‘𝑦)(Sect‘𝐷)((1^st ‘𝐹)‘𝑦))(𝑈‘𝑦))))
104	102, 103	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)(Sect‘𝐷)((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1^st ‘𝐺)‘𝑦)(Sect‘𝐷)((1^st ‘𝐹)‘𝑦))(𝑈‘𝑦)))
105	104	simprd 501	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1^st ‘𝐺)‘𝑦)(Sect‘𝐷)((1^st ‘𝐹)‘𝑦))(𝑈‘𝑦))
106	3, 21, 67, 68, 63, 58, 92, 74	issect 17846	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐺)‘𝑦)))))
107	105, 106	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦)) ∧ (𝑈‘𝑦) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑦)) ∧ ((𝑈‘𝑦)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1^st ‘𝐺)‘𝑦))))
108	107	simp1d 1160	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦)))
109	107	simp2d 1161	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑦)))
110	18	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐺)(𝐶 Func 𝐷)(2^nd ‘𝐺))
111	10, 75, 21, 110, 73, 38	funcf2 17961	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2^nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)))
112	111, 78	ffvelcdmd 7081	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2^nd ‘𝐺)𝑧)‘𝑓) ∈ (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)))
113	3, 21, 67, 58, 74, 92, 62, 109, 112	catcocl 17777	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))(𝑈‘𝑦)) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)))
114	3, 21, 67, 58, 92, 74, 62, 108, 113, 60, 86	catass 17778	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))))
115	82, 84, 10, 21, 73	natcl 18049	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑦)))
116	3, 21, 67, 58, 92, 74, 92, 108, 115, 62, 112	catass 17778	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))))
117	107	simp3d 1162	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1^st ‘𝐺)‘𝑦)))
118	117	oveq2d 7432	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐺)‘𝑦))))
119	3, 21, 68, 58, 92, 67, 62, 112	catrid 17776	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))((Id‘𝐷)‘((1^st ‘𝐺)‘𝑦))) = ((𝑦(2^nd ‘𝐺)𝑧)‘𝑓))
120	116, 118, 119	3eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))(𝑈‘𝑦))(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((𝑦(2^nd ‘𝐺)𝑧)‘𝑓))
121	120	oveq2d 7432	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(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 ‘𝐺)𝑧)‘𝑓)))
122	91, 114, 121	3eqtrrd 2802	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
123	122	ralrimivvva 3210	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
124	82, 10, 75, 21, 67, 16, 5	isnat2 18044	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹) ↔ ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ 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 ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))))
125	37, 123, 124	mpbir2and 726	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹))
126		nfv 1947	. . . 4 ⊢ Ⅎ𝑦(𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)
127	126, 96, 100	cbvralw 3306	. . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
128	44, 127	sylib 221	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
129		fuciso.q	. . 3 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
130		fucinv.i	. . 3 ⊢ 𝐼 = (Inv‘𝑄)
131	129, 10, 82, 5, 16, 130, 4	fucinv 18069	. 2 ⊢ (𝜑 → (𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋) ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹) ∧ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))))
132	1, 125, 128, 131	mpbir3and 1361	1 ⊢ (𝜑 → 𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3078 Vcvv 3453 ⟨cop 4593 class class class wbr 5107 ↦ cmpt 5190 × cxp 5657 Rel wrel 5664 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 1^st c1st 7987 2^nd c2nd 7988 Xcixp 8907 Basecbs 17305 Hom chom 17357 compcco 17358 Catccat 17756 Idccid 17757 Sectcsect 17837 Invcinv 17838 Func cfunc 17947 Nat cnat 18037 FuncCat cfuc 18038

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-er 8699 df-map 8831 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-fz 13564 df-struct 17243 df-slot 17278 df-ndx 17290 df-base 17306 df-hom 17370 df-cco 17371 df-cat 17760 df-cid 17761 df-sect 17840 df-inv 17841 df-func 17951 df-nat 18039 df-fuc 18040

This theorem is used by: fuciso 18071 yonedainv 18373

W3C validator