| Step | Hyp | Ref
| Expression |
| 1 | | relfunc 17907 |
. . 3
⊢ Rel
(𝐶 Func (𝐷 ↾cat 𝑅)) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝑅 ∈ (Subcat‘𝐷) → Rel (𝐶 Func (𝐷 ↾cat 𝑅))) |
| 3 | | simpr 484 |
. . . . 5
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) |
| 4 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 5 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 6 | | simpl 482 |
. . . . . 6
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝑅 ∈ (Subcat‘𝐷)) |
| 7 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → dom dom 𝑅 = dom dom 𝑅) |
| 8 | 6, 7 | subcfn 17886 |
. . . . . 6
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝑅 Fn (dom dom 𝑅 × dom dom 𝑅)) |
| 9 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝐷
↾cat 𝑅)) =
(Base‘(𝐷
↾cat 𝑅)) |
| 10 | 4, 9, 3 | funcf1 17911 |
. . . . . . 7
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝑓:(Base‘𝐶)⟶(Base‘(𝐷 ↾cat 𝑅))) |
| 11 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝐷 ↾cat 𝑅) = (𝐷 ↾cat 𝑅) |
| 12 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 13 | | subcrcl 17860 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (Subcat‘𝐷) → 𝐷 ∈ Cat) |
| 14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝐷 ∈ Cat) |
| 15 | 6, 8, 12 | subcss1 17887 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → dom dom 𝑅 ⊆ (Base‘𝐷)) |
| 16 | 11, 12, 14, 8, 15 | rescbas 17873 |
. . . . . . . 8
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → dom dom 𝑅 = (Base‘(𝐷 ↾cat 𝑅))) |
| 17 | 16 | feq3d 6723 |
. . . . . . 7
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → (𝑓:(Base‘𝐶)⟶dom dom 𝑅 ↔ 𝑓:(Base‘𝐶)⟶(Base‘(𝐷 ↾cat 𝑅)))) |
| 18 | 10, 17 | mpbird 257 |
. . . . . 6
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝑓:(Base‘𝐶)⟶dom dom 𝑅) |
| 19 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘(𝐷
↾cat 𝑅)) =
(Hom ‘(𝐷
↾cat 𝑅)) |
| 20 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) |
| 21 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) |
| 22 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
| 23 | 4, 5, 19, 20, 21, 22 | funcf2 17913 |
. . . . . . 7
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝑓‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝑓‘𝑦))) |
| 24 | 11, 12, 14, 8, 15 | reschom 17874 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
| 25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑅 = (Hom ‘(𝐷 ↾cat 𝑅))) |
| 26 | 25 | oveqd 7448 |
. . . . . . . 8
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑓‘𝑥)𝑅(𝑓‘𝑦)) = ((𝑓‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝑓‘𝑦))) |
| 27 | 26 | feq3d 6723 |
. . . . . . 7
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥𝑔𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝑓‘𝑥)𝑅(𝑓‘𝑦)) ↔ (𝑥𝑔𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝑓‘𝑥)(Hom ‘(𝐷 ↾cat 𝑅))(𝑓‘𝑦)))) |
| 28 | 23, 27 | mpbird 257 |
. . . . . 6
⊢ (((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥𝑔𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝑓‘𝑥)𝑅(𝑓‘𝑦))) |
| 29 | 4, 5, 6, 8, 18, 28 | funcres2b 17942 |
. . . . 5
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → (𝑓(𝐶 Func 𝐷)𝑔 ↔ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔)) |
| 30 | 3, 29 | mpbird 257 |
. . . 4
⊢ ((𝑅 ∈ (Subcat‘𝐷) ∧ 𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔) → 𝑓(𝐶 Func 𝐷)𝑔) |
| 31 | 30 | ex 412 |
. . 3
⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔 → 𝑓(𝐶 Func 𝐷)𝑔)) |
| 32 | | df-br 5144 |
. . 3
⊢ (𝑓(𝐶 Func (𝐷 ↾cat 𝑅))𝑔 ↔ 〈𝑓, 𝑔〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅))) |
| 33 | | df-br 5144 |
. . 3
⊢ (𝑓(𝐶 Func 𝐷)𝑔 ↔ 〈𝑓, 𝑔〉 ∈ (𝐶 Func 𝐷)) |
| 34 | 31, 32, 33 | 3imtr3g 295 |
. 2
⊢ (𝑅 ∈ (Subcat‘𝐷) → (〈𝑓, 𝑔〉 ∈ (𝐶 Func (𝐷 ↾cat 𝑅)) → 〈𝑓, 𝑔〉 ∈ (𝐶 Func 𝐷))) |
| 35 | 2, 34 | relssdv 5798 |
1
⊢ (𝑅 ∈ (Subcat‘𝐷) → (𝐶 Func (𝐷 ↾cat 𝑅)) ⊆ (𝐶 Func 𝐷)) |