Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . 6
⊢ (𝐽 ∈ (Subcat‘𝐷) → 𝐽 ∈ (Subcat‘𝐷)) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Homf ‘𝐷) = (Homf ‘𝐷) |
3 | 1, 2 | subcssc 16500 |
. . . . 5
⊢ (𝐽 ∈ (Subcat‘𝐷) → 𝐽 ⊆cat
(Homf ‘𝐷)) |
4 | | subsubc.d |
. . . . . . 7
⊢ 𝐷 = (𝐶 ↾cat 𝐻) |
5 | | eqid 2622 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
6 | | subcrcl 16476 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐶 ∈ Cat) |
7 | | id 22 |
. . . . . . . 8
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐻 ∈ (Subcat‘𝐶)) |
8 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom dom 𝐻 = dom dom 𝐻) |
9 | 7, 8 | subcfn 16501 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻)) |
10 | 7, 9, 5 | subcss1 16502 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom dom 𝐻 ⊆ (Base‘𝐶)) |
11 | 4, 5, 6, 9, 10 | reschomf 16491 |
. . . . . 6
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐻 = (Homf ‘𝐷)) |
12 | 11 | breq2d 4665 |
. . . . 5
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ⊆cat 𝐻 ↔ 𝐽 ⊆cat
(Homf ‘𝐷))) |
13 | 3, 12 | syl5ibr 236 |
. . . 4
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) → 𝐽 ⊆cat 𝐻)) |
14 | 13 | pm4.71rd 667 |
. . 3
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐷)))) |
15 | | simpr 477 |
. . . . . . . 8
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 ⊆cat 𝐻) |
16 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐻 ∈ (Subcat‘𝐶)) |
17 | | eqid 2622 |
. . . . . . . . 9
⊢
(Homf ‘𝐶) = (Homf ‘𝐶) |
18 | 16, 17 | subcssc 16500 |
. . . . . . . 8
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐻 ⊆cat
(Homf ‘𝐶)) |
19 | | ssctr 16485 |
. . . . . . . 8
⊢ ((𝐽 ⊆cat 𝐻 ∧ 𝐻 ⊆cat
(Homf ‘𝐶)) → 𝐽 ⊆cat
(Homf ‘𝐶)) |
20 | 15, 18, 19 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 ⊆cat
(Homf ‘𝐶)) |
21 | 12 | biimpa 501 |
. . . . . . 7
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 ⊆cat
(Homf ‘𝐷)) |
22 | 20, 21 | 2thd 255 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ⊆cat
(Homf ‘𝐶) ↔ 𝐽 ⊆cat
(Homf ‘𝐷))) |
23 | 16 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → 𝐻 ∈ (Subcat‘𝐶)) |
24 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻)) |
25 | 24 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → 𝐻 Fn (dom dom 𝐻 × dom dom 𝐻)) |
26 | | eqid 2622 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
27 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → dom dom 𝐽 = dom dom 𝐽) |
28 | 15, 27 | sscfn1 16477 |
. . . . . . . . . . 11
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐽 Fn (dom dom 𝐽 × dom dom 𝐽)) |
29 | 28, 24, 15 | ssc1 16481 |
. . . . . . . . . 10
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → dom dom 𝐽 ⊆ dom dom 𝐻) |
30 | 29 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → 𝑥 ∈ dom dom 𝐻) |
31 | 4, 23, 25, 26, 30 | subcid 16507 |
. . . . . . . 8
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → ((Id‘𝐶)‘𝑥) = ((Id‘𝐷)‘𝑥)) |
32 | 31 | eleq1d 2686 |
. . . . . . 7
⊢ (((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) ∧ 𝑥 ∈ dom dom 𝐽) → (((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥))) |
33 | 32 | ralbidva 2985 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (∀𝑥 ∈ dom dom 𝐽((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ↔ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥))) |
34 | 4 | oveq1i 6660 |
. . . . . . . 8
⊢ (𝐷 ↾cat 𝐽) = ((𝐶 ↾cat 𝐻) ↾cat 𝐽) |
35 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐶 ∈ Cat) |
36 | | dmexg 7097 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom 𝐻 ∈ V) |
37 | | dmexg 7097 |
. . . . . . . . . . 11
⊢ (dom
𝐻 ∈ V → dom dom
𝐻 ∈
V) |
38 | 36, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝐻 ∈ (Subcat‘𝐶) → dom dom 𝐻 ∈ V) |
39 | 38 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → dom dom 𝐻 ∈ V) |
40 | 35, 24, 28, 39, 29 | rescabs 16493 |
. . . . . . . 8
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → ((𝐶 ↾cat 𝐻) ↾cat 𝐽) = (𝐶 ↾cat 𝐽)) |
41 | 34, 40 | syl5req 2669 |
. . . . . . 7
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐶 ↾cat 𝐽) = (𝐷 ↾cat 𝐽)) |
42 | 41 | eleq1d 2686 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → ((𝐶 ↾cat 𝐽) ∈ Cat ↔ (𝐷 ↾cat 𝐽) ∈ Cat)) |
43 | 22, 33, 42 | 3anbi123d 1399 |
. . . . 5
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → ((𝐽 ⊆cat
(Homf ‘𝐶) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat) ↔ (𝐽 ⊆cat
(Homf ‘𝐷) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐷 ↾cat 𝐽) ∈ Cat))) |
44 | | eqid 2622 |
. . . . . 6
⊢ (𝐶 ↾cat 𝐽) = (𝐶 ↾cat 𝐽) |
45 | 17, 26, 44, 35, 28 | issubc3 16509 |
. . . . 5
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat
(Homf ‘𝐶) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐶)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐶 ↾cat 𝐽) ∈ Cat))) |
46 | | eqid 2622 |
. . . . . 6
⊢
(Id‘𝐷) =
(Id‘𝐷) |
47 | | eqid 2622 |
. . . . . 6
⊢ (𝐷 ↾cat 𝐽) = (𝐷 ↾cat 𝐽) |
48 | 4, 7 | subccat 16508 |
. . . . . . 7
⊢ (𝐻 ∈ (Subcat‘𝐶) → 𝐷 ∈ Cat) |
49 | 48 | adantr 481 |
. . . . . 6
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → 𝐷 ∈ Cat) |
50 | 2, 46, 47, 49, 28 | issubc3 16509 |
. . . . 5
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ⊆cat
(Homf ‘𝐷) ∧ ∀𝑥 ∈ dom dom 𝐽((Id‘𝐷)‘𝑥) ∈ (𝑥𝐽𝑥) ∧ (𝐷 ↾cat 𝐽) ∈ Cat))) |
51 | 43, 45, 50 | 3bitr4rd 301 |
. . . 4
⊢ ((𝐻 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻) → (𝐽 ∈ (Subcat‘𝐷) ↔ 𝐽 ∈ (Subcat‘𝐶))) |
52 | 51 | pm5.32da 673 |
. . 3
⊢ (𝐻 ∈ (Subcat‘𝐶) → ((𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐷)) ↔ (𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐶)))) |
53 | 14, 52 | bitrd 268 |
. 2
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐶)))) |
54 | | ancom 466 |
. 2
⊢ ((𝐽 ⊆cat 𝐻 ∧ 𝐽 ∈ (Subcat‘𝐶)) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻)) |
55 | 53, 54 | syl6bb 276 |
1
⊢ (𝐻 ∈ (Subcat‘𝐶) → (𝐽 ∈ (Subcat‘𝐷) ↔ (𝐽 ∈ (Subcat‘𝐶) ∧ 𝐽 ⊆cat 𝐻))) |