funcpropd - Metamath Proof Explorer

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

Theorem funcpropd 18057

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	⊢ (𝜑 → (Hom_f ‘𝐴) = (Hom_f ‘𝐵))
funcpropd.2	⊢ (𝜑 → (comp_f‘𝐴) = (comp_f‘𝐵))
funcpropd.3	⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
funcpropd.4	⊢ (𝜑 → (comp_f‘𝐶) = (comp_f‘𝐷))
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 18017	. 2 ⊢ Rel (𝐴 Func 𝐶)
2		relfunc 18017	. 2 ⊢ Rel (𝐵 Func 𝐷)
3		funcpropd.1	. . . . . 6 ⊢ (𝜑 → (Hom_f ‘𝐴) = (Hom_f ‘𝐵))
4		funcpropd.2	. . . . . 6 ⊢ (𝜑 → (comp_f‘𝐴) = (comp_f‘𝐵))
5		funcpropd.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
6		funcpropd.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
7	3, 4, 5, 6	catpropd 17863	. . . . 5 ⊢ (𝜑 → (𝐴 ∈ Cat ↔ 𝐵 ∈ Cat))
8		funcpropd.3	. . . . . 6 ⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
9		funcpropd.4	. . . . . 6 ⊢ (𝜑 → (comp_f‘𝐶) = (comp_f‘𝐷))
10		funcpropd.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
11		funcpropd.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
12	8, 9, 10, 11	catpropd 17863	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
13	7, 12	anbi12d 644	. . . 4 ⊢ (𝜑 → ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ↔ (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat)))
14		2fveq3 6882	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑓‘(1^st ‘𝑧)) = (𝑓‘(1^st ‘𝑤)))
15		2fveq3 6882	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑤 → (𝑓‘(2^nd ‘𝑧)) = (𝑓‘(2^nd ‘𝑤)))
16	14, 15	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) = ((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))))
17		fveq2 6877	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑤 → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘𝑤))
18	16, 17	oveq12d 7430	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))
19	18	cbvixpv 8927	. . . . . . . . . 10 ⊢ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) = X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤))
20	19	eleq2i 2853	. . . . . . . . 9 ⊢ (𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))
21	20	anbi2i 635	. . . . . . . 8 ⊢ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤))))
22	3	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Hom_f ‘𝐴) = (Hom_f ‘𝐵))
23	4	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (comp_f‘𝐴) = (comp_f‘𝐵))
24	5	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐴 ∈ 𝑉)
25	6	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐵 ∈ 𝑉)
26	22, 23, 24, 25	cidpropd 17864	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐴) = (Id‘𝐵))
27	26	fveq1d 6879	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐴)‘𝑥) = ((Id‘𝐵)‘𝑥))
28	27	fveq2d 6881	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)))
29	8, 9, 10, 11	cidpropd 17864	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷))
30	29	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐶) = (Id‘𝐷))
31	30	fveq1d 6879	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐶)‘(𝑓‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)))
32	28, 31	eqeq12d 2777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ↔ ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥))))
33		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘𝐴) = (Base‘𝐴)
34		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (Hom ‘𝐴) = (Hom ‘𝐴)
35		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (comp‘𝐴) = (comp‘𝐴)
36		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (comp‘𝐵) = (comp‘𝐵)
37	3	ad6antr 749	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Hom_f ‘𝐴) = (Hom_f ‘𝐵))
38	4	ad6antr 749	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (comp_f‘𝐴) = (comp_f‘𝐵))
39		simp-5r 798	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑥 ∈ (Base‘𝐴))
40		simp-4r 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑦 ∈ (Base‘𝐴))
41		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑧 ∈ (Base‘𝐴))
42		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦))
43		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧))
44	33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43	comfeqval 17862	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚))
45	44	fveq2d 6881	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)))
46		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐶) = (Base‘𝐶)
47		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
48		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (comp‘𝐶) = (comp‘𝐶)
49		eqid 2761	. . . . . . . . . . . . . . . . 17 ⊢ (comp‘𝐷) = (comp‘𝐷)
50	8	ad6antr 749	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
51	9	ad6antr 749	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (comp_f‘𝐶) = (comp_f‘𝐷))
52		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
53	52	ad5antr 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
54	53, 39	ffvelcdmd 7077	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑥) ∈ (Base‘𝐶))
55	53, 40	ffvelcdmd 7077	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑦) ∈ (Base‘𝐶))
56	53, 41	ffvelcdmd 7077	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑧) ∈ (Base‘𝐶))
57		df-ov 7415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑔𝑦) = (𝑔‘⟨𝑥, 𝑦⟩)
58		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))
59	58	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))
60	59	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))
61		opelxpi 5688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
62	61	ad5ant23 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
63		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑥 ∈ V
64		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑦 ∈ V
65	63, 64	op1std 8000	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (1^st ‘𝑤) = 𝑥)
66	65	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(1^st ‘𝑤)) = (𝑓‘𝑥))
67	63, 64	op2ndd 8001	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (2^nd ‘𝑤) = 𝑦)
68	67	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (𝑓‘(2^nd ‘𝑤)) = (𝑓‘𝑦))
69	66, 68	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
70		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩))
71		df-ov 7415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥(Hom ‘𝐴)𝑦) = ((Hom ‘𝐴)‘⟨𝑥, 𝑦⟩)
72	70, 71	eqtr4di 2814	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑥(Hom ‘𝐴)𝑦))
73	69, 72	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ⟨𝑥, 𝑦⟩ → (((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)) = (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑_m (𝑥(Hom ‘𝐴)𝑦)))
74	73	fvixp 8914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑥, 𝑦⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑_m (𝑥(Hom ‘𝐴)𝑦)))
75	60, 62, 74	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑔‘⟨𝑥, 𝑦⟩) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑_m (𝑥(Hom ‘𝐴)𝑦)))
76	57, 75	eqeltrid 2865	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑_m (𝑥(Hom ‘𝐴)𝑦)))
77		elmapi 8853	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥𝑔𝑦) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑_m (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
78	76, 77	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
79	78	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
80	79, 42	ffvelcdmd 7077	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑦)‘𝑚) ∈ ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)))
81		df-ov 7415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦𝑔𝑧) = (𝑔‘⟨𝑦, 𝑧⟩)
82		opelxpi 5688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ (Base‘𝐴) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
83	82	adantll 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴)))
84		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑧 ∈ V
85	64, 84	op1std 8000	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑤) = 𝑦)
86	85	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(1^st ‘𝑤)) = (𝑓‘𝑦))
87	64, 84	op2ndd 8001	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑤) = 𝑧)
88	87	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (𝑓‘(2^nd ‘𝑤)) = (𝑓‘𝑧))
89	86, 88	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) = ((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
90		fveq2 6877	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩))
91		df-ov 7415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦(Hom ‘𝐴)𝑧) = ((Hom ‘𝐴)‘⟨𝑦, 𝑧⟩)
92	90, 91	eqtr4di 2814	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → ((Hom ‘𝐴)‘𝑤) = (𝑦(Hom ‘𝐴)𝑧))
93	89, 92	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = ⟨𝑦, 𝑧⟩ → (((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)) = (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑_m (𝑦(Hom ‘𝐴)𝑧)))
94	93	fvixp 8914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)) ∧ ⟨𝑦, 𝑧⟩ ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑_m (𝑦(Hom ‘𝐴)𝑧)))
95	59, 83, 94	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑔‘⟨𝑦, 𝑧⟩) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑_m (𝑦(Hom ‘𝐴)𝑧)))
96	81, 95	eqeltrid 2865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑_m (𝑦(Hom ‘𝐴)𝑧)))
97		elmapi 8853	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦𝑔𝑧) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑_m (𝑦(Hom ‘𝐴)𝑧)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
98	96, 97	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
99	98	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
100	99	ffvelcdmda 7076	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑦𝑔𝑧)‘𝑛) ∈ ((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)))
101	46, 47, 48, 49, 50, 51, 54, 55, 56, 80, 100	comfeqval 17862	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))
102	45, 101	eqeq12d 2777	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
103	102	ralbidva 3184	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
104	103	ralbidva 3184	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
105		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝐵) = (Hom ‘𝐵)
106	22	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Hom_f ‘𝐴) = (Hom_f ‘𝐵))
107		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑥 ∈ (Base‘𝐴))
108		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑦 ∈ (Base‘𝐴))
109	33, 34, 105, 106, 107, 108	homfeqval 17851	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑥(Hom ‘𝐴)𝑦) = (𝑥(Hom ‘𝐵)𝑦))
110		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴))
111	33, 34, 105, 106, 108, 110	homfeqval 17851	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦(Hom ‘𝐴)𝑧) = (𝑦(Hom ‘𝐵)𝑧))
112	111	raleqdv 3320	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
113	109, 112	raleqbidv 3335	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
114	104, 113	bitrd 282	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
115	114	ralbidva 3184	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
116	115	ralbidva 3184	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
117	32, 116	anbi12d 644	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
118	117	ralbidva 3184	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑤))) ↑_m ((Hom ‘𝐴)‘𝑤)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
119	21, 118	sylan2b 606	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
120	119	pm5.32da 590	. . . . . 6 ⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
121		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
122	8	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
123		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶))
124		xp1st 8022	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (1^st ‘𝑧) ∈ (Base‘𝐴))
125	124	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (1^st ‘𝑧) ∈ (Base‘𝐴))
126	123, 125	ffvelcdmd 7077	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(1^st ‘𝑧)) ∈ (Base‘𝐶))
127		xp2nd 8023	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (2^nd ‘𝑧) ∈ (Base‘𝐴))
128	127	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (2^nd ‘𝑧) ∈ (Base‘𝐴))
129	123, 128	ffvelcdmd 7077	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(2^nd ‘𝑧)) ∈ (Base‘𝐶))
130	46, 47, 121, 122, 126, 129	homfeqval 17851	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) = ((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))))
131	3	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Hom_f ‘𝐴) = (Hom_f ‘𝐵))
132	33, 34, 105, 131, 125, 128	homfeqval 17851	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((1^st ‘𝑧)(Hom ‘𝐴)(2^nd ‘𝑧)) = ((1^st ‘𝑧)(Hom ‘𝐵)(2^nd ‘𝑧)))
133		df-ov 7415	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑧)(Hom ‘𝐴)(2^nd ‘𝑧)) = ((Hom ‘𝐴)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
134		df-ov 7415	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘𝑧)(Hom ‘𝐵)(2^nd ‘𝑧)) = ((Hom ‘𝐵)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
135	132, 133, 134	3eqtr3g 2819	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩) = ((Hom ‘𝐵)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
136		1st2nd2 8029	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
137	136	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
138	137	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
139	137	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐵)‘𝑧) = ((Hom ‘𝐵)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
140	135, 138, 139	3eqtr4d 2806	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐵)‘𝑧))
141	130, 140	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) = (((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)))
142	141	ixpeq2dva 8924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)))
143	3	homfeqbas 17850	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
144	143	sqxpeqd 5683	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
145	144	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵)))
146	145	ixpeq1d 8921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)))
147	142, 146	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) = X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)))
148	147	eleq2d 2847	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → (𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) ↔ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧))))
149	148	pm5.32da 590	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)))))
150	8	homfeqbas 17850	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
151	143, 150	feq23d 6696	. . . . . . . . 9 ⊢ (𝜑 → (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ↔ 𝑓:(Base‘𝐵)⟶(Base‘𝐷)))
152	151	anbi1d 643	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)))))
153	149, 152	bitrd 282	. . . . . . 7 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)))))
154	143	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵))
155	154	raleqdv 3320	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
156	154, 155	raleqbidv 3335	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
157	156	anbi2d 642	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
158	143, 157	raleqbidva 3326	. . . . . . 7 ⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
159	153, 158	anbi12d 644	. . . . . 6 ⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
160	120, 159	bitrd 282	. . . . 5 ⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
161		df-3an 1105	. . . . 5 ⊢ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
162		df-3an 1105	. . . . 5 ⊢ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
163	160, 161, 162	3bitr4g 317	. . . 4 ⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
164	13, 163	anbi12d 644	. . 3 ⊢ (𝜑 → (((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))))
165		df-br 5104	. . . . 5 ⊢ (𝑓(𝐴 Func 𝐶)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶))
166		funcrcl 18018	. . . . 5 ⊢ (⟨𝑓, 𝑔⟩ ∈ (𝐴 Func 𝐶) → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
167	165, 166	sylbi 220	. . . 4 ⊢ (𝑓(𝐴 Func 𝐶)𝑔 → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat))
168		eqid 2761	. . . . 5 ⊢ (Id‘𝐴) = (Id‘𝐴)
169		eqid 2761	. . . . 5 ⊢ (Id‘𝐶) = (Id‘𝐶)
170		simpl 488	. . . . 5 ⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐴 ∈ Cat)
171		simpr 490	. . . . 5 ⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat)
172	33, 46, 34, 47, 168, 169, 35, 48, 170, 171	isfunc 18019	. . . 4 ⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → (𝑓(𝐴 Func 𝐶)𝑔 ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
173	167, 172	biadanii 834	. . 3 ⊢ (𝑓(𝐴 Func 𝐶)𝑔 ↔ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
174		df-br 5104	. . . . 5 ⊢ (𝑓(𝐵 Func 𝐷)𝑔 ↔ ⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷))
175		funcrcl 18018	. . . . 5 ⊢ (⟨𝑓, 𝑔⟩ ∈ (𝐵 Func 𝐷) → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
176	174, 175	sylbi 220	. . . 4 ⊢ (𝑓(𝐵 Func 𝐷)𝑔 → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))
177		eqid 2761	. . . . 5 ⊢ (Base‘𝐵) = (Base‘𝐵)
178		eqid 2761	. . . . 5 ⊢ (Base‘𝐷) = (Base‘𝐷)
179		eqid 2761	. . . . 5 ⊢ (Id‘𝐵) = (Id‘𝐵)
180		eqid 2761	. . . . 5 ⊢ (Id‘𝐷) = (Id‘𝐷)
181		simpl 488	. . . . 5 ⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐵 ∈ Cat)
182		simpr 490	. . . . 5 ⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐷 ∈ Cat)
183	177, 178, 105, 121, 179, 180, 36, 49, 181, 182	isfunc 18019	. . . 4 ⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓(𝐵 Func 𝐷)𝑔 ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
184	176, 183	biadanii 834	. . 3 ⊢ (𝑓(𝐵 Func 𝐷)𝑔 ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1^st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2^nd ‘𝑧))) ↑_m ((Hom ‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
185	164, 173, 184	3bitr4g 317	. 2 ⊢ (𝜑 → (𝑓(𝐴 Func 𝐶)𝑔 ↔ 𝑓(𝐵 Func 𝐷)𝑔))
186	1, 2, 185	eqbrrdiv 5770	1 ⊢ (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))

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 3077 ⟨cop 4590 class class class wbr 5103 × cxp 5649 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 1^st c1st 7988 2^nd c2nd 7989 ↑_m cmap 8831 Xcixp 8909 Basecbs 17367 Hom chom 17419 compcco 17420 Catccat 17818 Idccid 17819 Hom_f chomf 17820 comp_fccomf 17821 Func cfunc 18009

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 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-1st 7990 df-2nd 7991 df-map 8833 df-ixp 8910 df-cat 17822 df-cid 17823 df-homf 17824 df-comf 17825 df-func 18013

This theorem is used by: funcres2c 18058 fullpropd 18077 fthpropd 18078 ressffth 18095 natpropd 18134 fucpropd 18135 funcsetcres2 18248 funcoppc2 50195 uppropd 50233 prcofpropd 50431 lanpropd 50667 ranpropd 50668 lmdpropd 50709 cmdpropd 50710

W3C validator