| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) → 𝐽 ∈ (Subcat‘𝐶)) |
| 2 | | issubc3.h |
. . . 4
⊢ 𝐻 = (Homf
‘𝐶) |
| 3 | 1, 2 | subcssc 17885 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) → 𝐽 ⊆cat 𝐻) |
| 4 | 1 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ (Subcat‘𝐶)) |
| 5 | | issubc3.a |
. . . . . 6
⊢ (𝜑 → 𝐽 Fn (𝑆 × 𝑆)) |
| 6 | 5 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) ∧ 𝑥 ∈ 𝑆) → 𝐽 Fn (𝑆 × 𝑆)) |
| 7 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 8 | | issubc3.i |
. . . . 5
⊢ 1 =
(Id‘𝐶) |
| 9 | 4, 6, 7, 8 | subcidcl 17889 |
. . . 4
⊢ (((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) ∧ 𝑥 ∈ 𝑆) → ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥)) |
| 10 | 9 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) → ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥)) |
| 11 | | issubc3.1 |
. . . 4
⊢ 𝐷 = (𝐶 ↾cat 𝐽) |
| 12 | 11, 1 | subccat 17893 |
. . 3
⊢ ((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) → 𝐷 ∈ Cat) |
| 13 | 3, 10, 12 | 3jca 1129 |
. 2
⊢ ((𝜑 ∧ 𝐽 ∈ (Subcat‘𝐶)) → (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) |
| 14 | | simpr1 1195 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → 𝐽 ⊆cat 𝐻) |
| 15 | | simpr2 1196 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥)) |
| 16 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 17 | | eqid 2737 |
. . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 18 | | eqid 2737 |
. . . . . . . . . 10
⊢
(comp‘𝐷) =
(comp‘𝐷) |
| 19 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝐷 ∈ Cat) |
| 20 | | simprl1 1219 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑥 ∈ 𝑆) |
| 21 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 22 | | issubc3.c |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 23 | 22 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝐶 ∈ Cat) |
| 24 | 5 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝐽 Fn (𝑆 × 𝑆)) |
| 25 | 2, 21 | homffn 17736 |
. . . . . . . . . . . . . 14
⊢ 𝐻 Fn ((Base‘𝐶) × (Base‘𝐶)) |
| 26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝐻 Fn ((Base‘𝐶) × (Base‘𝐶))) |
| 27 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝐽 ⊆cat 𝐻) |
| 28 | 24, 26, 27 | ssc1 17865 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑆 ⊆ (Base‘𝐶)) |
| 29 | 11, 21, 23, 24, 28 | rescbas 17873 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑆 = (Base‘𝐷)) |
| 30 | 20, 29 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑥 ∈ (Base‘𝐷)) |
| 31 | | simprl2 1220 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑦 ∈ 𝑆) |
| 32 | 31, 29 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑦 ∈ (Base‘𝐷)) |
| 33 | | simprl3 1221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑧 ∈ 𝑆) |
| 34 | 33, 29 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑧 ∈ (Base‘𝐷)) |
| 35 | | simprrl 781 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑓 ∈ (𝑥𝐽𝑦)) |
| 36 | 11, 21, 23, 24, 28 | reschom 17874 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝐽 = (Hom ‘𝐷)) |
| 37 | 36 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (𝑥𝐽𝑦) = (𝑥(Hom ‘𝐷)𝑦)) |
| 38 | 35, 37 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)) |
| 39 | | simprrr 782 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑔 ∈ (𝑦𝐽𝑧)) |
| 40 | 36 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (𝑦𝐽𝑧) = (𝑦(Hom ‘𝐷)𝑧)) |
| 41 | 39, 40 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) |
| 42 | 16, 17, 18, 19, 30, 32, 34, 38, 41 | catcocl 17728 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐷)𝑧)) |
| 43 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 44 | 11, 21, 23, 24, 28, 43 | rescco 17876 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (comp‘𝐶) = (comp‘𝐷)) |
| 45 | 44 | oveqd 7448 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (〈𝑥, 𝑦〉(comp‘𝐶)𝑧) = (〈𝑥, 𝑦〉(comp‘𝐷)𝑧)) |
| 46 | 45 | oveqd 7448 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓)) |
| 47 | 36 | oveqd 7448 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (𝑥𝐽𝑧) = (𝑥(Hom ‘𝐷)𝑧)) |
| 48 | 42, 46, 47 | 3eltr4d 2856 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 49 | 48 | anassrs 467 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ (𝑓 ∈ (𝑥𝐽𝑦) ∧ 𝑔 ∈ (𝑦𝐽𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 50 | 49 | ralrimivva 3202 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 51 | 50 | ralrimivvva 3205 |
. . . . 5
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ 𝐷 ∈ Cat)) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 52 | 51 | 3adantr2 1171 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)) |
| 53 | | r19.26 3111 |
. . . 4
⊢
(∀𝑥 ∈
𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧)) ↔ (∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
| 54 | 15, 52, 53 | sylanbrc 583 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))) |
| 55 | 22 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → 𝐶 ∈ Cat) |
| 56 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → 𝐽 Fn (𝑆 × 𝑆)) |
| 57 | 2, 8, 43, 55, 56 | issubc2 17881 |
. . 3
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 (( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑆 ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥𝐽𝑧))))) |
| 58 | 14, 54, 57 | mpbir2and 713 |
. 2
⊢ ((𝜑 ∧ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat)) → 𝐽 ∈ (Subcat‘𝐶)) |
| 59 | 13, 58 | impbida 801 |
1
⊢ (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽 ⊆cat 𝐻 ∧ ∀𝑥 ∈ 𝑆 ( 1 ‘𝑥) ∈ (𝑥𝐽𝑥) ∧ 𝐷 ∈ Cat))) |