Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
⊢ (𝐽 ∈ (Subcat‘𝐷) → 𝐽 ∈ (Subcat‘𝐷)) |
2 | | eqid 2798 |
. . . . . 6
⊢
(Homf ‘𝐷) = (Homf ‘𝐷) |
3 | 1, 2 | subcssc 17102 |
. . . . 5
⊢ (𝐽 ∈ (Subcat‘𝐷) → 𝐽 ⊆cat
(Homf ‘𝐷)) |
4 | | subsubc.d |
. . . . . . 7
⊢ 𝐷 = (𝐶 ↾cat 𝐻) |
5 | | eqid 2798 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
6 | | subcrcl 17078 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat) |
7 | | id 22 |
. . . . . . . 8
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐻 ∈ (Subcat‘𝐶)) |
8 | | eqidd 2799 |
. . . . . . . 8
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom dom 𝐻 = dom dom 𝐻) |
9 | 7, 8 | subcfn 17103 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻)) |
10 | 7, 9, 5 | subcss1 17104 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom dom 𝐻 ⊆ (Base‘𝐶)) |
11 | 4, 5, 6, 9, 10 | reschomf 17093 |
. . . . . 6
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐻 = (Homf ‘𝐷)) |
12 | 11 | breq2d 5042 |
. . . . 5
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ⊆cat 𝐻 ↔ 𝐽 ⊆cat
(Homf ‘𝐷))) |
13 | 3, 12 | syl5ibr 249 |
. . . 4
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) → 𝐽 ⊆cat 𝐻)) |
14 | 13 | pm4.71rd 566 |
. . 3
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐷)))) |
15 | | simpr 488 |
. . . . . . . 8
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 ⊆cat 𝐻) |
16 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐻 ∈ (Subcat‘𝐶)) |
17 | | eqid 2798 |
. . . . . . . . 9
⊢
(Homf ‘𝐶) = (Homf ‘𝐶) |
18 | 16, 17 | subcssc 17102 |
. . . . . . . 8
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐻 ⊆cat
(Homf ‘𝐶)) |
19 | | ssctr 17087 |
. . . . . . . 8
⊢ ((𝐽 ⊆cat 𝐻 ∧ 𝐻 ⊆cat
(Homf ‘𝐶)) → 𝐽 ⊆cat
(Homf ‘𝐶)) |
20 | 15, 18, 19 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 ⊆cat
(Homf ‘𝐶)) |
21 | 12 | biimpa 480 |
. . . . . . 7
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 ⊆cat
(Homf ‘𝐷)) |
22 | 20, 21 | 2thd 268 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ⊆cat
(Homf ‘𝐶) ↔ 𝐽 ⊆cat
(Homf ‘𝐷))) |
23 | 16 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → 𝐻 ∈ (Subcat‘𝐶)) |
24 | 9 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻)) |
25 | 24 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻)) |
26 | | eqid 2798 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
27 | | eqidd 2799 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → dom dom 𝐽 = dom dom 𝐽) |
28 | 15, 27 | sscfn1 17079 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 Fn (dom dom 𝐽 × dom dom 𝐽)) |
29 | 28, 24, 15 | ssc1 17083 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → dom dom 𝐽 ⊆ dom dom 𝐻) |
30 | 29 | sselda 3915 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → 𝑥 ∈ dom dom 𝐻) |
31 | 4, 23, 25, 26, 30 | subcid 17109 |
. . . . . . . 8
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → ((Id‘𝐶)‘𝑥) = ((Id‘𝐷)‘𝑥)) |
32 | 31 | eleq1d 2874 |
. . . . . . 7
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → (((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥))) |
33 | 32 | ralbidva 3161 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (∀𝑥 ∈ dom dom 𝐽((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥))) |
34 | 4 | oveq1i 7145 |
. . . . . . . 8
⊢ (𝐷 ↾cat 𝐽) = ((𝐶 ↾cat 𝐻) ↾cat 𝐽) |
35 | 6 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐶 ∈ Cat) |
36 | | dmexg 7594 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom 𝐻 ∈ V) |
37 | 36 | dmexd 7596 |
. . . . . . . . . 10
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom dom 𝐻 ∈ V) |
38 | 37 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → dom dom 𝐻 ∈ V) |
39 | 35, 24, 28, 38, 29 | rescabs 17095 |
. . . . . . . 8
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) |
40 | 34, 39 | syl5req 2846 |
. . . . . . 7
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐶 ↾cat 𝐽) = (𝐷 ↾cat 𝐽)) |
41 | 40 | eleq1d 2874 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → ((𝐶 ↾cat 𝐽) ∈ Cat ↔ (𝐷 ↾cat 𝐽) ∈ Cat)) |
42 | 22, 33, 41 | 3anbi123d 1433 |
. . . . 5
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → ((𝐽 ⊆cat
(Homf ‘𝐶) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat) ↔ (𝐽 ⊆cat
(Homf ‘𝐷) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐷 ↾cat 𝐽) ∈ Cat))) |
43 | | eqid 2798 |
. . . . . 6
⊢ (𝐶 ↾cat 𝐽) = (𝐶 ↾cat 𝐽) |
44 | 17, 26, 43, 35, 28 | issubc3 17111 |
. . . . 5
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat
(Homf ‘𝐶) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))) |
45 | | eqid 2798 |
. . . . . 6
⊢
(Id‘𝐷) =
(Id‘𝐷) |
46 | | eqid 2798 |
. . . . . 6
⊢ (𝐷 ↾cat 𝐽) = (𝐷 ↾cat 𝐽) |
47 | 4, 7 | subccat 17110 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐷 ∈ Cat) |
48 | 47 | adantr 484 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐷 ∈ Cat) |
49 | 2, 45, 46, 48, 28 | issubc3 17111 |
. . . . 5
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ⊆cat
(Homf ‘𝐷) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐷 ↾cat 𝐽) ∈ Cat))) |
50 | 42, 44, 49 | 3bitr4rd 315 |
. . . 4
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ∈ (Subcat‘𝐷) ↔ 𝐽 ∈ (Subcat‘𝐶))) |
51 | 50 | pm5.32da 582 |
. . 3
⊢ (𝐻 ∈ (Subcat‘𝐶) → ((𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐷)) ↔ (𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐶)))) |
52 | 14, 51 | bitrd 282 |
. 2
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐶)))) |
53 | 52 | biancomd 467 |
1
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻))) |