Step | Hyp | Ref
| Expression |
1 | | eqid 2609 |
. . 3
⊢ (𝐴 ×_{c}
𝐶) = (𝐴 ×_{c} 𝐶) |
2 | | eqid 2609 |
. . 3
⊢
(Base‘𝐴) =
(Base‘𝐴) |
3 | | eqid 2609 |
. . 3
⊢
(Base‘𝐶) =
(Base‘𝐶) |
4 | | eqid 2609 |
. . 3
⊢ (Hom
‘𝐴) = (Hom
‘𝐴) |
5 | | eqid 2609 |
. . 3
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
6 | | eqid 2609 |
. . 3
⊢
(comp‘𝐴) =
(comp‘𝐴) |
7 | | eqid 2609 |
. . 3
⊢
(comp‘𝐶) =
(comp‘𝐶) |
8 | | xpcpropd.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
9 | | xpcpropd.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
10 | | eqidd 2610 |
. . 3
⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐶)) = ((Base‘𝐴) × (Base‘𝐶))) |
11 | 1, 2, 3 | xpcbas 16587 |
. . . . 5
⊢
((Base‘𝐴)
× (Base‘𝐶)) =
(Base‘(𝐴
×_{c} 𝐶)) |
12 | | eqid 2609 |
. . . . 5
⊢ (Hom
‘(𝐴
×_{c} 𝐶)) = (Hom ‘(𝐴 ×_{c} 𝐶)) |
13 | 1, 11, 4, 5, 12 | xpchomfval 16588 |
. . . 4
⊢ (Hom
‘(𝐴
×_{c} 𝐶)) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝐴)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐶)(2^{nd} ‘𝑣)))) |
14 | 13 | a1i 11 |
. . 3
⊢ (𝜑 → (Hom ‘(𝐴 ×_{c}
𝐶)) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝐴)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐶)(2^{nd} ‘𝑣))))) |
15 | | eqidd 2610 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
14, 15 | xpcval 16586 |
. 2
⊢ (𝜑 → (𝐴 ×_{c} 𝐶) = {⟨(Base‘ndx),
((Base‘𝐴) ×
(Base‘𝐶))⟩,
⟨(Hom ‘ndx), (Hom ‘(𝐴 ×_{c} 𝐶))⟩,
⟨(comp‘ndx), (𝑥
∈ (((Base‘𝐴)
× (Base‘𝐶))
× ((Base‘𝐴)
× (Base‘𝐶))),
𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩}) |
17 | | eqid 2609 |
. . 3
⊢ (𝐵 ×_{c}
𝐷) = (𝐵 ×_{c} 𝐷) |
18 | | eqid 2609 |
. . 3
⊢
(Base‘𝐵) =
(Base‘𝐵) |
19 | | eqid 2609 |
. . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) |
20 | | eqid 2609 |
. . 3
⊢ (Hom
‘𝐵) = (Hom
‘𝐵) |
21 | | eqid 2609 |
. . 3
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
22 | | eqid 2609 |
. . 3
⊢
(comp‘𝐵) =
(comp‘𝐵) |
23 | | eqid 2609 |
. . 3
⊢
(comp‘𝐷) =
(comp‘𝐷) |
24 | | xpcpropd.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
25 | | xpcpropd.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
26 | | xpcpropd.1 |
. . . . 5
⊢ (𝜑 → (Hom_{f}
‘𝐴) =
(Hom_{f} ‘𝐵)) |
27 | 26 | homfeqbas 16125 |
. . . 4
⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵)) |
28 | | xpcpropd.3 |
. . . . 5
⊢ (𝜑 → (Hom_{f}
‘𝐶) =
(Hom_{f} ‘𝐷)) |
29 | 28 | homfeqbas 16125 |
. . . 4
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
30 | 27, 29 | xpeq12d 5054 |
. . 3
⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐶)) = ((Base‘𝐵) × (Base‘𝐷))) |
31 | 26 | 3ad2ant1 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (Hom_{f}
‘𝐴) =
(Hom_{f} ‘𝐵)) |
32 | | xp1st 7066 |
. . . . . . . 8
⊢ (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1^{st}
‘𝑢) ∈
(Base‘𝐴)) |
33 | 32 | 3ad2ant2 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (1^{st} ‘𝑢) ∈ (Base‘𝐴)) |
34 | | xp1st 7066 |
. . . . . . . 8
⊢ (𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1^{st}
‘𝑣) ∈
(Base‘𝐴)) |
35 | 34 | 3ad2ant3 1076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (1^{st} ‘𝑣) ∈ (Base‘𝐴)) |
36 | 2, 4, 20, 31, 33, 35 | homfeqval 16126 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → ((1^{st} ‘𝑢)(Hom ‘𝐴)(1^{st} ‘𝑣)) = ((1^{st} ‘𝑢)(Hom ‘𝐵)(1^{st} ‘𝑣))) |
37 | 28 | 3ad2ant1 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (Hom_{f}
‘𝐶) =
(Hom_{f} ‘𝐷)) |
38 | | xp2nd 7067 |
. . . . . . . 8
⊢ (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2^{nd}
‘𝑢) ∈
(Base‘𝐶)) |
39 | 38 | 3ad2ant2 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (2^{nd} ‘𝑢) ∈ (Base‘𝐶)) |
40 | | xp2nd 7067 |
. . . . . . . 8
⊢ (𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2^{nd}
‘𝑣) ∈
(Base‘𝐶)) |
41 | 40 | 3ad2ant3 1076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (2^{nd} ‘𝑣) ∈ (Base‘𝐶)) |
42 | 3, 5, 21, 37, 39, 41 | homfeqval 16126 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → ((2^{nd} ‘𝑢)(Hom ‘𝐶)(2^{nd} ‘𝑣)) = ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))) |
43 | 36, 42 | xpeq12d 5054 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)) ∧ 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (((1^{st} ‘𝑢)(Hom ‘𝐴)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐶)(2^{nd} ‘𝑣))) = (((1^{st} ‘𝑢)(Hom ‘𝐵)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣)))) |
44 | 43 | mpt2eq3dva 6595 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝐴)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐶)(2^{nd} ‘𝑣)))) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝐵)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))))) |
45 | 13, 44 | syl5eq 2655 |
. . 3
⊢ (𝜑 → (Hom ‘(𝐴 ×_{c}
𝐶)) = (𝑢 ∈ ((Base‘𝐴) × (Base‘𝐶)), 𝑣 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝐵)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝐷)(2^{nd} ‘𝑣))))) |
46 | 26 | ad4antr 763 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (Hom_{f}
‘𝐴) =
(Hom_{f} ‘𝐵)) |
47 | | xpcpropd.2 |
. . . . . . . . . 10
⊢ (𝜑 →
(comp_{f}‘𝐴) = (comp_{f}‘𝐵)) |
48 | 47 | ad4antr 763 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) →
(comp_{f}‘𝐴) = (comp_{f}‘𝐵)) |
49 | | simp-4r 802 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) |
50 | | xp1st 7066 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) → (1^{st}
‘𝑥) ∈
((Base‘𝐴) ×
(Base‘𝐶))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (1^{st} ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶))) |
52 | | xp1st 7066 |
. . . . . . . . . 10
⊢
((1^{st} ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1^{st}
‘(1^{st} ‘𝑥)) ∈ (Base‘𝐴)) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (1^{st}
‘(1^{st} ‘𝑥)) ∈ (Base‘𝐴)) |
54 | | xp2nd 7067 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) → (2^{nd}
‘𝑥) ∈
((Base‘𝐴) ×
(Base‘𝐶))) |
55 | 49, 54 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (2^{nd} ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶))) |
56 | | xp1st 7066 |
. . . . . . . . . 10
⊢
((2^{nd} ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1^{st}
‘(2^{nd} ‘𝑥)) ∈ (Base‘𝐴)) |
57 | 55, 56 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (1^{st}
‘(2^{nd} ‘𝑥)) ∈ (Base‘𝐴)) |
58 | | simpllr 794 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) |
59 | | xp1st 7066 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (1^{st}
‘𝑦) ∈
(Base‘𝐴)) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (1^{st} ‘𝑦) ∈ (Base‘𝐴)) |
61 | | simpr 475 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) |
62 | | 1st2nd2 7073 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
63 | 49, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
64 | 63 | fveq2d 6092 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) = ((Hom ‘(𝐴 ×_{c} 𝐶))‘⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)) |
65 | | df-ov 6530 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))(2^{nd} ‘𝑥)) = ((Hom ‘(𝐴 ×_{c}
𝐶))‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
66 | 64, 65 | syl6eqr 2661 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) = ((1^{st} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))(2^{nd} ‘𝑥))) |
67 | 1, 11, 4, 5, 12, 51, 55 | xpchom 16589 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ((1^{st} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))(2^{nd} ‘𝑥)) = (((1^{st}
‘(1^{st} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘(2^{nd}
‘𝑥))) ×
((2^{nd} ‘(1^{st} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘(2^{nd}
‘𝑥))))) |
68 | 66, 67 | eqtrd 2643 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) = (((1^{st} ‘(1^{st}
‘𝑥))(Hom ‘𝐴)(1^{st}
‘(2^{nd} ‘𝑥))) × ((2^{nd}
‘(1^{st} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘(2^{nd}
‘𝑥))))) |
69 | 61, 68 | eleqtrd 2689 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → 𝑓 ∈ (((1^{st}
‘(1^{st} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘(2^{nd}
‘𝑥))) ×
((2^{nd} ‘(1^{st} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘(2^{nd}
‘𝑥))))) |
70 | | xp1st 7066 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (((1^{st}
‘(1^{st} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘(2^{nd}
‘𝑥))) ×
((2^{nd} ‘(1^{st} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘(2^{nd}
‘𝑥)))) →
(1^{st} ‘𝑓)
∈ ((1^{st} ‘(1^{st} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘(2^{nd}
‘𝑥)))) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (1^{st} ‘𝑓) ∈ ((1^{st}
‘(1^{st} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘(2^{nd}
‘𝑥)))) |
72 | | simplr 787 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) |
73 | 1, 11, 4, 5, 12, 55, 58 | xpchom 16589 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦) = (((1^{st} ‘(2^{nd}
‘𝑥))(Hom ‘𝐴)(1^{st} ‘𝑦)) × ((2^{nd}
‘(2^{nd} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
74 | 72, 73 | eleqtrd 2689 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → 𝑔 ∈ (((1^{st}
‘(2^{nd} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘𝑦)) × ((2^{nd}
‘(2^{nd} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
75 | | xp1st 7066 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (((1^{st}
‘(2^{nd} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘𝑦)) × ((2^{nd}
‘(2^{nd} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘𝑦))) → (1^{st} ‘𝑔) ∈ ((1^{st}
‘(2^{nd} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘𝑦))) |
76 | 74, 75 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (1^{st} ‘𝑔) ∈ ((1^{st}
‘(2^{nd} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘𝑦))) |
77 | 2, 4, 6, 22, 46, 48, 53, 57, 60, 71, 76 | comfeqval 16137 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) = ((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐵)(1^{st} ‘𝑦))(1^{st} ‘𝑓))) |
78 | 28 | ad4antr 763 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (Hom_{f}
‘𝐶) =
(Hom_{f} ‘𝐷)) |
79 | | xpcpropd.4 |
. . . . . . . . . 10
⊢ (𝜑 →
(comp_{f}‘𝐶) = (comp_{f}‘𝐷)) |
80 | 79 | ad4antr 763 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) →
(comp_{f}‘𝐶) = (comp_{f}‘𝐷)) |
81 | | xp2nd 7067 |
. . . . . . . . . 10
⊢
((1^{st} ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2^{nd}
‘(1^{st} ‘𝑥)) ∈ (Base‘𝐶)) |
82 | 51, 81 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (2^{nd}
‘(1^{st} ‘𝑥)) ∈ (Base‘𝐶)) |
83 | | xp2nd 7067 |
. . . . . . . . . 10
⊢
((2^{nd} ‘𝑥) ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2^{nd}
‘(2^{nd} ‘𝑥)) ∈ (Base‘𝐶)) |
84 | 55, 83 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (2^{nd}
‘(2^{nd} ‘𝑥)) ∈ (Base‘𝐶)) |
85 | | xp2nd 7067 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) → (2^{nd}
‘𝑦) ∈
(Base‘𝐶)) |
86 | 58, 85 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
87 | | xp2nd 7067 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (((1^{st}
‘(1^{st} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘(2^{nd}
‘𝑥))) ×
((2^{nd} ‘(1^{st} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘(2^{nd}
‘𝑥)))) →
(2^{nd} ‘𝑓)
∈ ((2^{nd} ‘(1^{st} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘(2^{nd}
‘𝑥)))) |
88 | 69, 87 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (2^{nd} ‘𝑓) ∈ ((2^{nd}
‘(1^{st} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘(2^{nd}
‘𝑥)))) |
89 | | xp2nd 7067 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (((1^{st}
‘(2^{nd} ‘𝑥))(Hom ‘𝐴)(1^{st} ‘𝑦)) × ((2^{nd}
‘(2^{nd} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘𝑦))) → (2^{nd} ‘𝑔) ∈ ((2^{nd}
‘(2^{nd} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
90 | 74, 89 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → (2^{nd} ‘𝑔) ∈ ((2^{nd}
‘(2^{nd} ‘𝑥))(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
91 | 3, 5, 7, 23, 78, 80, 82, 84, 86, 88, 90 | comfeqval 16137 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) = ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐷)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))) |
92 | 77, 91 | opeq12d 4342 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦)) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ = ⟨((1^{st}
‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐵)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐷)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) |
93 | 92 | 3impa 1250 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦) ∧ 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥)) → ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ = ⟨((1^{st}
‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐵)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐷)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) |
94 | 93 | mpt2eq3dva 6595 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶)))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) = (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐵)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐷)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |
95 | 94 | 3impa 1250 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))) ∧ 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶))) → (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) = (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐵)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐷)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |
96 | 95 | mpt2eq3dva 6595 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = (𝑥 ∈ (((Base‘𝐴) × (Base‘𝐶)) × ((Base‘𝐴) × (Base‘𝐶))), 𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐵)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐷)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
97 | 17, 18, 19, 20, 21, 22, 23, 24, 25, 30, 45, 96 | xpcval 16586 |
. 2
⊢ (𝜑 → (𝐵 ×_{c} 𝐷) = {⟨(Base‘ndx),
((Base‘𝐴) ×
(Base‘𝐶))⟩,
⟨(Hom ‘ndx), (Hom ‘(𝐴 ×_{c} 𝐶))⟩,
⟨(comp‘ndx), (𝑥
∈ (((Base‘𝐴)
× (Base‘𝐶))
× ((Base‘𝐴)
× (Base‘𝐶))),
𝑦 ∈ ((Base‘𝐴) × (Base‘𝐶)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘(𝐴 ×_{c} 𝐶))𝑦), 𝑓 ∈ ((Hom ‘(𝐴 ×_{c} 𝐶))‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐴)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝐶)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩}) |
98 | 16, 97 | eqtr4d 2646 |
1
⊢ (𝜑 → (𝐴 ×_{c} 𝐶) = (𝐵 ×_{c} 𝐷)) |