| Step | Hyp | Ref
| Expression |
| 1 | | orc 868 |
. . 3
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺))) |
| 3 | | olc 869 |
. . 3
⊢ (𝐹(𝐶 Func 𝐸)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func 𝐸)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺))) |
| 5 | | funcres2c.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
| 6 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 7 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 8 | | eqid 2737 |
. . . . . . 7
⊢
(Homf ‘𝐷) = (Homf ‘𝐷) |
| 9 | | funcres2c.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 10 | | inss2 4238 |
. . . . . . . 8
⊢ (𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷) |
| 11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷)) |
| 12 | 7, 8, 9, 11 | fullsubc 17895 |
. . . . . 6
⊢ (𝜑 → ((Homf
‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) ∈ (Subcat‘𝐷)) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ((Homf
‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) ∈ (Subcat‘𝐷)) |
| 14 | 8, 7 | homffn 17736 |
. . . . . . 7
⊢
(Homf ‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)) |
| 15 | | xpss12 5700 |
. . . . . . . 8
⊢ (((𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷) ∧ (𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷)) → ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))) ⊆ ((Base‘𝐷) × (Base‘𝐷))) |
| 16 | 10, 10, 15 | mp2an 692 |
. . . . . . 7
⊢ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))) ⊆ ((Base‘𝐷) × (Base‘𝐷)) |
| 17 | | fnssres 6691 |
. . . . . . 7
⊢
(((Homf ‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)) ∧ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))) ⊆ ((Base‘𝐷) × (Base‘𝐷))) → ((Homf
‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) Fn ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) |
| 18 | 14, 16, 17 | mp2an 692 |
. . . . . 6
⊢
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) Fn ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))) |
| 19 | 18 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ((Homf
‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) Fn ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) |
| 20 | | funcres2c.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
| 21 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐹:𝐴⟶𝑆) |
| 22 | 21 | ffnd 6737 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐹 Fn 𝐴) |
| 23 | 21 | frnd 6744 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ran 𝐹 ⊆ 𝑆) |
| 24 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝐹(𝐶 Func 𝐷)𝐺) |
| 25 | 5, 7, 24 | funcf1 17911 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝐹:𝐴⟶(Base‘𝐷)) |
| 26 | 25 | frnd 6744 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐷)𝐺) → ran 𝐹 ⊆ (Base‘𝐷)) |
| 27 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐸) =
(Base‘𝐸) |
| 28 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐹(𝐶 Func 𝐸)𝐺) |
| 29 | 5, 27, 28 | funcf1 17911 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐹:𝐴⟶(Base‘𝐸)) |
| 30 | 29 | frnd 6744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ran 𝐹 ⊆ (Base‘𝐸)) |
| 31 | | funcres2c.e |
. . . . . . . . . 10
⊢ 𝐸 = (𝐷 ↾s 𝑆) |
| 32 | 31, 7 | ressbasss 17284 |
. . . . . . . . 9
⊢
(Base‘𝐸)
⊆ (Base‘𝐷) |
| 33 | 30, 32 | sstrdi 3996 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ran 𝐹 ⊆ (Base‘𝐷)) |
| 34 | 26, 33 | jaodan 960 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ran 𝐹 ⊆ (Base‘𝐷)) |
| 35 | 23, 34 | ssind 4241 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ran 𝐹 ⊆ (𝑆 ∩ (Base‘𝐷))) |
| 36 | | df-f 6565 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝑆 ∩ (Base‘𝐷)) ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ (𝑆 ∩ (Base‘𝐷)))) |
| 37 | 22, 35, 36 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐹:𝐴⟶(𝑆 ∩ (Base‘𝐷))) |
| 38 | | eqid 2737 |
. . . . . . . . 9
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 39 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝐹(𝐶 Func 𝐷)𝐺) |
| 40 | | simplrl 777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝑥 ∈ 𝐴) |
| 41 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝑦 ∈ 𝐴) |
| 42 | 5, 6, 38, 39, 40, 41 | funcf2 17913 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 43 | | eqid 2737 |
. . . . . . . . . 10
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
| 44 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐹(𝐶 Func 𝐸)𝐺) |
| 45 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝑥 ∈ 𝐴) |
| 46 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝑦 ∈ 𝐴) |
| 47 | 5, 6, 43, 44, 45, 46 | funcf2 17913 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐸)(𝐹‘𝑦))) |
| 48 | | funcres2c.r |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
| 49 | 31, 38 | resshom 17463 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑉 → (Hom ‘𝐷) = (Hom ‘𝐸)) |
| 50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Hom ‘𝐷) = (Hom ‘𝐸)) |
| 51 | 50 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → (Hom ‘𝐷) = (Hom ‘𝐸)) |
| 52 | 51 | oveqd 7448 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘𝐸)(𝐹‘𝑦))) |
| 53 | 52 | feq3d 6723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ((𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐸)(𝐹‘𝑦)))) |
| 54 | 47, 53 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 55 | 42, 54 | jaodan 960 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 56 | 55 | an32s 652 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 57 | 37 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝐹:𝐴⟶(𝑆 ∩ (Base‘𝐷))) |
| 58 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
| 59 | 57, 58 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑥) ∈ (𝑆 ∩ (Base‘𝐷))) |
| 60 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
| 61 | 57, 60 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑦) ∈ (𝑆 ∩ (Base‘𝐷))) |
| 62 | 59, 61 | ovresd 7600 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦)) = ((𝐹‘𝑥)(Homf ‘𝐷)(𝐹‘𝑦))) |
| 63 | 59 | elin2d 4205 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑥) ∈ (Base‘𝐷)) |
| 64 | 61 | elin2d 4205 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑦) ∈ (Base‘𝐷)) |
| 65 | 8, 7, 38, 63, 64 | homfval 17735 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)(Homf ‘𝐷)(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 66 | 62, 65 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
| 67 | 66 | feq3d 6723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
| 68 | 56, 67 | mpbird 257 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦))) |
| 69 | 5, 6, 13, 19, 37, 68 | funcres2b 17942 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))𝐺)) |
| 70 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (Homf
‘𝐶) =
(Homf ‘𝐶)) |
| 71 | | eqidd 2738 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) →
(compf‘𝐶) = (compf‘𝐶)) |
| 72 | 7 | ressinbas 17291 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ 𝑉 → (𝐷 ↾s 𝑆) = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) |
| 73 | 48, 72 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ↾s 𝑆) = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) |
| 74 | 31, 73 | eqtrid 2789 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) |
| 75 | 74 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 → (Homf
‘𝐸) =
(Homf ‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷))))) |
| 76 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝐷 ↾s (𝑆 ∩ (Base‘𝐷))) = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷))) |
| 77 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))) = (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))) |
| 78 | 7, 8, 9, 11, 76, 77 | fullresc 17896 |
. . . . . . . . 9
⊢ (𝜑 → ((Homf
‘(𝐷
↾s (𝑆
∩ (Base‘𝐷)))) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))))) ∧
(compf‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))))))) |
| 79 | 78 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → (Homf
‘(𝐷
↾s (𝑆
∩ (Base‘𝐷)))) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
| 80 | 75, 79 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (Homf
‘𝐸) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
| 81 | 80 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (Homf
‘𝐸) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
| 82 | 74 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 →
(compf‘𝐸) = (compf‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷))))) |
| 83 | 78 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 →
(compf‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
| 84 | 82, 83 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 →
(compf‘𝐸) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
| 85 | 84 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) →
(compf‘𝐸) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
| 86 | | df-br 5144 |
. . . . . . . . . . 11
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
| 87 | | funcrcl 17908 |
. . . . . . . . . . 11
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 88 | 86, 87 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
| 89 | 88 | simpld 494 |
. . . . . . . . 9
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat) |
| 90 | | df-br 5144 |
. . . . . . . . . . 11
⊢ (𝐹(𝐶 Func 𝐸)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐸)) |
| 91 | | funcrcl 17908 |
. . . . . . . . . . 11
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
| 92 | 90, 91 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝐹(𝐶 Func 𝐸)𝐺 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
| 93 | 92 | simpld 494 |
. . . . . . . . 9
⊢ (𝐹(𝐶 Func 𝐸)𝐺 → 𝐶 ∈ Cat) |
| 94 | 89, 93 | jaoi 858 |
. . . . . . . 8
⊢ ((𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐶 ∈ Cat) |
| 95 | 94 | elexd 3504 |
. . . . . . 7
⊢ ((𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐶 ∈ V) |
| 96 | 95 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐶 ∈ V) |
| 97 | 31 | ovexi 7465 |
. . . . . . 7
⊢ 𝐸 ∈ V |
| 98 | 97 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐸 ∈ V) |
| 99 | | ovexd 7466 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))) ∈ V) |
| 100 | 70, 71, 81, 85, 96, 96, 98, 99 | funcpropd 17947 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐶 Func 𝐸) = (𝐶 Func (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
| 101 | 100 | breqd 5154 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐹(𝐶 Func 𝐸)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))𝐺)) |
| 102 | 69, 101 | bitr4d 282 |
. . 3
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺)) |
| 103 | 102 | ex 412 |
. 2
⊢ (𝜑 → ((𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺))) |
| 104 | 2, 4, 103 | pm5.21ndd 379 |
1
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺)) |