Step | Hyp | Ref
| Expression |
1 | | relfunc 17588 |
. 2
⊢ Rel
(𝐴 Func 𝐶) |
2 | | relfunc 17588 |
. 2
⊢ Rel
(𝐵 Func 𝐷) |
3 | | funcpropd.1 |
. . . . . 6
⊢ (𝜑 → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
4 | | funcpropd.2 |
. . . . . 6
⊢ (𝜑 →
(compf‘𝐴) = (compf‘𝐵)) |
5 | | funcpropd.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
6 | | funcpropd.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
7 | 3, 4, 5, 6 | catpropd 17429 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ Cat ↔ 𝐵 ∈ Cat)) |
8 | | funcpropd.3 |
. . . . . 6
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
9 | | funcpropd.4 |
. . . . . 6
⊢ (𝜑 →
(compf‘𝐶) = (compf‘𝐷)) |
10 | | funcpropd.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
11 | | funcpropd.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
12 | 8, 9, 10, 11 | catpropd 17429 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat)) |
13 | 7, 12 | anbi12d 631 |
. . . 4
⊢ (𝜑 → ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ↔ (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat))) |
14 | | 2fveq3 6776 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → (𝑓‘(1st ‘𝑧)) = (𝑓‘(1st ‘𝑤))) |
15 | | 2fveq3 6776 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → (𝑓‘(2nd ‘𝑧)) = (𝑓‘(2nd ‘𝑤))) |
16 | 14, 15 | oveq12d 7290 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → ((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤)))) |
17 | | fveq2 6771 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘𝑤)) |
18 | 16, 17 | oveq12d 7290 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → (((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) = (((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤))) |
19 | 18 | cbvixpv 8695 |
. . . . . . . . . 10
⊢ X𝑧 ∈
((Base‘𝐴) ×
(Base‘𝐴))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) = X𝑤 ∈
((Base‘𝐴) ×
(Base‘𝐴))(((𝑓‘(1st
‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)) |
20 | 19 | eleq2i 2832 |
. . . . . . . . 9
⊢ (𝑔 ∈ X𝑧 ∈
((Base‘𝐴) ×
(Base‘𝐴))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) ↔ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤))) |
21 | 20 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) |
22 | 3 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
23 | 4 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) →
(compf‘𝐴) = (compf‘𝐵)) |
24 | 5 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐴 ∈ 𝑉) |
25 | 6 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝐵 ∈ 𝑉) |
26 | 22, 23, 24, 25 | cidpropd 17430 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐴) = (Id‘𝐵)) |
27 | 26 | fveq1d 6773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐴)‘𝑥) = ((Id‘𝐵)‘𝑥)) |
28 | 27 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥))) |
29 | 8, 9, 10, 11 | cidpropd 17430 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷)) |
30 | 29 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Id‘𝐶) = (Id‘𝐷)) |
31 | 30 | fveq1d 6773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((Id‘𝐶)‘(𝑓‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥))) |
32 | 28, 31 | eqeq12d 2756 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ↔ ((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)))) |
33 | | eqid 2740 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘𝐴) =
(Base‘𝐴) |
34 | | eqid 2740 |
. . . . . . . . . . . . . . . . . 18
⊢ (Hom
‘𝐴) = (Hom
‘𝐴) |
35 | | eqid 2740 |
. . . . . . . . . . . . . . . . . 18
⊢
(comp‘𝐴) =
(comp‘𝐴) |
36 | | eqid 2740 |
. . . . . . . . . . . . . . . . . 18
⊢
(comp‘𝐵) =
(comp‘𝐵) |
37 | 3 | ad6antr 733 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
38 | 4 | ad6antr 733 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) →
(compf‘𝐴) = (compf‘𝐵)) |
39 | | simp-5r 783 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑥 ∈ (Base‘𝐴)) |
40 | | simp-4r 781 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑦 ∈ (Base‘𝐴)) |
41 | | simpllr 773 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑧 ∈ (Base‘𝐴)) |
42 | | simplr 766 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) |
43 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) |
44 | 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43 | comfeqval 17428 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚) = (𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) |
45 | 44 | fveq2d 6775 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚))) |
46 | | eqid 2740 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘𝐶) =
(Base‘𝐶) |
47 | | eqid 2740 |
. . . . . . . . . . . . . . . . 17
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
48 | | eqid 2740 |
. . . . . . . . . . . . . . . . 17
⊢
(comp‘𝐶) =
(comp‘𝐶) |
49 | | eqid 2740 |
. . . . . . . . . . . . . . . . 17
⊢
(comp‘𝐷) =
(comp‘𝐷) |
50 | 8 | ad6antr 733 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
51 | 9 | ad6antr 733 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) →
(compf‘𝐶) = (compf‘𝐷)) |
52 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) |
53 | 52 | ad5antr 731 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) |
54 | 53, 39 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑥) ∈ (Base‘𝐶)) |
55 | 53, 40 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑦) ∈ (Base‘𝐶)) |
56 | 53, 41 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑓‘𝑧) ∈ (Base‘𝐶)) |
57 | | df-ov 7275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑔𝑦) = (𝑔‘〈𝑥, 𝑦〉) |
58 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤))) |
59 | 58 | ad5ant12 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤))) |
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤))) |
61 | | opelxpi 5627 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ (Base‘𝐴) ∧ 𝑦 ∈ (Base‘𝐴)) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐴) × (Base‘𝐴))) |
62 | 61 | ad5ant23 757 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → 〈𝑥, 𝑦〉 ∈ ((Base‘𝐴) × (Base‘𝐴))) |
63 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑥 ∈ V |
64 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑦 ∈ V |
65 | 63, 64 | op1std 7835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (1st ‘𝑤) = 𝑥) |
66 | 65 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑓‘(1st ‘𝑤)) = (𝑓‘𝑥)) |
67 | 63, 64 | op2ndd 7836 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (2nd ‘𝑤) = 𝑦) |
68 | 67 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (𝑓‘(2nd ‘𝑤)) = (𝑓‘𝑦)) |
69 | 66, 68 | oveq12d 7290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) = ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦))) |
70 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘〈𝑥, 𝑦〉)) |
71 | | df-ov 7275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥(Hom ‘𝐴)𝑦) = ((Hom ‘𝐴)‘〈𝑥, 𝑦〉) |
72 | 70, 71 | eqtr4di 2798 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 〈𝑥, 𝑦〉 → ((Hom ‘𝐴)‘𝑤) = (𝑥(Hom ‘𝐴)𝑦)) |
73 | 69, 72 | oveq12d 7290 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 〈𝑥, 𝑦〉 → (((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)) = (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦))) |
74 | 73 | fvixp 8682 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ X𝑤 ∈
((Base‘𝐴) ×
(Base‘𝐴))(((𝑓‘(1st
‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)) ∧ 〈𝑥, 𝑦〉 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘〈𝑥, 𝑦〉) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦))) |
75 | 60, 62, 74 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑔‘〈𝑥, 𝑦〉) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦))) |
76 | 57, 75 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦))) |
77 | | elmapi 8629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥𝑔𝑦) ∈ (((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦)) ↑m (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦))) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐴)𝑦)⟶((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦))) |
80 | 79, 42 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑥𝑔𝑦)‘𝑚) ∈ ((𝑓‘𝑥)(Hom ‘𝐶)(𝑓‘𝑦))) |
81 | | df-ov 7275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦𝑔𝑧) = (𝑔‘〈𝑦, 𝑧〉) |
82 | | opelxpi 5627 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ (Base‘𝐴) ∧ 𝑧 ∈ (Base‘𝐴)) → 〈𝑦, 𝑧〉 ∈ ((Base‘𝐴) × (Base‘𝐴))) |
83 | 82 | adantll 711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 〈𝑦, 𝑧〉 ∈ ((Base‘𝐴) × (Base‘𝐴))) |
84 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑧 ∈ V |
85 | 64, 84 | op1std 7835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (1st ‘𝑤) = 𝑦) |
86 | 85 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (𝑓‘(1st ‘𝑤)) = (𝑓‘𝑦)) |
87 | 64, 84 | op2ndd 7836 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (2nd ‘𝑤) = 𝑧) |
88 | 87 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (𝑓‘(2nd ‘𝑤)) = (𝑓‘𝑧)) |
89 | 86, 88 | oveq12d 7290 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 〈𝑦, 𝑧〉 → ((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) = ((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧))) |
90 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 〈𝑦, 𝑧〉 → ((Hom ‘𝐴)‘𝑤) = ((Hom ‘𝐴)‘〈𝑦, 𝑧〉)) |
91 | | df-ov 7275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦(Hom ‘𝐴)𝑧) = ((Hom ‘𝐴)‘〈𝑦, 𝑧〉) |
92 | 90, 91 | eqtr4di 2798 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 〈𝑦, 𝑧〉 → ((Hom ‘𝐴)‘𝑤) = (𝑦(Hom ‘𝐴)𝑧)) |
93 | 89, 92 | oveq12d 7290 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)) = (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧))) |
94 | 93 | fvixp 8682 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ X𝑤 ∈
((Base‘𝐴) ×
(Base‘𝐴))(((𝑓‘(1st
‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)) ∧ 〈𝑦, 𝑧〉 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑔‘〈𝑦, 𝑧〉) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧))) |
95 | 59, 83, 94 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑔‘〈𝑦, 𝑧〉) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧))) |
96 | 81, 95 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧))) |
97 | | elmapi 8629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦𝑔𝑧) ∈ (((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧)) ↑m (𝑦(Hom ‘𝐴)𝑧)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧))) |
99 | 98 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (𝑦𝑔𝑧):(𝑦(Hom ‘𝐴)𝑧)⟶((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧))) |
100 | 99 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → ((𝑦𝑔𝑧)‘𝑛) ∈ ((𝑓‘𝑦)(Hom ‘𝐶)(𝑓‘𝑧))) |
101 | 46, 47, 48, 49, 50, 51, 54, 55, 56, 80, 100 | comfeqval 17428 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) |
102 | 45, 101 | eqeq12d 2756 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) ∧ 𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)) → (((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
103 | 102 | ralbidva 3122 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) ∧ 𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
104 | 103 | ralbidva 3122 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
105 | | eqid 2740 |
. . . . . . . . . . . . . . 15
⊢ (Hom
‘𝐵) = (Hom
‘𝐵) |
106 | 22 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
107 | | simpllr 773 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑥 ∈ (Base‘𝐴)) |
108 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑦 ∈ (Base‘𝐴)) |
109 | 33, 34, 105, 106, 107, 108 | homfeqval 17417 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑥(Hom ‘𝐴)𝑦) = (𝑥(Hom ‘𝐵)𝑦)) |
110 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → 𝑧 ∈ (Base‘𝐴)) |
111 | 33, 34, 105, 106, 108, 110 | homfeqval 17417 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (𝑦(Hom ‘𝐴)𝑧) = (𝑦(Hom ‘𝐵)𝑧)) |
112 | 111 | raleqdv 3347 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
113 | 109, 112 | raleqbidv 3335 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
114 | 104, 113 | bitrd 278 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) ∧ 𝑧 ∈ (Base‘𝐴)) → (∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
115 | 114 | ralbidva 3122 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) ∧ 𝑦 ∈ (Base‘𝐴)) → (∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
116 | 115 | ralbidva 3122 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → (∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
117 | 32, 116 | anbi12d 631 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
118 | 117 | ralbidva 3122 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑤 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑤))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑤))) ↑m ((Hom
‘𝐴)‘𝑤)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
119 | 21, 118 | sylan2b 594 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)))) → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
120 | 119 | pm5.32da 579 |
. . . . . 6
⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
121 | | eqid 2740 |
. . . . . . . . . . . . . 14
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
122 | 8 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
123 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) |
124 | | xp1st 7857 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (1st
‘𝑧) ∈
(Base‘𝐴)) |
125 | 124 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (1st ‘𝑧) ∈ (Base‘𝐴)) |
126 | 123, 125 | ffvelrnd 6959 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(1st ‘𝑧)) ∈ (Base‘𝐶)) |
127 | | xp2nd 7858 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → (2nd
‘𝑧) ∈
(Base‘𝐴)) |
128 | 127 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (2nd ‘𝑧) ∈ (Base‘𝐴)) |
129 | 123, 128 | ffvelrnd 6959 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (𝑓‘(2nd ‘𝑧)) ∈ (Base‘𝐶)) |
130 | 46, 47, 121, 122, 126, 129 | homfeqval 17417 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧)))) |
131 | 3 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (Homf
‘𝐴) =
(Homf ‘𝐵)) |
132 | 33, 34, 105, 131, 125, 128 | homfeqval 17417 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((1st ‘𝑧)(Hom ‘𝐴)(2nd ‘𝑧)) = ((1st ‘𝑧)(Hom ‘𝐵)(2nd ‘𝑧))) |
133 | | df-ov 7275 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑧)(Hom ‘𝐴)(2nd ‘𝑧)) = ((Hom ‘𝐴)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
134 | | df-ov 7275 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑧)(Hom ‘𝐵)(2nd ‘𝑧)) = ((Hom ‘𝐵)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
135 | 132, 133,
134 | 3eqtr3g 2803 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) = ((Hom ‘𝐵)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
136 | | 1st2nd2 7864 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
138 | 137 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐴)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
139 | 137 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐵)‘𝑧) = ((Hom ‘𝐵)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
140 | 135, 138,
139 | 3eqtr4d 2790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → ((Hom ‘𝐴)‘𝑧) = ((Hom ‘𝐵)‘𝑧)) |
141 | 130, 140 | oveq12d 7290 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))) → (((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) = (((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) |
142 | 141 | ixpeq2dva 8692 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) = X𝑧 ∈
((Base‘𝐴) ×
(Base‘𝐴))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) |
143 | 3 | homfeqbas 17416 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (Base‘𝐴) = (Base‘𝐵)) |
144 | 143 | sqxpeqd 5622 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵))) |
145 | 144 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → ((Base‘𝐴) × (Base‘𝐴)) = ((Base‘𝐵) × (Base‘𝐵))) |
146 | 145 | ixpeq1d 8689 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧)) = X𝑧 ∈
((Base‘𝐵) ×
(Base‘𝐵))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) |
147 | 142, 146 | eqtrd 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) = X𝑧 ∈
((Base‘𝐵) ×
(Base‘𝐵))(((𝑓‘(1st
‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) |
148 | 147 | eleq2d 2826 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓:(Base‘𝐴)⟶(Base‘𝐶)) → (𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) ↔ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧)))) |
149 | 148 | pm5.32da 579 |
. . . . . . . 8
⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))))) |
150 | 8 | homfeqbas 17416 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
151 | 143, 150 | feq23d 6593 |
. . . . . . . . 9
⊢ (𝜑 → (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ↔ 𝑓:(Base‘𝐵)⟶(Base‘𝐷))) |
152 | 151 | anbi1d 630 |
. . . . . . . 8
⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))))) |
153 | 149, 152 | bitrd 278 |
. . . . . . 7
⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))))) |
154 | 143 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → (Base‘𝐴) = (Base‘𝐵)) |
155 | 154 | raleqdv 3347 |
. . . . . . . . . 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 629 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐴)) → ((((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
158 | 143, 157 | raleqbidva 3353 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
159 | 153, 158 | anbi12d 631 |
. . . . . 6
⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
160 | 120, 159 | bitrd 278 |
. . . . 5
⊢ (𝜑 → (((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
161 | | df-3an 1088 |
. . . . 5
⊢ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
162 | | df-3an 1088 |
. . . . 5
⊢ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧))) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
163 | 160, 161,
162 | 3bitr4g 314 |
. . . 4
⊢ (𝜑 → ((𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
164 | 13, 163 | anbi12d 631 |
. . 3
⊢ (𝜑 → (((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))) |
165 | | df-br 5080 |
. . . . 5
⊢ (𝑓(𝐴 Func 𝐶)𝑔 ↔ 〈𝑓, 𝑔〉 ∈ (𝐴 Func 𝐶)) |
166 | | funcrcl 17589 |
. . . . 5
⊢
(〈𝑓, 𝑔〉 ∈ (𝐴 Func 𝐶) → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat)) |
167 | 165, 166 | sylbi 216 |
. . . 4
⊢ (𝑓(𝐴 Func 𝐶)𝑔 → (𝐴 ∈ Cat ∧ 𝐶 ∈ Cat)) |
168 | | eqid 2740 |
. . . . 5
⊢
(Id‘𝐴) =
(Id‘𝐴) |
169 | | eqid 2740 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
170 | | simpl 483 |
. . . . 5
⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐴 ∈ Cat) |
171 | | simpr 485 |
. . . . 5
⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat) |
172 | 33, 46, 34, 47, 168, 169, 35, 48, 170, 171 | isfunc 17590 |
. . . 4
⊢ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) → (𝑓(𝐴 Func 𝐶)𝑔 ↔ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
173 | 167, 172 | biadanii 819 |
. . 3
⊢ (𝑓(𝐴 Func 𝐶)𝑔 ↔ ((𝐴 ∈ Cat ∧ 𝐶 ∈ Cat) ∧ (𝑓:(Base‘𝐴)⟶(Base‘𝐶) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐴) × (Base‘𝐴))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐶)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐴)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐴)(((𝑥𝑔𝑥)‘((Id‘𝐴)‘𝑥)) = ((Id‘𝐶)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐴)∀𝑧 ∈ (Base‘𝐴)∀𝑚 ∈ (𝑥(Hom ‘𝐴)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐴)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐴)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐶)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
174 | | df-br 5080 |
. . . . 5
⊢ (𝑓(𝐵 Func 𝐷)𝑔 ↔ 〈𝑓, 𝑔〉 ∈ (𝐵 Func 𝐷)) |
175 | | funcrcl 17589 |
. . . . 5
⊢
(〈𝑓, 𝑔〉 ∈ (𝐵 Func 𝐷) → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat)) |
176 | 174, 175 | sylbi 216 |
. . . 4
⊢ (𝑓(𝐵 Func 𝐷)𝑔 → (𝐵 ∈ Cat ∧ 𝐷 ∈ Cat)) |
177 | | eqid 2740 |
. . . . 5
⊢
(Base‘𝐵) =
(Base‘𝐵) |
178 | | eqid 2740 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
179 | | eqid 2740 |
. . . . 5
⊢
(Id‘𝐵) =
(Id‘𝐵) |
180 | | eqid 2740 |
. . . . 5
⊢
(Id‘𝐷) =
(Id‘𝐷) |
181 | | simpl 483 |
. . . . 5
⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐵 ∈ Cat) |
182 | | simpr 485 |
. . . . 5
⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → 𝐷 ∈ Cat) |
183 | 177, 178,
105, 121, 179, 180, 36, 49, 181, 182 | isfunc 17590 |
. . . 4
⊢ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓(𝐵 Func 𝐷)𝑔 ↔ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
184 | 176, 183 | biadanii 819 |
. . 3
⊢ (𝑓(𝐵 Func 𝐷)𝑔 ↔ ((𝐵 ∈ Cat ∧ 𝐷 ∈ Cat) ∧ (𝑓:(Base‘𝐵)⟶(Base‘𝐷) ∧ 𝑔 ∈ X𝑧 ∈ ((Base‘𝐵) × (Base‘𝐵))(((𝑓‘(1st ‘𝑧))(Hom ‘𝐷)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom
‘𝐵)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐵)(((𝑥𝑔𝑥)‘((Id‘𝐵)‘𝑥)) = ((Id‘𝐷)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐵)∀𝑧 ∈ (Base‘𝐵)∀𝑚 ∈ (𝑥(Hom ‘𝐵)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐵)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐵)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝐷)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
185 | 164, 173,
184 | 3bitr4g 314 |
. 2
⊢ (𝜑 → (𝑓(𝐴 Func 𝐶)𝑔 ↔ 𝑓(𝐵 Func 𝐷)𝑔)) |
186 | 1, 2, 185 | eqbrrdiv 5703 |
1
⊢ (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷)) |