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 17944

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 2736	. . . . . . . . . 10 ⊢ (Base‘𝐷) = (Base‘𝐷)
4		fucinv.j	. . . . . . . . . 10 ⊢ 𝐽 = (Inv‘𝐷)
5		fuciso.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
6		funcrcl 17830	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
7	5, 6	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
8	7	simprd 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ Cat)
9	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ Cat)
10		fuciso.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝐶)
11		relfunc 17829	. . . . . . . . . . . . 13 ⊢ Rel (𝐶 Func 𝐷)
12		1st2ndbr 7995	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
13	11, 5, 12	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
14	10, 3, 13	funcf1 17833	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝐷))
15	14	ffvelcdmda 7036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1^st ‘𝐹)‘𝑥) ∈ (Base‘𝐷))
16		fuciso.g	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷))
17		1st2ndbr 7995	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝐺)(𝐶 Func 𝐷)(2^nd ‘𝐺))
18	11, 16, 17	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝐺)(𝐶 Func 𝐷)(2^nd ‘𝐺))
19	10, 3, 18	funcf1 17833	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘𝐺):𝐵⟶(Base‘𝐷))
20	19	ffvelcdmda 7036	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1^st ‘𝐺)‘𝑥) ∈ (Base‘𝐷))
21		eqid 2736	. . . . . . . . . 10 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
22	3, 4, 9, 15, 20, 21	invss 17728	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥)) ⊆ ((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥))))
23	22	ssbrd 5128	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))𝑋 → (𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋))
24	2, 23	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋)
25		brxp 5680	. . . . . . . 8 ⊢ ((𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋 ↔ ((𝑈‘𝑥) ∈ (((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) ∧ 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥))))
26	25	simprbi 497	. . . . . . 7 ⊢ ((𝑈‘𝑥)((((1^st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑥)) × (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))𝑋 → 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
27	24, 26	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
28	27	ralrimiva 3129	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
29	10	fvexi 6854	. . . . . 6 ⊢ 𝐵 ∈ V
30		mptelixpg 8883	. . . . . 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 234	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)))
33		fveq2 6840	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝐺)‘𝑥) = ((1^st ‘𝐺)‘𝑦))
34		fveq2 6840	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((1^st ‘𝐹)‘𝑥) = ((1^st ‘𝐹)‘𝑦))
35	33, 34	oveq12d 7385	. . . . 5 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)) = (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦)))
36	35	cbvixpv 8863	. . . 4 ⊢ X𝑥 ∈ 𝐵 (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥)) = X𝑦 ∈ 𝐵 (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦))
37	32, 36	eleqtrdi 2846	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑦 ∈ 𝐵 (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦)))
38		simpr2 1197	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ 𝐵)
39		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
40		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐵 ↦ 𝑋) = (𝑥 ∈ 𝐵 ↦ 𝑋)
41	40	fvmpt2 6959	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ (((1^st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑥))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋)
42	39, 27, 41	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋)
43	2, 42	breqtrrd 5113	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))
44	43	ralrimiva 3129	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))
45	44	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥))
46		nfcv 2898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑈‘𝑧)
47		nfcv 2898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))
48		nffvmpt1 6851	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)
49	46, 47, 48	nfbr 5132	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)
50		fveq2 6840	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (𝑈‘𝑥) = (𝑈‘𝑧))
51		fveq2 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((1^st ‘𝐹)‘𝑥) = ((1^st ‘𝐹)‘𝑧))
52		fveq2 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ((1^st ‘𝐺)‘𝑥) = ((1^st ‘𝐺)‘𝑧))
53	51, 52	oveq12d 7385	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥)) = (((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧)))
54		fveq2 6840	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))
55	50, 53, 54	breq123d 5099	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)))
56	49, 55	rspc 3552	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)))
57	38, 45, 56	sylc 65	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))
58	8	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐷 ∈ Cat)
59	14	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐹):𝐵⟶(Base‘𝐷))
60	59, 38	ffvelcdmd 7037	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐹)‘𝑧) ∈ (Base‘𝐷))
61	19	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐺):𝐵⟶(Base‘𝐷))
62	61, 38	ffvelcdmd 7037	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐺)‘𝑧) ∈ (Base‘𝐷))
63		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (Sect‘𝐷) = (Sect‘𝐷)
64	3, 4, 58, 60, 62, 63	isinv 17727	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)𝐽((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ↔ ((𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)(Sect‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1^st ‘𝐺)‘𝑧)(Sect‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧))))
65	57, 64	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)(Sect‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1^st ‘𝐺)‘𝑧)(Sect‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧)))
66	65	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1^st ‘𝐹)‘𝑧)(Sect‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))
67		eqid 2736	. . . . . . . . . . . 12 ⊢ (comp‘𝐷) = (comp‘𝐷)
68		eqid 2736	. . . . . . . . . . . 12 ⊢ (Id‘𝐷) = (Id‘𝐷)
69	3, 21, 67, 68, 63, 58, 60, 62	issect 17720	. . . . . . . . . . 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 232	. . . . . . . . . 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 1145	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐹)‘𝑧), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1^st ‘𝐹)‘𝑧)))
72	71	oveq1d 7382	. . . . . . . 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 1196	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ 𝐵)
74	59, 73	ffvelcdmd 7037	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐹)‘𝑦) ∈ (Base‘𝐷))
75		eqid 2736	. . . . . . . . . . 11 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
76	13	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐹)(𝐶 Func 𝐷)(2^nd ‘𝐹))
77	10, 75, 21, 76, 73, 38	funcf2 17835	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2^nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑧)))
78		simpr3 1198	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))
79	77, 78	ffvelcdmd 7037	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2^nd ‘𝐹)𝑧)‘𝑓) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑧)))
80	3, 21, 68, 58, 74, 67, 60, 79	catlid 17649	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((Id‘𝐷)‘((1^st ‘𝐹)‘𝑧))(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐹)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)) = ((𝑦(2^nd ‘𝐹)𝑧)‘𝑓))
81	72, 80	eqtr2d 2772	. . . . . . 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 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (𝐹𝑁𝐺))
84	82, 83	nat1st2nd 17921	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩𝑁⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩))
85	82, 84, 10, 21, 38	natcl 17923	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧) ∈ (((1^st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)))
86	70	simp2d 1144	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1^st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑧)))
87	3, 21, 67, 58, 74, 60, 62, 79, 85, 60, 86	catass 17652	. . . . . . 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 17925	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐹)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)) = (((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))(𝑈‘𝑦)))
89	88	oveq2d 7383	. . . . . . 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 2775	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2^nd ‘𝐹)𝑧)‘𝑓) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))(((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))(𝑈‘𝑦))))
91	90	oveq1d 7382	. . . . 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 7037	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1^st ‘𝐺)‘𝑦) ∈ (Base‘𝐷))
93		nfcv 2898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑈‘𝑦)
94		nfcv 2898	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))
95		nffvmpt1 6851	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)
96	93, 94, 95	nfbr 5132	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)
97		fveq2 6840	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑈‘𝑥) = (𝑈‘𝑦))
98	34, 33	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥)) = (((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦)))
99		fveq2 6840	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
100	97, 98, 99	breq123d 5099	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
101	96, 100	rspc 3552	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
102	73, 45, 101	sylc 65	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
103	3, 4, 58, 74, 92, 63	isinv 17727	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ↔ ((𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)(Sect‘𝐷)((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1^st ‘𝐺)‘𝑦)(Sect‘𝐷)((1^st ‘𝐹)‘𝑦))(𝑈‘𝑦))))
104	102, 103	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)(Sect‘𝐷)((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1^st ‘𝐺)‘𝑦)(Sect‘𝐷)((1^st ‘𝐹)‘𝑦))(𝑈‘𝑦)))
105	104	simprd 495	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1^st ‘𝐺)‘𝑦)(Sect‘𝐷)((1^st ‘𝐹)‘𝑦))(𝑈‘𝑦))
106	3, 21, 67, 68, 63, 58, 92, 74	issect 17720	. . . . . . . 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 232	. . . . . . 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 1143	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐹)‘𝑦)))
109	107	simp2d 1144	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑦)))
110	18	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1^st ‘𝐺)(𝐶 Func 𝐷)(2^nd ‘𝐺))
111	10, 75, 21, 110, 73, 38	funcf2 17835	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2^nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)))
112	111, 78	ffvelcdmd 7037	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2^nd ‘𝐺)𝑧)‘𝑓) ∈ (((1^st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑧)))
113	3, 21, 67, 58, 74, 92, 62, 109, 112	catcocl 17651	. . . . . 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 17652	. . . . 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 17923	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1^st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1^st ‘𝐺)‘𝑦)))
116	3, 21, 67, 58, 92, 74, 92, 108, 115, 62, 112	catass 17652	. . . . . . 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 1145	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1^st ‘𝐺)‘𝑦)))
118	117	oveq2d 7383	. . . . . . 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 17650	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))((Id‘𝐷)‘((1^st ‘𝐺)‘𝑦))) = ((𝑦(2^nd ‘𝐺)𝑧)‘𝑓))
120	116, 118, 119	3eqtrd 2775	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)(⟨((1^st ‘𝐹)‘𝑦), ((1^st ‘𝐺)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))(𝑈‘𝑦))(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((𝑦(2^nd ‘𝐺)𝑧)‘𝑓))
121	120	oveq2d 7383	. . . . 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 2776	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐺)‘𝑧)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑦(2^nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2^nd ‘𝐹)𝑧)‘𝑓)(⟨((1^st ‘𝐺)‘𝑦), ((1^st ‘𝐹)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))
123	122	ralrimivvva 3183	. . 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 17918	. . 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 714	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹))
126		nfv 1916	. . . 4 ⊢ Ⅎ𝑦(𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)
127	126, 96, 100	cbvralw 3279	. . 3 ⊢ (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1^st ‘𝐹)‘𝑥)𝐽((1^st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
128	44, 127	sylib 218	. 2 ⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))
129		fuciso.q	. . 3 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
130		fucinv.i	. . 3 ⊢ 𝐼 = (Inv‘𝑄)
131	129, 10, 82, 5, 16, 130, 4	fucinv 17943	. 2 ⊢ (𝜑 → (𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋) ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹) ∧ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1^st ‘𝐹)‘𝑦)𝐽((1^st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))))
132	1, 125, 128, 131	mpbir3and 1344	1 ⊢ (𝜑 → 𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3051 Vcvv 3429 ⟨cop 4573 class class class wbr 5085 ↦ cmpt 5166 × cxp 5629 Rel wrel 5636 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 1^st c1st 7940 2^nd c2nd 7941 Xcixp 8845 Basecbs 17179 Hom chom 17231 compcco 17232 Catccat 17630 Idccid 17631 Sectcsect 17711 Invcinv 17712 Func cfunc 17821 Nat cnat 17911 FuncCat cfuc 17912

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-map 8775 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-fz 13462 df-struct 17117 df-slot 17152 df-ndx 17164 df-base 17180 df-hom 17244 df-cco 17245 df-cat 17634 df-cid 17635 df-sect 17714 df-inv 17715 df-func 17825 df-nat 17913 df-fuc 17914

This theorem is referenced by: fuciso 17945 yonedainv 18247

W3C validator