| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . 3
⊢ (𝐴 ×c
𝐶) = (𝐴 ×c 𝐶) | 
| 2 |  | eqid 2736 | . . 3
⊢
(Base‘𝐴) =
(Base‘𝐴) | 
| 3 |  | eqid 2736 | . . 3
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 4 |  | eqid 2736 | . . 3
⊢ (Hom
‘𝐴) = (Hom
‘𝐴) | 
| 5 |  | eqid 2736 | . . 3
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 6 |  | eqid 2736 | . . 3
⊢
(comp‘𝐴) =
(comp‘𝐴) | 
| 7 |  | eqid 2736 | . . 3
⊢
(comp‘𝐶) =
(comp‘𝐶) | 
| 8 |  | xpcpropd.a | . . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 9 |  | xpcpropd.c | . . 3
⊢ (𝜑 → 𝐶 ∈ 𝑉) | 
| 10 |  | eqidd 2737 | . . 3
⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐶)) = ((Base‘𝐴) × (Base‘𝐶))) | 
| 11 | 1, 2, 3 | xpcbas 18224 | . . . . 5
⊢
((Base‘𝐴)
× (Base‘𝐶)) =
(Base‘(𝐴
×c 𝐶)) | 
| 12 |  | eqid 2736 | . . . . 5
⊢ (Hom
‘(𝐴
×c 𝐶)) = (Hom ‘(𝐴 ×c 𝐶)) | 
| 13 | 1, 11, 4, 5, 12 | xpchomfval 18225 | . . . 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 2737 | . . 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 18223 | . 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 2736 | . . 3
⊢ (𝐵 ×c
𝐷) = (𝐵 ×c 𝐷) | 
| 18 |  | eqid 2736 | . . 3
⊢
(Base‘𝐵) =
(Base‘𝐵) | 
| 19 |  | eqid 2736 | . . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 20 |  | eqid 2736 | . . 3
⊢ (Hom
‘𝐵) = (Hom
‘𝐵) | 
| 21 |  | eqid 2736 | . . 3
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 22 |  | eqid 2736 | . . 3
⊢
(comp‘𝐵) =
(comp‘𝐵) | 
| 23 |  | eqid 2736 | . . 3
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 24 |  | xpcpropd.b | . . 3
⊢ (𝜑 → 𝐵 ∈ 𝑉) | 
| 25 |  | xpcpropd.d | . . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) | 
| 26 |  | xpcpropd.1 | . . . . 5
⊢ (𝜑 → (Homf
‘𝐴) =
(Homf ‘𝐵)) | 
| 27 | 26 | homfeqbas 17740 | . . . 4
⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵)) | 
| 28 |  | xpcpropd.3 | . . . . 5
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) | 
| 29 | 28 | homfeqbas 17740 | . . . 4
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) | 
| 30 | 27, 29 | xpeq12d 5715 | . . 3
⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐶)) = ((Base‘𝐵) × (Base‘𝐷))) | 
| 31 | 26 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (Homf
‘𝐴) =
(Homf ‘𝐵)) | 
| 32 |  | xp1st 8047 | . . . . . . . 8
⊢ (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1st
‘𝑢) ∈
(Base‘𝐴)) | 
| 33 | 32 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (1st ‘𝑢) ∈ (Base‘𝐴)) | 
| 34 |  | xp1st 8047 | . . . . . . . 8
⊢ (𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1st
‘𝑣) ∈
(Base‘𝐴)) | 
| 35 | 34 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (1st ‘𝑣) ∈ (Base‘𝐴)) | 
| 36 | 2, 4, 20, 31, 33, 35 | homfeqval 17741 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → ((1st ‘𝑢)(Hom ‘𝐴)(1st ‘𝑣)) = ((1st ‘𝑢)(Hom ‘𝐵)(1st ‘𝑣))) | 
| 37 | 28 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (Homf
‘𝐶) =
(Homf ‘𝐷)) | 
| 38 |  | xp2nd 8048 | . . . . . . . 8
⊢ (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2nd
‘𝑢) ∈
(Base‘𝐶)) | 
| 39 | 38 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (2nd ‘𝑢) ∈ (Base‘𝐶)) | 
| 40 |  | xp2nd 8048 | . . . . . . . 8
⊢ (𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2nd
‘𝑣) ∈
(Base‘𝐶)) | 
| 41 | 40 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (2nd ‘𝑣) ∈ (Base‘𝐶)) | 
| 42 | 3, 5, 21, 37, 39, 41 | homfeqval 17741 | . . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → ((2nd ‘𝑢)(Hom ‘𝐶)(2nd ‘𝑣)) = ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣))) | 
| 43 | 36, 42 | xpeq12d 5715 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (((1st ‘𝑢)(Hom ‘𝐴)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐶)(2nd ‘𝑣))) = (((1st ‘𝑢)(Hom ‘𝐵)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝐷)(2nd ‘𝑣)))) | 
| 44 | 43 | mpoeq3dva 7511 | . . . 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 2788 | . . 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 8047 | . . . . . . . . . . 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 8047 | . . . . . . . . . 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 8048 | . . . . . . . . . . 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 8047 | . . . . . . . . . 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 8047 | . . . . . . . . . 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 8054 | . . . . . . . . . . . . . . 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 6909 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → ((Hom ‘(𝐴 ×c 𝐶))‘𝑥) = ((Hom ‘(𝐴 ×c 𝐶))‘〈(1st
‘𝑥), (2nd
‘𝑥)〉)) | 
| 65 |  | df-ov 7435 | . . . . . . . . . . . . 13
⊢
((1st ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))(2nd ‘𝑥)) = ((Hom ‘(𝐴 ×c
𝐶))‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 66 | 64, 65 | eqtr4di 2794 | . . . . . . . . . . . 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 18226 | . . . . . . . . . . . 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 2776 | . . . . . . . . . . 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 2842 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑓 ∈ (((1st
‘(1st ‘𝑥))(Hom ‘𝐴)(1st ‘(2nd
‘𝑥))) ×
((2nd ‘(1st ‘𝑥))(Hom ‘𝐶)(2nd ‘(2nd
‘𝑥))))) | 
| 70 |  | xp1st 8047 | . . . . . . . . . 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 18226 | . . . . . . . . . . 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 2842 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘(𝐴 ×c 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×c 𝐶))‘𝑥)) → 𝑔 ∈ (((1st
‘(2nd ‘𝑥))(Hom ‘𝐴)(1st ‘𝑦)) × ((2nd
‘(2nd ‘𝑥))(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 75 |  | xp1st 8047 | . . . . . . . . . 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 17752 | . . . . . . . 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 8048 | . . . . . . . . . 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 8048 | . . . . . . . . . 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 8048 | . . . . . . . . . 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 8048 | . . . . . . . . . 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 8048 | . . . . . . . . . 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 17752 | . . . . . . . 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 4880 | . . . . . . 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 7511 | . . . . 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 7511 | . . 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 18223 | . 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 2779 | 1
⊢ (𝜑 → (𝐴 ×c 𝐶) = (𝐵 ×c 𝐷)) |