Theorem funcpropd 16383

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.)

Hypotheses

Ref	Expression
funcpropd.1	⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))
funcpropd.2	⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))
funcpropd.3	⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))
funcpropd.4	⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))
funcpropd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
funcpropd.b	⊢ (𝜑 → 𝐵 ∈ 𝑉)
funcpropd.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)
funcpropd.d	⊢ (𝜑 → 𝐷 ∈ 𝑉)

Assertion

Ref	Expression
funcpropd	⊢ (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))

Proof of Theorem funcpropd

Dummy variables 𝑓 𝑔 𝑚 𝑛 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relfunc 16345	. 2 ⊢ Rel (𝐴 Func 𝐶)
2		relfunc 16345	. 2 ⊢ Rel (𝐵 Func 𝐷)
3		funcpropd.1	. . . . . 6 ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))
4		funcpropd.2	. . . . . 6 ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))
5		funcpropd.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
6		funcpropd.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
7	3, 4, 5, 6	catpropd 16192	. . . . 5 ⊢ (𝜑 → (𝐴 ∈ Cat ↔ 𝐵 ∈ Cat))
8		funcpropd.3	. . . . . 6 ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))
9		funcpropd.4	. . . . . 6 ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))
10		funcpropd.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
11		funcpropd.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
12	8, 9, 10, 11	catpropd 16192	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
13	7, 12	anbi12d 743	. . . 4 ⊢ (𝜑 → ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ↔ (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat)))
14		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑤 → (1st ‘𝑧) = (1st ‘𝑤))
15	14	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑓‘(1st ‘𝑧)) = (𝑓‘(1st ‘𝑤)))
16		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑤 → (2nd ‘𝑧) = (2nd ‘𝑤))
17	16	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑓‘(2nd ‘𝑧)) = (𝑓‘(2nd ‘𝑤)))
18	15, 17	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))))
19		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘𝑤))
20	18, 19	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
21	20	cbvixpv 7812	. . . . . . . . . 10 ⊢ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤))
22	21	eleq2i 2680	. . . . . . . . 9 ⊢ (𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
23	22	anbi2i 726	. . . . . . . 8 ⊢ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤))))
24	3	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Homf ‘𝐴) = (Homf ‘𝐵))
25	4	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (compf‘𝐴) = (compf‘𝐵))
26	5	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐴 ∈ 𝑉)
27	6	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐵 ∈ 𝑉)
28	24, 25, 26, 27	cidpropd 16193	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐴) = (Id‘𝐵))
29	28	fveq1d 6105	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐴)‘𝑥) = ((Id‘𝐵)‘𝑥))
30	29	fveq2d 6107	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)))
31	8, 9, 10, 11	cidpropd 16193	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷))
32	31	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐶) = (Id‘𝐷))
33	32	fveq1d 6105	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐶)‘(𝑓‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)))
34	30, 33	eqeq12d 2625	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ↔ ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥))))
35		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐴) = (Base‘𝐴)
36		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (Hom ‘𝐴) = (Hom ‘𝐴)
37		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (comp‘𝐴) = (comp‘𝐴)
38		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (comp‘𝐵) = (comp‘𝐵)
39	3	ad6antr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf ‘𝐴) = (Homf ‘𝐵))
40	4	ad6antr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (compf‘𝐴) = (compf‘𝐵))
41		simp-5r 805	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑥 ∈ (Base‘𝐴))
42		simp-4r 803	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑦 ∈ (Base‘𝐴))
43		simpllr 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑧 ∈ (Base‘𝐴))
44		simplr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦))
45		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧))
46	35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45	comfeqval 16191	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚))
47	46	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)))
48		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐶) = (Base‘𝐶)
49		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
50		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ (comp‘𝐶) = (comp‘𝐶)
51		eqid 2610	. . . . . . . . . . . . . . . . 17 ⊢ (comp‘𝐷) = (comp‘𝐷)
52	8	ad6antr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf ‘𝐶) = (Homf ‘𝐷))
53	9	ad6antr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (compf‘𝐶) = (compf‘𝐷))
54		simprl 790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
55	54	ad5antr 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
56	55, 41	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑥) ∈ (Base‘𝐶))
57	55, 42	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑦) ∈ (Base‘𝐶))
58	55, 43	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑧) ∈ (Base‘𝐶))
59		df-ov 6552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑔𝑦) = (𝑔‘⟨𝑥, 𝑦⟩)
60		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
61	60	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
62	61	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))
63		simp-4r 803	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑥 ∈ (Base‘𝐴))
64		simpllr 795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑦 ∈ (Base‘𝐴))
65		opelxpi 5072	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
66	63, 64, 65	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
67		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑥 ∈ V
68		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑦 ∈ V
69	67, 68	op1std 7069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑤) = 𝑥)
70	69	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(1st ‘𝑤)) = (𝑓‘𝑥))
71	67, 68	op2ndd 7070	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑤) = 𝑦)
72	71	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(2nd ‘𝑤)) = (𝑓‘𝑦))
73	70, 72	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
74		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩))
75		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥(Hom ‘𝐴)𝑦) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩)
76	74, 75	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑥(Hom ‘𝐴)𝑦))
77	73, 76	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) = (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
78	77	fvixp 7799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
79	62, 66, 78	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
80	59, 79	syl5eqel 2692	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)))
81		elmapi 7765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑔𝑦) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑𝑚 (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
83	82	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
84	83, 44	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑦)‘𝑚) ∈ ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
85		df-ov 6552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦𝑔𝑧) = (𝑔‘⟨𝑦, 𝑧⟩)
86		opelxpi 5072	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ (Base‘𝐴) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
87	86	adantll 746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
88		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑧 ∈ V
89	68, 88	op1std 7069	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (1st ‘𝑤) = 𝑦)
90	89	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(1st ‘𝑤)) = (𝑓‘𝑦))
91	68, 88	op2ndd 7070	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (2nd ‘𝑤) = 𝑧)
92	91	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(2nd ‘𝑤)) = (𝑓‘𝑧))
93	90, 92	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) = ((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
94		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩))
95		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦(Hom ‘𝐴)𝑧) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩)
96	94, 95	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑦(Hom ‘𝐴)𝑧))
97	93, 96	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) = (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
98	97	fvixp 7799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
99	61, 87, 98	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
100	85, 99	syl5eqel 2692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)))
101		elmapi 7765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦𝑔𝑧) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑𝑚 (𝑦(Hom ‘𝐴)𝑧)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
103	102	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
104	103	ffvelrnda 6267	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑦𝑔𝑧)‘𝑛) ∈ ((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
105	48, 49, 50, 51, 52, 53, 56, 57, 58, 84, 104	comfeqval 16191	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))
106	47, 105	eqeq12d 2625	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
107	106	ralbidva 2968	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
108	107	ralbidva 2968	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
109		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝐵) = (Hom ‘𝐵)
110	24	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Homf ‘𝐴) = (Homf ‘𝐵))
111		simpllr 795	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑥 ∈ (Base‘𝐴))
112		simplr 788	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑦 ∈ (Base‘𝐴))
113	35, 36, 109, 110, 111, 112	homfeqval 16180	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑥(Hom ‘𝐴)𝑦) = (𝑥(Hom ‘𝐵)𝑦))
114		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
115	35, 36, 109, 110, 112, 114	homfeqval 16180	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦(Hom ‘𝐴)𝑧) = (𝑦(Hom ‘𝐵)𝑧))
116	115	raleqdv 3121	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
117	113, 116	raleqbidv 3129	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
118	108, 117	bitrd 267	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
119	118	ralbidva 2968	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
120	119	ralbidva 2968	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
121	34, 120	anbi12d 743	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
122	121	ralbidva 2968	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑𝑚 ((Hom ‘𝐴)‘𝑤)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
123	23, 122	sylan2b 491	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
124	123	pm5.32da 671	. . . . . 6 ⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
125		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
126	8	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf ‘𝐶) = (Homf ‘𝐷))
127		simplr 788	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
128		xp1st 7089	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (1st ‘𝑧) ∈ (Base‘𝐴))
129	128	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (1st ‘𝑧) ∈ (Base‘𝐴))
130	127, 129	ffvelrnd 6268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(1st ‘𝑧)) ∈ (Base‘𝐶))
131		xp2nd 7090	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (2nd ‘𝑧) ∈ (Base‘𝐴))
132	131	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (2nd ‘𝑧) ∈ (Base‘𝐴))
133	127, 132	ffvelrnd 6268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(2nd ‘𝑧)) ∈ (Base‘𝐶))
134	48, 49, 125, 126, 130, 133	homfeqval 16180	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))))
135	3	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf ‘𝐴) = (Homf ‘𝐵))
136	35, 36, 109, 135, 129, 132	homfeqval 16180	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((1st ‘𝑧)(Hom ‘𝐴)(2nd ‘𝑧)) = ((1st ‘𝑧)(Hom ‘𝐵)(2nd ‘𝑧)))
137		df-ov 6552	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘𝑧)(Hom ‘𝐴)(2nd ‘𝑧)) = ((Hom ‘𝐴)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
138		df-ov 6552	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘𝑧)(Hom ‘𝐵)(2nd ‘𝑧)) = ((Hom ‘𝐵)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
139	136, 137, 138	3eqtr3g 2667	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) = ((Hom ‘𝐵)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
140		1st2nd2 7096	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
141	140	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
142	141	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
143	141	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐵)‘𝑧) = ((Hom ‘𝐵)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
144	139, 142, 143	3eqtr4d 2654	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐵)‘𝑧))
145	134, 144	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
146	145	ixpeq2dva 7809	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
147	3	homfeqbas 16179	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
148	147	sqxpeqd 5065	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
149	148	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
150	149	ixpeq1d 7806	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
151	146, 150	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))
152	151	eleq2d 2673	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → (𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))))
153	152	pm5.32da 671	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))))
154	8	homfeqbas 16179	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
155	147, 154	feq23d 5953	. . . . . . . . 9 ⊢ (𝜑 → (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ↔ 𝑓:(Base‘𝐵)⟶(Base‘𝐷)))
156	155	anbi1d 737	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))))
157	153, 156	bitrd 267	. . . . . . 7 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)))))
158	147	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
159	158	raleqdv 3121	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
160	158, 159	raleqbidv 3129	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
161	160	anbi2d 736	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
162	147, 161	raleqbidva 3131	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
163	157, 162	anbi12d 743	. . . . . 6 ⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
164	124, 163	bitrd 267	. . . . 5 ⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
165		df-3an 1033	. . . . 5 ⊢ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
166		df-3an 1033	. . . . 5 ⊢ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
167	164, 165, 166	3bitr4g 302	. . . 4 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
168	13, 167	anbi12d 743	. . 3 ⊢ (𝜑 → (((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))))
169		df-br 4584	. . . . 5 ⊢ (𝑓(𝐴 Func 𝐶)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶))
170		funcrcl 16346	. . . . 5 ⊢ (⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶) → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
171	169, 170	sylbi 206	. . . 4 ⊢ (𝑓(𝐴 Func 𝐶)𝑔 → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
172		eqid 2610	. . . . 5 ⊢ (Id‘𝐴) = (Id‘𝐴)
173		eqid 2610	. . . . 5 ⊢ (Id‘𝐶) = (Id‘𝐶)
174		simpl 472	. . . . 5 ⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐴 ∈ Cat)
175		simpr 476	. . . . 5 ⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat)
176	35, 48, 36, 49, 172, 173, 37, 50, 174, 175	isfunc 16347	. . . 4 ⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → (𝑓(𝐴 Func 𝐶)𝑔 ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
177	171, 176	biadan2 672	. . 3 ⊢ (𝑓(𝐴 Func 𝐶)𝑔 ↔ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
178		df-br 4584	. . . . 5 ⊢ (𝑓(𝐵 Func 𝐷)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷))
179		funcrcl 16346	. . . . 5 ⊢ (⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷) → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
180	178, 179	sylbi 206	. . . 4 ⊢ (𝑓(𝐵 Func 𝐷)𝑔 → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
181		eqid 2610	. . . . 5 ⊢ (Base‘𝐵) = (Base‘𝐵)
182		eqid 2610	. . . . 5 ⊢ (Base‘𝐷) = (Base‘𝐷)
183		eqid 2610	. . . . 5 ⊢ (Id‘𝐵) = (Id‘𝐵)
184		eqid 2610	. . . . 5 ⊢ (Id‘𝐷) = (Id‘𝐷)
185		simpl 472	. . . . 5 ⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐵 ∈ Cat)
186		simpr 476	. . . . 5 ⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐷 ∈ Cat)
187	181, 182, 109, 125, 183, 184, 38, 51, 185, 186	isfunc 16347	. . . 4 ⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓(𝐵 Func 𝐷)𝑔 ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
188	180, 187	biadan2 672	. . 3 ⊢ (𝑓(𝐵 Func 𝐷)𝑔 ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑𝑚 ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
189	168, 177, 188	3bitr4g 302	. 2 ⊢ (𝜑 → (𝑓(𝐴 Func 𝐶)𝑔 ↔ 𝑓(𝐵 Func 𝐷)𝑔))
190	1, 2, 189	eqbrrdiv 5141	1 ⊢ (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ⟨cop 4131   class class class wbr 4583   × cxp 5036  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058   ↑_𝑚 cmap 7744  Xcixp 7794  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148  Idccid 16149  Hom_f chomf 16150  comp_fccomf 16151   Func cfunc 16337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-ixp 7795  df-cat 16152  df-cid 16153  df-homf 16154  df-comf 16155  df-func 16341

This theorem is referenced by:  funcres2c  16384  fullpropd  16403  fthpropd  16404  ressffth  16421  natpropd  16459  fucpropd  16460  funcsetcres2  16566