Step | Hyp | Ref
| Expression |
1 | | oveq1 7178 |
. . . 4
⊢ (𝑐 = 𝐶 → (𝑐 Full 𝑑) = (𝐶 Full 𝑑)) |
2 | | oveq1 7178 |
. . . 4
⊢ (𝑐 = 𝐶 → (𝑐 Func 𝑑) = (𝐶 Func 𝑑)) |
3 | 1, 2 | sseq12d 3911 |
. . 3
⊢ (𝑐 = 𝐶 → ((𝑐 Full 𝑑) ⊆ (𝑐 Func 𝑑) ↔ (𝐶 Full 𝑑) ⊆ (𝐶 Func 𝑑))) |
4 | | oveq2 7179 |
. . . 4
⊢ (𝑑 = 𝐷 → (𝐶 Full 𝑑) = (𝐶 Full 𝐷)) |
5 | | oveq2 7179 |
. . . 4
⊢ (𝑑 = 𝐷 → (𝐶 Func 𝑑) = (𝐶 Func 𝐷)) |
6 | 4, 5 | sseq12d 3911 |
. . 3
⊢ (𝑑 = 𝐷 → ((𝐶 Full 𝑑) ⊆ (𝐶 Func 𝑑) ↔ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷))) |
7 | | ovex 7204 |
. . . . . 6
⊢ (𝑐 Func 𝑑) ∈ V |
8 | | simpl 486 |
. . . . . . . 8
⊢ ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))) → 𝑓(𝑐 Func 𝑑)𝑔) |
9 | 8 | ssopab2i 5406 |
. . . . . . 7
⊢
{〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ⊆ {〈𝑓, 𝑔〉 ∣ 𝑓(𝑐 Func 𝑑)𝑔} |
10 | | opabss 5095 |
. . . . . . 7
⊢
{〈𝑓, 𝑔〉 ∣ 𝑓(𝑐 Func 𝑑)𝑔} ⊆ (𝑐 Func 𝑑) |
11 | 9, 10 | sstri 3887 |
. . . . . 6
⊢
{〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ⊆ (𝑐 Func 𝑑) |
12 | 7, 11 | ssexi 5191 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ∈ V |
13 | | df-full 17280 |
. . . . . 6
⊢ Full =
(𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}) |
14 | 13 | ovmpt4g 7313 |
. . . . 5
⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ∧ {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ∈ V) → (𝑐 Full 𝑑) = {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}) |
15 | 12, 14 | mp3an3 1451 |
. . . 4
⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat) → (𝑐 Full 𝑑) = {〈𝑓, 𝑔〉 ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))}) |
16 | 15, 11 | eqsstrdi 3932 |
. . 3
⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat) → (𝑐 Full 𝑑) ⊆ (𝑐 Func 𝑑)) |
17 | 3, 6, 16 | vtocl2ga 3480 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)) |
18 | 13 | mpondm0 7403 |
. . 3
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) = ∅) |
19 | | 0ss 4286 |
. . 3
⊢ ∅
⊆ (𝐶 Func 𝐷) |
20 | 18, 19 | eqsstrdi 3932 |
. 2
⊢ (¬
(𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)) |
21 | 17, 20 | pm2.61i 185 |
1
⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷) |