Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . 3
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺))) |
3 | | olc 398 |
. . 3
⊢ (𝐹(𝐶 Func 𝐸)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹(𝐶 Func 𝐸)𝐺 → (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺))) |
5 | | funcres2c.a |
. . . . 5
⊢ 𝐴 = (Base‘𝐶) |
6 | | eqid 2610 |
. . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
7 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐷) =
(Base‘𝐷) |
8 | | eqid 2610 |
. . . . . . 7
⊢
(Homf ‘𝐷) = (Homf ‘𝐷) |
9 | | funcres2c.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ Cat) |
10 | | inss2 3796 |
. . . . . . . 8
⊢ (𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷)) |
12 | 7, 8, 9, 11 | fullsubc 16333 |
. . . . . 6
⊢ (𝜑 → ((Homf
‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) ∈ (Subcat‘𝐷)) |
13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ((Homf
‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) ∈ (Subcat‘𝐷)) |
14 | 8, 7 | homffn 16176 |
. . . . . . 7
⊢
(Homf ‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)) |
15 | | xpss12 5148 |
. . . . . . . 8
⊢ (((𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷) ∧ (𝑆 ∩ (Base‘𝐷)) ⊆ (Base‘𝐷)) → ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))) ⊆ ((Base‘𝐷) × (Base‘𝐷))) |
16 | 10, 10, 15 | mp2an 704 |
. . . . . . 7
⊢ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))) ⊆ ((Base‘𝐷) × (Base‘𝐷)) |
17 | | fnssres 5918 |
. . . . . . 7
⊢
(((Homf ‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)) ∧ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))) ⊆ ((Base‘𝐷) × (Base‘𝐷))) → ((Homf
‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) Fn ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))) |
18 | 14, 16, 17 | mp2an 704 |
. . . . . 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 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝑆 → 𝐹 Fn 𝐴) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐹 Fn 𝐴) |
24 | | frn 5966 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝑆 → ran 𝐹 ⊆ 𝑆) |
25 | 21, 24 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ran 𝐹 ⊆ 𝑆) |
26 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝐹(𝐶 Func 𝐷)𝐺) |
27 | 5, 7, 26 | funcf1 16349 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝐹:𝐴⟶(Base‘𝐷)) |
28 | | frn 5966 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶(Base‘𝐷) → ran 𝐹 ⊆ (Base‘𝐷)) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐷)𝐺) → ran 𝐹 ⊆ (Base‘𝐷)) |
30 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝐸) =
(Base‘𝐸) |
31 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐹(𝐶 Func 𝐸)𝐺) |
32 | 5, 30, 31 | funcf1 16349 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐹:𝐴⟶(Base‘𝐸)) |
33 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶(Base‘𝐸) → ran 𝐹 ⊆ (Base‘𝐸)) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ran 𝐹 ⊆ (Base‘𝐸)) |
35 | | funcres2c.e |
. . . . . . . . . 10
⊢ 𝐸 = (𝐷 ↾s 𝑆) |
36 | 35, 7 | ressbasss 15759 |
. . . . . . . . 9
⊢
(Base‘𝐸)
⊆ (Base‘𝐷) |
37 | 34, 36 | syl6ss 3580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ran 𝐹 ⊆ (Base‘𝐷)) |
38 | 29, 37 | jaodan 822 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ran 𝐹 ⊆ (Base‘𝐷)) |
39 | 25, 38 | ssind 3799 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → ran 𝐹 ⊆ (𝑆 ∩ (Base‘𝐷))) |
40 | | df-f 5808 |
. . . . . 6
⊢ (𝐹:𝐴⟶(𝑆 ∩ (Base‘𝐷)) ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ (𝑆 ∩ (Base‘𝐷)))) |
41 | 23, 39, 40 | sylanbrc 695 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐹:𝐴⟶(𝑆 ∩ (Base‘𝐷))) |
42 | | eqid 2610 |
. . . . . . . . 9
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
43 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝐹(𝐶 Func 𝐷)𝐺) |
44 | | simplrl 796 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝑥 ∈ 𝐴) |
45 | | simplrr 797 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → 𝑦 ∈ 𝐴) |
46 | 5, 6, 42, 43, 44, 45 | funcf2 16351 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
47 | | eqid 2610 |
. . . . . . . . . 10
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
48 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐹(𝐶 Func 𝐸)𝐺) |
49 | | simplrl 796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝑥 ∈ 𝐴) |
50 | | simplrr 797 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → 𝑦 ∈ 𝐴) |
51 | 5, 6, 47, 48, 49, 50 | funcf2 16351 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐸)(𝐹‘𝑦))) |
52 | | funcres2c.r |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
53 | 35, 42 | resshom 15901 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑉 → (Hom ‘𝐷) = (Hom ‘𝐸)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Hom ‘𝐷) = (Hom ‘𝐸)) |
55 | 54 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → (Hom ‘𝐷) = (Hom ‘𝐸)) |
56 | 55 | oveqd 6566 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘𝐸)(𝐹‘𝑦))) |
57 | 56 | feq3d 5945 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → ((𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐸)(𝐹‘𝑦)))) |
58 | 51, 57 | mpbird 246 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ 𝐹(𝐶 Func 𝐸)𝐺) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
59 | 46, 58 | jaodan 822 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
60 | 59 | an32s 842 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
61 | 41 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝐹:𝐴⟶(𝑆 ∩ (Base‘𝐷))) |
62 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ 𝐴) |
63 | 61, 62 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑥) ∈ (𝑆 ∩ (Base‘𝐷))) |
64 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑦 ∈ 𝐴) |
65 | 61, 64 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑦) ∈ (𝑆 ∩ (Base‘𝐷))) |
66 | 63, 65 | ovresd 6699 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦)) = ((𝐹‘𝑥)(Homf ‘𝐷)(𝐹‘𝑦))) |
67 | 10, 63 | sseldi 3566 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑥) ∈ (Base‘𝐷)) |
68 | 10, 65 | sseldi 3566 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝐹‘𝑦) ∈ (Base‘𝐷)) |
69 | 8, 7, 42, 67, 68 | homfval 16175 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)(Homf ‘𝐷)(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
70 | 66, 69 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦)) = ((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦))) |
71 | 70 | feq3d 5945 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦)) ↔ (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝐷)(𝐹‘𝑦)))) |
72 | 60, 71 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝐺𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶((𝐹‘𝑥)((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))(𝐹‘𝑦))) |
73 | 5, 6, 13, 19, 41, 72 | funcres2b 16380 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))𝐺)) |
74 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (Homf
‘𝐶) =
(Homf ‘𝐶)) |
75 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) →
(compf‘𝐶) = (compf‘𝐶)) |
76 | 7 | ressinbas 15763 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ 𝑉 → (𝐷 ↾s 𝑆) = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) |
77 | 52, 76 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ↾s 𝑆) = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) |
78 | 35, 77 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) |
79 | 78 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → (Homf
‘𝐸) =
(Homf ‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷))))) |
80 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝐷 ↾s (𝑆 ∩ (Base‘𝐷))) = (𝐷 ↾s (𝑆 ∩ (Base‘𝐷))) |
81 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))) = (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))) |
82 | 7, 8, 9, 11, 80, 81 | fullresc 16334 |
. . . . . . . . 9
⊢ (𝜑 → ((Homf
‘(𝐷
↾s (𝑆
∩ (Base‘𝐷)))) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))))) ∧
(compf‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷)))))))) |
83 | 82 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → (Homf
‘(𝐷
↾s (𝑆
∩ (Base‘𝐷)))) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
84 | 79, 83 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (Homf
‘𝐸) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
85 | 84 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (Homf
‘𝐸) =
(Homf ‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
86 | 78 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 →
(compf‘𝐸) = (compf‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷))))) |
87 | 82 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 →
(compf‘(𝐷 ↾s (𝑆 ∩ (Base‘𝐷)))) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
88 | 86, 87 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 →
(compf‘𝐸) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
89 | 88 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) →
(compf‘𝐸) = (compf‘(𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
90 | | df-br 4584 |
. . . . . . . . . . 11
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
91 | | funcrcl 16346 |
. . . . . . . . . . 11
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
92 | 90, 91 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
93 | 92 | simpld 474 |
. . . . . . . . 9
⊢ (𝐹(𝐶 Func 𝐷)𝐺 → 𝐶 ∈ Cat) |
94 | | df-br 4584 |
. . . . . . . . . . 11
⊢ (𝐹(𝐶 Func 𝐸)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐸)) |
95 | | funcrcl 16346 |
. . . . . . . . . . 11
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
96 | 94, 95 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝐹(𝐶 Func 𝐸)𝐺 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
97 | 96 | simpld 474 |
. . . . . . . . 9
⊢ (𝐹(𝐶 Func 𝐸)𝐺 → 𝐶 ∈ Cat) |
98 | 93, 97 | jaoi 393 |
. . . . . . . 8
⊢ ((𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐶 ∈ Cat) |
99 | | elex 3185 |
. . . . . . . 8
⊢ (𝐶 ∈ Cat → 𝐶 ∈ V) |
100 | 98, 99 | syl 17 |
. . . . . . 7
⊢ ((𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺) → 𝐶 ∈ V) |
101 | 100 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐶 ∈ V) |
102 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐷 ↾s 𝑆) ∈ V |
103 | 35, 102 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐸 ∈ V |
104 | 103 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → 𝐸 ∈ V) |
105 | | ovex 6577 |
. . . . . . 7
⊢ (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))) ∈ V |
106 | 105 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))) ∈ V) |
107 | 74, 75, 85, 89, 101, 101, 104, 106 | funcpropd 16383 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐶 Func 𝐸) = (𝐶 Func (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))) |
108 | 107 | breqd 4594 |
. . . 4
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐹(𝐶 Func 𝐸)𝐺 ↔ 𝐹(𝐶 Func (𝐷 ↾cat
((Homf ‘𝐷) ↾ ((𝑆 ∩ (Base‘𝐷)) × (𝑆 ∩ (Base‘𝐷))))))𝐺)) |
109 | 73, 108 | bitr4d 270 |
. . 3
⊢ ((𝜑 ∧ (𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺)) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺)) |
110 | 109 | ex 449 |
. 2
⊢ (𝜑 → ((𝐹(𝐶 Func 𝐷)𝐺 ∨ 𝐹(𝐶 Func 𝐸)𝐺) → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺))) |
111 | 2, 4, 110 | pm5.21ndd 368 |
1
⊢ (𝜑 → (𝐹(𝐶 Func 𝐷)𝐺 ↔ 𝐹(𝐶 Func 𝐸)𝐺)) |