| Step | Hyp | Ref
| Expression |
| 1 | | df-br 5144 |
. . . . 5
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
| 2 | | funcrcl 17908 |
. . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 3 | 1, 2 | sylbi 217 |
. . . 4
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 4 | 3 | simpld 494 |
. . 3
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat) |
| 5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat)) |
| 6 | | df-br 5144 |
. . . . 5
⊢ (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅))) |
| 7 | | funcrcl 17908 |
. . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅)) → (𝐶 ∈ Cat ∧ (𝐷 ↾cat 𝑅) ∈ Cat)) |
| 8 | 6, 7 | sylbi 217 |
. . . 4
⊢ (𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺 → (𝐶 ∈ Cat ∧ (𝐷 ↾cat 𝑅) ∈ Cat)) |
| 9 | 8 | simpld 494 |
. . 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 2737 |
. . . . . . . . 9
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 15 | 12, 13, 14 | subcss1 17887 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝐷)) |
| 16 | 11, 15 | fssd 6753 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝐷)) |
| 17 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝐷 ↾cat 𝑅) = (𝐷 ↾cat 𝑅) |
| 18 | | subcrcl 17860 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (Subcat‘𝐷) → 𝐷 ∈ Cat) |
| 19 | 12, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 20 | 17, 14, 19, 13, 15 | rescbas 17873 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (Base‘(𝐷 ↾cat 𝑅))) |
| 21 | 20 | feq3d 6723 |
. . . . . . . 8
⊢ (𝜑 → (𝐹:𝐴⟶𝑆 ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
| 22 | 11, 21 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅))) |
| 23 | 16, 22 | 2thd 265 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝐴⟶(Base‘𝐷) ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
| 24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹:𝐴⟶(Base‘𝐷) ↔ 𝐹:𝐴⟶(Base‘(𝐷 ↾cat 𝑅)))) |
| 25 | | funcres2b.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
| 26 | 25 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):𝑌⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
| 27 | 26 | frnd 6744 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦))) |
| 28 | 12 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 ∈ (Subcat‘𝐷)) |
| 29 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 Fn (𝑆 × 𝑆)) |
| 30 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 31 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝐹:𝐴⟶𝑆) |
| 32 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
| 33 | 31, 32 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑥) ∈ 𝑆) |
| 34 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
| 35 | 31, 34 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑦) ∈ 𝑆) |
| 36 | 28, 29, 30, 33, 35 | subcss2 17888 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 37 | 27, 36 | sstrd 3994 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 38 | 37, 27 | 2thd 265 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
| 39 | 38 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦))))) |
| 40 | | df-f 6565 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
| 41 | | df-f 6565 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ↔ ((𝑥𝐺𝑦) Fn (𝑥𝐻𝑦) ∧ ran (𝑥𝐺𝑦) ⊆ ((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
| 42 | 39, 40, 41 | 3bitr4g 314 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)))) |
| 43 | 17, 14, 19, 13, 15 | reschom 17874 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
| 44 | 43 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
| 45 | 44 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)𝑅(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
| 46 | 45 | feq3d 6723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝑅(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
| 47 | 42, 46 | bitrd 279 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
| 48 | 47 | ralrimivva 3202 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
| 49 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝐺‘〈𝑥, 𝑦〉)) |
| 50 | | df-ov 7434 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝐺𝑦) = (𝐺‘〈𝑥, 𝑦〉) |
| 51 | 49, 50 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝑥𝐺𝑦)) |
| 52 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
| 53 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
| 54 | 52, 53 | op1std 8024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
| 55 | 54 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥)) |
| 56 | 52, 53 | op2ndd 8025 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
| 57 | 56 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑧)) = (𝐹‘𝑦)) |
| 58 | 55, 57 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 59 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
| 60 | | df-ov 7434 |
. . . . . . . . . . . . . . 15
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
| 61 | 59, 60 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
| 62 | 58, 61 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) |
| 63 | 51, 62 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))) |
| 64 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ∈ V |
| 65 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝑥𝐻𝑦) ∈ V |
| 66 | 64, 65 | elmap 8911 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 67 | 63, 66 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
| 68 | 55, 57 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
| 69 | 68, 61 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) |
| 70 | 51, 69 | eleq12d 2835 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))) |
| 71 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ∈ V |
| 72 | 71, 65 | elmap 8911 |
. . . . . . . . . . . 12
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))) |
| 73 | 70, 72 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
| 74 | 67, 73 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ↔ ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦))))) |
| 75 | 74 | ralxp 5852 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘𝑦)))) |
| 76 | 48, 75 | sylibr 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ∀𝑧 ∈ (𝐴 × 𝐴)((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
| 77 | | ralbi 3103 |
. . . . . . . 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 1444 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → ((𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘(𝐷 ↾cat 𝑅))(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))) |
| 80 | | elixp2 8941 |
. . . . . 6
⊢ (𝐺 ∈ X𝑧 ∈
(𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐴 × 𝐴) ∧ ∀𝑧 ∈ (𝐴 × 𝐴)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) |
| 81 | | elixp2 8941 |
. . . . . 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 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ (Subcat‘𝐷)) |
| 84 | 13 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → 𝑅 Fn (𝑆 × 𝑆)) |
| 85 | | eqid 2737 |
. . . . . . . . 9
⊢
(Id‘𝐷) =
(Id‘𝐷) |
| 86 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐹:𝐴⟶𝑆) |
| 87 | 86 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝑆) |
| 88 | 17, 83, 84, 85, 87 | subcid 17892 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → ((Id‘𝐷)‘(𝐹‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥))) |
| 89 | 88 | eqeq2d 2748 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ↔ ((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)))) |
| 90 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(comp‘𝐷) =
(comp‘𝐷) |
| 91 | 17, 14, 19, 13, 15, 90 | rescco 17876 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (comp‘𝐷) = (comp‘(𝐷 ↾cat 𝑅))) |
| 92 | 91 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (comp‘𝐷) = (comp‘(𝐷 ↾cat 𝑅))) |
| 93 | 92 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧)) = (〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))) |
| 94 | 93 | oveqd 7448 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) |
| 95 | 94 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
| 96 | 95 | 2ralbidv 3221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
| 97 | 96 | 2ralbidv 3221 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))) |
| 98 | 89, 97 | anbi12d 632 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ 𝐴) → ((((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) ↔ (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))))) |
| 99 | 98 | ralbidva 3176 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))) ↔ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 ↾cat 𝑅))‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘(𝐷 ↾cat 𝑅))(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓))))) |
| 100 | 24, 82, 99 | 3anbi123d 1438 |
. . . 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 2737 |
. . . . 5
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 104 | | eqid 2737 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 105 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat) |
| 106 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐷 ∈ Cat) |
| 107 | 101, 14, 102, 30, 103, 85, 104, 90, 105, 106 | isfunc 17909 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ (𝐹:𝐴⟶(Base‘𝐷) ∧ 𝐺 ∈ X𝑧 ∈ (𝐴 × 𝐴)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐷)(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐴 (((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ∀𝑓 ∈ (𝑥𝐻𝑦)∀𝑔 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑓)))))) |
| 108 | | eqid 2737 |
. . . . 5
⊢
(Base‘(𝐷
↾cat 𝑅)) =
(Base‘(𝐷
↾cat 𝑅)) |
| 109 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘(𝐷
↾cat 𝑅)) =
(Hom ‘(𝐷
↾cat 𝑅)) |
| 110 | | eqid 2737 |
. . . . 5
⊢
(Id‘(𝐷
↾cat 𝑅)) =
(Id‘(𝐷
↾cat 𝑅)) |
| 111 | | eqid 2737 |
. . . . 5
⊢
(comp‘(𝐷
↾cat 𝑅)) =
(comp‘(𝐷
↾cat 𝑅)) |
| 112 | 17, 12 | subccat 17893 |
. . . . . 6
⊢ (𝜑 → (𝐷 ↾cat 𝑅) ∈ Cat) |
| 113 | 112 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝐷 ↾cat 𝑅) ∈ Cat) |
| 114 | 101, 108,
102, 109, 103, 110, 104, 111, 105, 113 | isfunc 17909 |
. . . 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 412 |
. 2
⊢ (𝜑 → (𝐶 ∈ Cat → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺))) |
| 117 | 5, 10, 116 | pm5.21ndd 379 |
1
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat 𝑅))𝐺)) |