Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. . . . 5
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
2 | | funcrcl 16346 |
. . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
3 | 1, 2 | sylbi 206 |
. . . 4
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
4 | 3 | simpld 474 |
. . 3
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat) |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat)) |
6 | | df-br 4584 |
. . . . 5
⊢ (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅))) |
7 | | funcrcl 16346 |
. . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅)) → (𝐶 ∈ Cat ∧ (𝐷 ↾cat 𝑅) ∈ Cat)) |
8 | 6, 7 | sylbi 206 |
. . . 4
⊢ (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 → (𝐶 ∈ Cat ∧ (𝐷 ↾cat 𝑅) ∈ Cat)) |
9 | 8 | simpld 474 |
. . 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 2610 |
. . . . . . . . 9
⊢
(Base‘𝐷) =
(Base‘𝐷) |
15 | 12, 13, 14 | subcss1 16325 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝐷)) |
16 | 11, 15 | fssd 5970 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐷)) |
17 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝐷 ↾cat 𝑅) = (𝐷 ↾cat 𝑅) |
18 | | subcrcl 16299 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (Subcat‘𝐷) → 𝐷 ∈ Cat) |
19 | 12, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ Cat) |
20 | 17, 14, 19, 13, 15 | rescbas 16312 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (Base‘(𝐷 ↾cat 𝑅))) |
21 | 20 | feq3d 5945 |
. . . . . . . 8
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
22 | 11, 21 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅))) |
23 | 16, 22 | 2thd 254 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝐴⟶(Base‘𝐷) ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹:𝐴⟶(Base‘𝐷) ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
25 | | funcres2b.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
26 | 25 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
27 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)) → ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
29 | 12 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 ∈ (Subcat‘𝐷)) |
30 | 13 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 Fn (𝑆 × 𝑆)) |
31 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
32 | 11 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝐹:𝐴⟶𝑆) |
33 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
34 | 32, 33 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑥) ∈ 𝑆) |
35 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
36 | 32, 35 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑦) ∈ 𝑆) |
37 | 29, 30, 31, 34, 36 | subcss2 16326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
38 | 28, 37 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
39 | 38, 28 | 2thd 254 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
40 | 39 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦))))) |
41 | | df-f 5808 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
42 | | df-f 5808 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
43 | 40, 41, 42 | 3bitr4g 302 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
44 | 17, 14, 19, 13, 15 | reschom 16313 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
45 | 44 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
46 | 45 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)𝑅(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
47 | 46 | feq3d 5945 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
48 | 43, 47 | bitrd 267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
49 | 48 | ralrimivva 2954 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
50 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝐺‘〈𝑥, 𝑦〉)) |
51 | | df-ov 6552 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝐺𝑦) = (𝐺‘〈𝑥, 𝑦〉) |
52 | 50, 51 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝑥𝐺𝑦)) |
53 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
54 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
55 | 53, 54 | op1std 7069 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
56 | 55 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥)) |
57 | 53, 54 | op2ndd 7070 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
58 | 57 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑧)) = (𝐹‘𝑦)) |
59 | 56, 58 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
61 | | df-ov 6552 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
62 | 60, 61 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
63 | 59, 62 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) = (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦))) |
64 | 52, 63 | eleq12d 2682 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦)))) |
65 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ∈ V |
66 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑥𝐻𝑦) ∈ V |
67 | 65, 66 | elmap 7772 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
68 | 64, 67 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
69 | 56, 58 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
70 | 69, 62 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) = (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦))) |
71 | 52, 70 | eleq12d 2682 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦)))) |
72 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ∈ V |
73 | 72, 66 | elmap 7772 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
74 | 71, 73 | syl6bb 275 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
75 | 68, 74 | bibi12d 334 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ↔ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))))) |
76 | 75 | ralxp 5185 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
77 | 49, 76 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ∀𝑧 ∈ (𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
78 | | ralbi 3050 |
. . . . . . . 8
⊢
(∀𝑧 ∈
(𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) → (∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
80 | 79 | 3anbi3d 1397 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ((𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))))) |
81 | | elixp2 7798 |
. . . . . 6
⊢ (𝐺 ∈ X𝑧 ∈
(𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
82 | | elixp2 7798 |
. . . . . 6
⊢ (𝐺 ∈ X𝑧 ∈
(𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
83 | 80, 81, 82 | 3bitr4g 302 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
84 | 12 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ (Subcat‘𝐷)) |
85 | 13 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → 𝑅 Fn (𝑆 × 𝑆)) |
86 | | eqid 2610 |
. . . . . . . . 9
⊢
(Id‘𝐷) =
(Id‘𝐷) |
87 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐹:𝐴⟶𝑆) |
88 | 87 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝑆) |
89 | 17, 84, 85, 86, 88 | subcid 16330 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → ((Id‘𝐷)‘(𝐹‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥))) |
90 | 89 | eqeq2d 2620 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ↔ ((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)))) |
91 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(comp‘𝐷) =
(comp‘𝐷) |
92 | 17, 14, 19, 13, 15, 91 | rescco 16315 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (comp‘𝐷) = (comp‘(𝐷 ↾cat 𝑅))) |
93 | 92 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (comp‘𝐷) = (comp‘(𝐷 ↾cat 𝑅))) |
94 | 93 | oveqd 6566 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧)) = (〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))) |
95 | 94 | oveqd 6566 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) |
96 | 95 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
97 | 96 | 2ralbidv 2972 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
98 | 97 | 2ralbidv 2972 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
99 | 90, 98 | anbi12d 743 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → ((((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) ↔ (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))))) |
100 | 99 | ralbidva 2968 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) ↔ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))))) |
101 | 24, 83, 100 | 3anbi123d 1391 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ((𝐹:𝐴⟶(Base‘𝐷) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) ↔ (𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))))) |
102 | | funcres2b.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
103 | | funcres2b.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
104 | | eqid 2610 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
105 | | eqid 2610 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
106 | | simpr 476 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat) |
107 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐷 ∈ Cat) |
108 | 102, 14, 103, 31, 104, 86, 105, 91, 106, 107 | isfunc 16347 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ (𝐹:𝐴⟶(Base‘𝐷) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))))) |
109 | | eqid 2610 |
. . . . 5
⊢
(Base‘(𝐷
↾cat 𝑅)) =
(Base‘(𝐷
↾cat 𝑅)) |
110 | | eqid 2610 |
. . . . 5
⊢ (Hom
‘(𝐷
↾cat 𝑅)) =
(Hom ‘(𝐷
↾cat 𝑅)) |
111 | | eqid 2610 |
. . . . 5
⊢
(Id‘(𝐷
↾cat 𝑅)) =
(Id‘(𝐷
↾cat 𝑅)) |
112 | | eqid 2610 |
. . . . 5
⊢
(comp‘(𝐷
↾cat 𝑅)) =
(comp‘(𝐷
↾cat 𝑅)) |
113 | 17, 12 | subccat 16331 |
. . . . . 6
⊢ (𝜑 → (𝐷 ↾cat 𝑅) ∈ Cat) |
114 | 113 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐷 ↾cat 𝑅) ∈ Cat) |
115 | 102, 109,
103, 110, 104, 111, 105, 112, 106, 114 | isfunc 16347 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 ↔ (𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))))) |
116 | 101, 108,
115 | 3bitr4d 299 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺)) |
117 | 116 | ex 449 |
. 2
⊢ (𝜑 → (𝐶 ∈ Cat → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺))) |
118 | 5, 10, 117 | pm5.21ndd 368 |
1
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺)) |