Theorem xpcpropd 18207

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

Hypotheses

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

Assertion

Ref	Expression
xpcpropd	⊢ (𝜑 → (𝐴 ×c 𝐶) = (𝐵 ×c 𝐷))

Proof of Theorem xpcpropd

Dummy variables 𝑓 𝑔 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2734	. . 3 ⊢ (𝐴 ×c 𝐶) = (𝐴 ×c 𝐶)
2		eqid 2734	. . 3 ⊢ (Base‘𝐴) = (Base‘𝐴)
3		eqid 2734	. . 3 ⊢ (Base‘𝐶) = (Base‘𝐶)
4		eqid 2734	. . 3 ⊢ (Hom ‘𝐴) = (Hom ‘𝐴)
5		eqid 2734	. . 3 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2734	. . 3 ⊢ (comp‘𝐴) = (comp‘𝐴)
7		eqid 2734	. . 3 ⊢ (comp‘𝐶) = (comp‘𝐶)
8		xpcpropd.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
9		xpcpropd.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
10		eqidd 2735	. . 3 ⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐶)) = ((Base‘𝐴) × (Base‘𝐶)))
11	1, 2, 3	xpcbas 18177	. . . . 5 ⊢ ((Base‘𝐴) × (Base‘𝐶)) = (Base‘(𝐴 ×c 𝐶))
12		eqid 2734	. . . . 5 ⊢ (Hom ‘(𝐴 ×c 𝐶)) = (Hom ‘(𝐴 ×c 𝐶))
13	1, 11, 4, 5, 12	xpchomfval 18178	. . . 4 ⊢ (Hom ‘(𝐴 ×c 𝐶)) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1st ‘𝑢)(Hom ‘𝐴)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐶)(2nd ‘𝑣))))
14	13	a1i 11	. . 3 ⊢ (𝜑 → (Hom ‘(𝐴 ×c 𝐶)) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1st ‘𝑢)(Hom ‘𝐴)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐶)(2nd ‘𝑣)))))
15		eqidd 2735	. . 3 ⊢ (𝜑 → (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩)) = (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩)))
16	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 14, 15	xpcval 18176	. 2 ⊢ (𝜑 → (𝐴 ×c 𝐶) = {⟨(Base‘ndx), ((Base‘𝐴) × (Base‘𝐶))⟩, ⟨(Hom ‘ndx), (Hom ‘(𝐴 ×c 𝐶))⟩, ⟨(comp‘ndx), (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩))⟩})
17		eqid 2734	. . 3 ⊢ (𝐵 ×c 𝐷) = (𝐵 ×c 𝐷)
18		eqid 2734	. . 3 ⊢ (Base‘𝐵) = (Base‘𝐵)
19		eqid 2734	. . 3 ⊢ (Base‘𝐷) = (Base‘𝐷)
20		eqid 2734	. . 3 ⊢ (Hom ‘𝐵) = (Hom ‘𝐵)
21		eqid 2734	. . 3 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
22		eqid 2734	. . 3 ⊢ (comp‘𝐵) = (comp‘𝐵)
23		eqid 2734	. . 3 ⊢ (comp‘𝐷) = (comp‘𝐷)
24		xpcpropd.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
25		xpcpropd.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
26		xpcpropd.1	. . . . 5 ⊢ (𝜑 → (Homf ‘𝐴) = (Homf ‘𝐵))
27	26	homfeqbas 17695	. . . 4 ⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵))
28		xpcpropd.3	. . . . 5 ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))
29	28	homfeqbas 17695	. . . 4 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
30	27, 29	xpeq12d 5683	. . 3 ⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐶)) = ((Base‘𝐵) × (Base‘𝐷)))
31	26	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (Homf ‘𝐴) = (Homf ‘𝐵))
32		xp1st 8015	. . . . . . . 8 ⊢ (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1st ‘𝑢) ∈ (Base‘𝐴))
33	32	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (1st ‘𝑢) ∈ (Base‘𝐴))
34		xp1st 8015	. . . . . . . 8 ⊢ (𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1st ‘𝑣) ∈ (Base‘𝐴))
35	34	3ad2ant3 1135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (1st ‘𝑣) ∈ (Base‘𝐴))
36	2, 4, 20, 31, 33, 35	homfeqval 17696	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → ((1st ‘𝑢)(Hom ‘𝐴)(1st ‘𝑣)) = ((1st ‘𝑢)(Hom ‘𝐵)(1st ‘𝑣)))
37	28	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (Homf ‘𝐶) = (Homf ‘𝐷))
38		xp2nd 8016	. . . . . . . 8 ⊢ (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2nd ‘𝑢) ∈ (Base‘𝐶))
39	38	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (2nd ‘𝑢) ∈ (Base‘𝐶))
40		xp2nd 8016	. . . . . . . 8 ⊢ (𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2nd ‘𝑣) ∈ (Base‘𝐶))
41	40	3ad2ant3 1135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (2nd ‘𝑣) ∈ (Base‘𝐶))
42	3, 5, 21, 37, 39, 41	homfeqval 17696	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → ((2nd ‘𝑢)(Hom ‘𝐶)(2nd ‘𝑣)) = ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))
43	36, 42	xpeq12d 5683	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (((1st ‘𝑢)(Hom ‘𝐴)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐶)(2nd ‘𝑣))) = (((1st ‘𝑢)(Hom ‘𝐵)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))))
44	43	mpoeq3dva 7479	. . . 4 ⊢ (𝜑 → (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1st ‘𝑢)(Hom ‘𝐴)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐶)(2nd ‘𝑣)))) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1st ‘𝑢)(Hom ‘𝐵)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))))
45	13, 44	eqtrid 2781	. . 3 ⊢ (𝜑 → (Hom ‘(𝐴 ×c 𝐶)) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1st ‘𝑢)(Hom ‘𝐵)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))))
46	26	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (Homf ‘𝐴) = (Homf ‘𝐵))
47		xpcpropd.2	. . . . . . . . . 10 ⊢ (𝜑 → (compf‘𝐴) = (compf‘𝐵))
48	47	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (compf‘𝐴) = (compf‘𝐵))
49		simp-4r 783	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))))
50		xp1st 8015	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) → (1st ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)))
51	49, 50	syl 17	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (1st ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)))
52		xp1st 8015	. . . . . . . . . 10 ⊢ ((1st ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1st ‘(1st ‘𝑥)) ∈ (Base‘𝐴))
53	51, 52	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (1st ‘(1st ‘𝑥)) ∈ (Base‘𝐴))
54		xp2nd 8016	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) → (2nd ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)))
55	49, 54	syl 17	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (2nd ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)))
56		xp1st 8015	. . . . . . . . . 10 ⊢ ((2nd ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1st ‘(2nd ‘𝑥)) ∈ (Base‘𝐴))
57	55, 56	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (1st ‘(2nd ‘𝑥)) ∈ (Base‘𝐴))
58		simpllr 775	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)))
59		xp1st 8015	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1st ‘𝑦) ∈ (Base‘𝐴))
60	58, 59	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (1st ‘𝑦) ∈ (Base‘𝐴))
61		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥))
62		1st2nd2 8022	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
63	49, 62	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
64	63	fveq2d 6877	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) = ((Hom ‘(𝐴 ×c 𝐶))‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
65		df-ov 7403	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))(2nd ‘𝑥)) = ((Hom ‘(𝐴 ×c 𝐶))‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
66	64, 65	eqtr4di 2787	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) = ((1st ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))(2nd ‘𝑥)))
67	1, 11, 4, 5, 12, 51, 55	xpchom 18179	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((1st ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))(2nd ‘𝑥)) = (((1st ‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd ‘𝑥))) × ((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd ‘𝑥)))))
68	66, 67	eqtrd 2769	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) = (((1st ‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd ‘𝑥))) × ((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd ‘𝑥)))))
69	61, 68	eleqtrd 2835	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑓 ∈ (((1st ‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd ‘𝑥))) × ((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd ‘𝑥)))))
70		xp1st 8015	. . . . . . . . . 10 ⊢ (𝑓 ∈ (((1st ‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd ‘𝑥))) × ((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd ‘𝑥)))) → (1st ‘𝑓) ∈ ((1st ‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd ‘𝑥))))
71	69, 70	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (1st ‘𝑓) ∈ ((1st ‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd ‘𝑥))))
72		simplr 768	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦))
73	1, 11, 4, 5, 12, 55, 58	xpchom 18179	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦) = (((1st ‘(2nd ‘𝑥))(Hom ‘𝐴)(1st ‘𝑦)) × ((2nd ‘(2nd ‘𝑥))(Hom ‘𝐶)(2nd ‘𝑦))))
74	72, 73	eleqtrd 2835	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑔 ∈ (((1st ‘(2nd ‘𝑥))(Hom ‘𝐴)(1st ‘𝑦)) × ((2nd ‘(2nd ‘𝑥))(Hom ‘𝐶)(2nd ‘𝑦))))
75		xp1st 8015	. . . . . . . . . 10 ⊢ (𝑔 ∈ (((1st ‘(2nd ‘𝑥))(Hom ‘𝐴)(1st ‘𝑦)) × ((2nd ‘(2nd ‘𝑥))(Hom ‘𝐶)(2nd ‘𝑦))) → (1st ‘𝑔) ∈ ((1st ‘(2nd ‘𝑥))(Hom ‘𝐴)(1st ‘𝑦)))
76	74, 75	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (1st ‘𝑔) ∈ ((1st ‘(2nd ‘𝑥))(Hom ‘𝐴)(1st ‘𝑦)))
77	2, 4, 6, 22, 46, 48, 53, 57, 60, 71, 76	comfeqval 17707	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)) = ((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐵)(1st ‘𝑦))(1st ‘𝑓)))
78	28	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (Homf ‘𝐶) = (Homf ‘𝐷))
79		xpcpropd.4	. . . . . . . . . 10 ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))
80	79	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (compf‘𝐶) = (compf‘𝐷))
81		xp2nd 8016	. . . . . . . . . 10 ⊢ ((1st ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2nd ‘(1st ‘𝑥)) ∈ (Base‘𝐶))
82	51, 81	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (2nd ‘(1st ‘𝑥)) ∈ (Base‘𝐶))
83		xp2nd 8016	. . . . . . . . . 10 ⊢ ((2nd ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2nd ‘(2nd ‘𝑥)) ∈ (Base‘𝐶))
84	55, 83	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (2nd ‘(2nd ‘𝑥)) ∈ (Base‘𝐶))
85		xp2nd 8016	. . . . . . . . . 10 ⊢ (𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2nd ‘𝑦) ∈ (Base‘𝐶))
86	58, 85	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (2nd ‘𝑦) ∈ (Base‘𝐶))
87		xp2nd 8016	. . . . . . . . . 10 ⊢ (𝑓 ∈ (((1st ‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd ‘𝑥))) × ((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd ‘𝑥)))) → (2nd ‘𝑓) ∈ ((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd ‘𝑥))))
88	69, 87	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (2nd ‘𝑓) ∈ ((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd ‘𝑥))))
89		xp2nd 8016	. . . . . . . . . 10 ⊢ (𝑔 ∈ (((1st ‘(2nd ‘𝑥))(Hom ‘𝐴)(1st ‘𝑦)) × ((2nd ‘(2nd ‘𝑥))(Hom ‘𝐶)(2nd ‘𝑦))) → (2nd ‘𝑔) ∈ ((2nd ‘(2nd ‘𝑥))(Hom ‘𝐶)(2nd ‘𝑦)))
90	74, 89	syl 17	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → (2nd ‘𝑔) ∈ ((2nd ‘(2nd ‘𝑥))(Hom ‘𝐶)(2nd ‘𝑦)))
91	3, 5, 7, 23, 78, 80, 82, 84, 86, 88, 90	comfeqval 17707	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓)) = ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓)))
92	77, 91	opeq12d 4855	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩ = ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐵)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))⟩)
93	92	3impa 1109	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩ = ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐵)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))⟩)
94	93	mpoeq3dva 7479	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩) = (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐵)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))⟩))
95	94	3impa 1109	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩) = (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐵)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))⟩))
96	95	mpoeq3dva 7479	. . 3 ⊢ (𝜑 → (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩)) = (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐵)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐷)(2nd ‘𝑦))(2nd ‘𝑓))⟩)))
97	17, 18, 19, 20, 21, 22, 23, 24, 25, 30, 45, 96	xpcval 18176	. 2 ⊢ (𝜑 → (𝐵 ×c 𝐷) = {⟨(Base‘ndx), ((Base‘𝐴) × (Base‘𝐶))⟩, ⟨(Hom ‘ndx), (Hom ‘(𝐴 ×c 𝐶))⟩, ⟨(comp‘ndx), (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) ↦ ⟨((1st ‘𝑔)(⟨(1st ‘(1st ‘𝑥)), (1st ‘(2nd ‘𝑥))⟩(comp‘𝐴)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd ‘𝑥))⟩(comp‘𝐶)(2nd ‘𝑦))(2nd ‘𝑓))⟩))⟩})
98	16, 97	eqtr4d 2772	1 ⊢ (𝜑 → (𝐴 ×c 𝐶) = (𝐵 ×c 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  {ctp 4603  ⟨cop 4605   × cxp 5650  ‘cfv 6528  (class class class)co 7400   ∈ cmpo 7402  1^st c1st 7981  2^nd c2nd 7982  ndxcnx 17199  Basecbs 17215  Hom chom 17269  compcco 17270  Hom_f chomf 17665  comp_fccomf 17666   ×_c cxpc 18167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5247  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-cnex 11178  ax-resscn 11179  ax-1cn 11180  ax-icn 11181  ax-addcl 11182  ax-addrcl 11183  ax-mulcl 11184  ax-mulrcl 11185  ax-mulcom 11186  ax-addass 11187  ax-mulass 11188  ax-distr 11189  ax-i2m1 11190  ax-1ne0 11191  ax-1rid 11192  ax-rnegex 11193  ax-rrecex 11194  ax-cnre 11195  ax-pre-lttri 11196  ax-pre-lttrn 11197  ax-pre-ltadd 11198  ax-pre-mulgt0 11199

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-tp 4604  df-op 4606  df-uni 4882  df-iun 4967  df-br 5118  df-opab 5180  df-mpt 5200  df-tr 5228  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6288  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7857  df-1st 7983  df-2nd 7984  df-frecs 8275  df-wrecs 8306  df-recs 8380  df-rdg 8419  df-1o 8475  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-fin 8958  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268  df-sub 11461  df-neg 11462  df-nn 12234  df-2 12296  df-3 12297  df-4 12298  df-5 12299  df-6 12300  df-7 12301  df-8 12302  df-9 12303  df-n0 12495  df-z 12582  df-dec 12702  df-uz 12846  df-fz 13515  df-struct 17153  df-slot 17188  df-ndx 17200  df-base 17216  df-hom 17282  df-cco 17283  df-homf 17669  df-comf 17670  df-xpc 18171

This theorem is referenced by:  curfpropd  18232  oppchofcl  18259