Step | Hyp | Ref
| Expression |
1 | | df-br 5077 |
. . . . 5
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
2 | | funcrcl 17576 |
. . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
3 | 1, 2 | sylbi 216 |
. . . 4
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
4 | 3 | simpld 495 |
. . 3
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat) |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat)) |
6 | | df-br 5077 |
. . . . 5
⊢ (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅))) |
7 | | funcrcl 17576 |
. . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅)) → (𝐶 ∈ Cat ∧ (𝐷 ↾cat 𝑅) ∈ Cat)) |
8 | 6, 7 | sylbi 216 |
. . . 4
⊢ (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 → (𝐶 ∈ Cat ∧ (𝐷 ↾cat 𝑅) ∈ Cat)) |
9 | 8 | simpld 495 |
. . 3
⊢ (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 → 𝐶 ∈ Cat) |
10 | 9 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 → 𝐶 ∈ Cat)) |
11 | | funcres2b.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
12 | | funcres2b.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (Subcat‘𝐷)) |
13 | | funcres2b.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 Fn (𝑆 × 𝑆)) |
14 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝐷) =
(Base‘𝐷) |
15 | 12, 13, 14 | subcss1 17555 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝐷)) |
16 | 11, 15 | fssd 6620 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐷)) |
17 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝐷 ↾cat 𝑅) = (𝐷 ↾cat 𝑅) |
18 | | subcrcl 17526 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (Subcat‘𝐷) → 𝐷 ∈ Cat) |
19 | 12, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ Cat) |
20 | 17, 14, 19, 13, 15 | rescbas 17539 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (Base‘(𝐷 ↾cat 𝑅))) |
21 | 20 | feq3d 6589 |
. . . . . . . 8
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
22 | 11, 21 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅))) |
23 | 16, 22 | 2thd 264 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝐴⟶(Base‘𝐷) ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
24 | 23 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹:𝐴⟶(Base‘𝐷) ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
25 | | funcres2b.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
26 | 25 | adantlr 712 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
27 | 26 | frnd 6610 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
28 | 12 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 ∈ (Subcat‘𝐷)) |
29 | 13 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 Fn (𝑆 × 𝑆)) |
30 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
31 | 11 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝐹:𝐴⟶𝑆) |
32 | | simprl 768 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
33 | 31, 32 | ffvelrnd 6964 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑥) ∈ 𝑆) |
34 | | simprr 770 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
35 | 31, 34 | ffvelrnd 6964 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑦) ∈ 𝑆) |
36 | 28, 29, 30, 33, 35 | subcss2 17556 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
37 | 27, 36 | sstrd 3932 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
38 | 37, 27 | 2thd 264 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
39 | 38 | anbi2d 629 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦))))) |
40 | | df-f 6439 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
41 | | df-f 6439 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
42 | 39, 40, 41 | 3bitr4g 314 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
43 | 17, 14, 19, 13, 15 | reschom 17541 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
44 | 43 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
45 | 44 | oveqd 7294 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)𝑅(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
46 | 45 | feq3d 6589 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
47 | 42, 46 | bitrd 278 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
48 | 47 | ralrimivva 3111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
49 | | fveq2 6776 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝐺‘〈𝑥, 𝑦〉)) |
50 | | df-ov 7280 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝐺𝑦) = (𝐺‘〈𝑥, 𝑦〉) |
51 | 49, 50 | eqtr4di 2796 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝑥𝐺𝑦)) |
52 | | vex 3435 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
53 | | vex 3435 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
54 | 52, 53 | op1std 7841 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
55 | 54 | fveq2d 6780 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥)) |
56 | 52, 53 | op2ndd 7842 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
57 | 56 | fveq2d 6780 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑧)) = (𝐹‘𝑦)) |
58 | 55, 57 | oveq12d 7295 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
59 | | fveq2 6776 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
60 | | df-ov 7280 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
61 | 59, 60 | eqtr4di 2796 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
62 | 58, 61 | oveq12d 7295 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) |
63 | 51, 62 | eleq12d 2833 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))) |
64 | | ovex 7310 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ∈ V |
65 | | ovex 7310 |
. . . . . . . . . . . . 13
⊢ (𝑥𝐻𝑦) ∈ V |
66 | 64, 65 | elmap 8657 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
67 | 63, 66 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
68 | 55, 57 | oveq12d 7295 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
69 | 68, 61 | oveq12d 7295 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) |
70 | 51, 69 | eleq12d 2833 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))) |
71 | | ovex 7310 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ∈ V |
72 | 71, 65 | elmap 8657 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
73 | 70, 72 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
74 | 67, 73 | bibi12d 346 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ↔ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))))) |
75 | 74 | ralxp 5752 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
76 | 48, 75 | sylibr 233 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ∀𝑧 ∈ (𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
77 | | ralbi 3089 |
. . . . . . . 8
⊢
(∀𝑧 ∈
(𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) → (∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
78 | 76, 77 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
79 | 78 | 3anbi3d 1441 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ((𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))) |
80 | | elixp2 8687 |
. . . . . 6
⊢ (𝐺 ∈ X𝑧 ∈
(𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
81 | | elixp2 8687 |
. . . . . 6
⊢ (𝐺 ∈ X𝑧 ∈
(𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
82 | 79, 80, 81 | 3bitr4g 314 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
83 | 12 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ (Subcat‘𝐷)) |
84 | 13 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → 𝑅 Fn (𝑆 × 𝑆)) |
85 | | eqid 2738 |
. . . . . . . . 9
⊢
(Id‘𝐷) =
(Id‘𝐷) |
86 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐹:𝐴⟶𝑆) |
87 | 86 | ffvelrnda 6963 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝑆) |
88 | 17, 83, 84, 85, 87 | subcid 17560 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → ((Id‘𝐷)‘(𝐹‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥))) |
89 | 88 | eqeq2d 2749 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ↔ ((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)))) |
90 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(comp‘𝐷) =
(comp‘𝐷) |
91 | 17, 14, 19, 13, 15, 90 | rescco 17543 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (comp‘𝐷) = (comp‘(𝐷 ↾cat 𝑅))) |
92 | 91 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (comp‘𝐷) = (comp‘(𝐷 ↾cat 𝑅))) |
93 | 92 | oveqd 7294 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧)) = (〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))) |
94 | 93 | oveqd 7294 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) |
95 | 94 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
96 | 95 | 2ralbidv 3120 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
97 | 96 | 2ralbidv 3120 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
98 | 89, 97 | anbi12d 631 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → ((((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) ↔ (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))))) |
99 | 98 | ralbidva 3117 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) ↔ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))))) |
100 | 24, 82, 99 | 3anbi123d 1435 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ((𝐹:𝐴⟶(Base‘𝐷) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) ↔ (𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))))) |
101 | | funcres2b.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
102 | | funcres2b.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
103 | | eqid 2738 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
104 | | eqid 2738 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
105 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat) |
106 | 19 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐷 ∈ Cat) |
107 | 101, 14, 102, 30, 103, 85, 104, 90, 105, 106 | isfunc 17577 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ (𝐹:𝐴⟶(Base‘𝐷) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))))) |
108 | | eqid 2738 |
. . . . 5
⊢
(Base‘(𝐷
↾cat 𝑅)) =
(Base‘(𝐷
↾cat 𝑅)) |
109 | | eqid 2738 |
. . . . 5
⊢ (Hom
‘(𝐷
↾cat 𝑅)) =
(Hom ‘(𝐷
↾cat 𝑅)) |
110 | | eqid 2738 |
. . . . 5
⊢
(Id‘(𝐷
↾cat 𝑅)) =
(Id‘(𝐷
↾cat 𝑅)) |
111 | | eqid 2738 |
. . . . 5
⊢
(comp‘(𝐷
↾cat 𝑅)) =
(comp‘(𝐷
↾cat 𝑅)) |
112 | 17, 12 | subccat 17561 |
. . . . . 6
⊢ (𝜑 → (𝐷 ↾cat 𝑅) ∈ Cat) |
113 | 112 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐷 ↾cat 𝑅) ∈ Cat) |
114 | 101, 108,
102, 109, 103, 110, 104, 111, 105, 113 | isfunc 17577 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 ↔ (𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))))) |
115 | 100, 107,
114 | 3bitr4d 311 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺)) |
116 | 115 | ex 413 |
. 2
⊢ (𝜑 → (𝐶 ∈ Cat → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺))) |
117 | 5, 10, 116 | pm5.21ndd 381 |
1
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺)) |