| Step | Hyp | Ref
| Expression |
| 1 | | uncfval.g |
. . . . . . . . . 10
⊢ 𝐹 = (〈“𝐶𝐷𝐸”〉 uncurryF
𝐺) |
| 2 | | uncfval.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 3 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat) |
| 4 | | uncfval.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ Cat) |
| 5 | 4 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐸 ∈ Cat) |
| 6 | | uncfval.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) |
| 7 | 6 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) |
| 8 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 9 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 10 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶)) |
| 11 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐷)) |
| 12 | 1, 3, 5, 7, 8, 9, 10, 11 | uncf1 18281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷)) → (𝑥(1st ‘𝐹)𝑦) = ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑦)) |
| 13 | 12 | mpteq2dva 5242 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)) = (𝑦 ∈ (Base‘𝐷) ↦ ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦))) |
| 14 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐸) =
(Base‘𝐸) |
| 15 | | relfunc 17907 |
. . . . . . . . . . 11
⊢ Rel
(𝐷 Func 𝐸) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝐷 FuncCat 𝐸) = (𝐷 FuncCat 𝐸) |
| 17 | 16 | fucbas 18008 |
. . . . . . . . . . . . 13
⊢ (𝐷 Func 𝐸) = (Base‘(𝐷 FuncCat 𝐸)) |
| 18 | | relfunc 17907 |
. . . . . . . . . . . . . 14
⊢ Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) |
| 19 | | 1st2ndbr 8067 |
. . . . . . . . . . . . . 14
⊢ ((Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) ∧ 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
| 20 | 18, 6, 19 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
| 21 | 8, 17, 20 | funcf1 17911 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(𝐷 Func 𝐸)) |
| 22 | 21 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) |
| 23 | | 1st2ndbr 8067 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐷 Func 𝐸) ∧ ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) → (1st
‘((1st ‘𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑥))) |
| 24 | 15, 22, 23 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st
‘((1st ‘𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑥))) |
| 25 | 9, 14, 24 | funcf1 17911 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st
‘((1st ‘𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸)) |
| 26 | 25 | feqmptd 6977 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st
‘((1st ‘𝐺)‘𝑥)) = (𝑦 ∈ (Base‘𝐷) ↦ ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦))) |
| 27 | 13, 26 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)) = (1st ‘((1st
‘𝐺)‘𝑥))) |
| 28 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat) |
| 29 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐸 ∈ Cat) |
| 30 | 6 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) |
| 31 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑥 ∈ (Base‘𝐶)) |
| 32 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ (Base‘𝐷)) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 34 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 35 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) → 𝑧 ∈ (Base‘𝐷)) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ (Base‘𝐷)) |
| 37 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Id‘𝐶) =
(Id‘𝐶) |
| 38 | | funcrcl 17908 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸)) → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
| 39 | 6, 38 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 ∈ Cat ∧ (𝐷 FuncCat 𝐸) ∈ Cat)) |
| 40 | 39 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 41 | 40 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat) |
| 42 | 8, 33, 37, 41, 31 | catidcl 17725 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥)) |
| 43 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) |
| 44 | 1, 28, 29, 30, 8, 9, 31, 32, 33, 34, 31, 36, 42, 43 | uncf2 18282 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔) = ((((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))‘𝑧)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧))((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔))) |
| 45 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(Id‘(𝐷 FuncCat
𝐸)) = (Id‘(𝐷 FuncCat 𝐸)) |
| 46 | 20 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
| 47 | 8, 37, 45, 46, 31 | funcid 17915 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘(𝐷 FuncCat 𝐸))‘((1st ‘𝐺)‘𝑥))) |
| 48 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(Id‘𝐸) =
(Id‘𝐸) |
| 49 | 22 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) |
| 50 | 16, 45, 48, 49 | fucid 18019 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘(𝐷 FuncCat 𝐸))‘((1st ‘𝐺)‘𝑥)) = ((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥)))) |
| 51 | 47, 50 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥)))) |
| 52 | 51 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))‘𝑧) = (((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥)))‘𝑧)) |
| 53 | 25 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st
‘((1st ‘𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸)) |
| 54 | | fvco3 7008 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ‘((1st ‘𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸) ∧ 𝑧 ∈ (Base‘𝐷)) → (((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥)))‘𝑧) = ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧))) |
| 55 | 53, 36, 54 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐸) ∘ (1st
‘((1st ‘𝐺)‘𝑥)))‘𝑧) = ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧))) |
| 56 | 52, 55 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))‘𝑧) = ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧))) |
| 57 | 56 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))‘𝑧)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧))((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔)) = (((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧))(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧))((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔))) |
| 58 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
| 59 | 53, 32 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦) ∈ (Base‘𝐸)) |
| 60 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(comp‘𝐸) =
(comp‘𝐸) |
| 61 | 53, 36 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧) ∈ (Base‘𝐸)) |
| 62 | 24 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) → (1st
‘((1st ‘𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑥))) |
| 63 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐷)) |
| 64 | 9, 34, 58, 62, 63, 35 | funcf2 17913 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) → (𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧))) |
| 65 | 64 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔) ∈ (((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧))) |
| 66 | 14, 58, 48, 29, 59, 60, 61, 65 | catlid 17726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧))(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑦), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧))((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔)) = ((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔)) |
| 67 | 44, 57, 66 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔) = ((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔)) |
| 68 | 67 | mpteq2dva 5242 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) → (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ ((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔))) |
| 69 | 64 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) → (𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ ((𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘𝑔))) |
| 70 | 68, 69 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷))) → (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)) = (𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)) |
| 71 | 70 | 3impb 1115 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑦 ∈ (Base‘𝐷) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)) = (𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)) |
| 72 | 71 | mpoeq3dva 7510 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔))) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧))) |
| 73 | 9, 24 | funcfn2 17914 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (2nd
‘((1st ‘𝐺)‘𝑥)) Fn ((Base‘𝐷) × (Base‘𝐷))) |
| 74 | | fnov 7564 |
. . . . . . . . 9
⊢
((2nd ‘((1st ‘𝐺)‘𝑥)) Fn ((Base‘𝐷) × (Base‘𝐷)) ↔ (2nd
‘((1st ‘𝐺)‘𝑥)) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧))) |
| 75 | 73, 74 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (2nd
‘((1st ‘𝐺)‘𝑥)) = (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑦(2nd ‘((1st
‘𝐺)‘𝑥))𝑧))) |
| 76 | 72, 75 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔))) = (2nd ‘((1st
‘𝐺)‘𝑥))) |
| 77 | 27, 76 | opeq12d 4881 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉 = 〈(1st
‘((1st ‘𝐺)‘𝑥)), (2nd ‘((1st
‘𝐺)‘𝑥))〉) |
| 78 | | 1st2nd 8064 |
. . . . . . 7
⊢ ((Rel
(𝐷 Func 𝐸) ∧ ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) → ((1st ‘𝐺)‘𝑥) = 〈(1st
‘((1st ‘𝐺)‘𝑥)), (2nd ‘((1st
‘𝐺)‘𝑥))〉) |
| 79 | 15, 22, 78 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) = 〈(1st
‘((1st ‘𝐺)‘𝑥)), (2nd ‘((1st
‘𝐺)‘𝑥))〉) |
| 80 | 77, 79 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉 = ((1st ‘𝐺)‘𝑥)) |
| 81 | 80 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝐺)‘𝑥))) |
| 82 | 21 | feqmptd 6977 |
. . . 4
⊢ (𝜑 → (1st
‘𝐺) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st
‘𝐺)‘𝑥))) |
| 83 | 81, 82 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉) = (1st ‘𝐺)) |
| 84 | 2 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝐷 ∈ Cat) |
| 85 | 4 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝐸 ∈ Cat) |
| 86 | 6 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) |
| 87 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) |
| 88 | 87 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑥 ∈ (Base‘𝐶)) |
| 89 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑧 ∈ (Base‘𝐷)) |
| 90 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
| 91 | 90 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑦 ∈ (Base‘𝐶)) |
| 92 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
| 93 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Id‘𝐷) =
(Id‘𝐷) |
| 94 | 9, 34, 93, 84, 89 | catidcl 17725 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((Id‘𝐷)‘𝑧) ∈ (𝑧(Hom ‘𝐷)𝑧)) |
| 95 | 1, 84, 85, 86, 8, 9, 88, 89, 33, 34, 91, 89, 92, 94 | uncf2 18282 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)) = ((((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑦))‘𝑧))((𝑧(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘((Id‘𝐷)‘𝑧)))) |
| 96 | 22 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) |
| 97 | 96 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((1st ‘𝐺)‘𝑥) ∈ (𝐷 Func 𝐸)) |
| 98 | 15, 97, 23 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (1st
‘((1st ‘𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑥))) |
| 99 | 98 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (1st
‘((1st ‘𝐺)‘𝑥))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑥))) |
| 100 | 9, 93, 48, 99, 89 | funcid 17915 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((𝑧(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘((Id‘𝐷)‘𝑧)) = ((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧))) |
| 101 | 100 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑦))‘𝑧))((𝑧(2nd ‘((1st
‘𝐺)‘𝑥))𝑧)‘((Id‘𝐷)‘𝑧))) = ((((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑦))‘𝑧))((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧)))) |
| 102 | 9, 14, 98 | funcf1 17911 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (1st
‘((1st ‘𝐺)‘𝑥)):(Base‘𝐷)⟶(Base‘𝐸)) |
| 103 | 102 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧) ∈ (Base‘𝐸)) |
| 104 | 21 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑦) ∈ (𝐷 Func 𝐸)) |
| 105 | 104 | adantrl 716 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐺)‘𝑦) ∈ (𝐷 Func 𝐸)) |
| 106 | 105 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((1st ‘𝐺)‘𝑦) ∈ (𝐷 Func 𝐸)) |
| 107 | | 1st2ndbr 8067 |
. . . . . . . . . . . . . . 15
⊢ ((Rel
(𝐷 Func 𝐸) ∧ ((1st ‘𝐺)‘𝑦) ∈ (𝐷 Func 𝐸)) → (1st
‘((1st ‘𝐺)‘𝑦))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑦))) |
| 108 | 15, 106, 107 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (1st
‘((1st ‘𝐺)‘𝑦))(𝐷 Func 𝐸)(2nd ‘((1st
‘𝐺)‘𝑦))) |
| 109 | 9, 14, 108 | funcf1 17911 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (1st
‘((1st ‘𝐺)‘𝑦)):(Base‘𝐷)⟶(Base‘𝐸)) |
| 110 | 109 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((1st
‘((1st ‘𝐺)‘𝑦))‘𝑧) ∈ (Base‘𝐸)) |
| 111 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝐷 Nat 𝐸) = (𝐷 Nat 𝐸) |
| 112 | 16, 111 | fuchom 18009 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 Nat 𝐸) = (Hom ‘(𝐷 FuncCat 𝐸)) |
| 113 | 20 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
| 114 | 8, 33, 112, 113, 88, 91 | funcf2 17913 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑦))) |
| 115 | 114, 92 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) ∈ (((1st ‘𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑦))) |
| 116 | 111, 115 | nat1st2nd 17999 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) ∈ (〈(1st
‘((1st ‘𝐺)‘𝑥)), (2nd ‘((1st
‘𝐺)‘𝑥))〉(𝐷 Nat 𝐸)〈(1st
‘((1st ‘𝐺)‘𝑦)), (2nd ‘((1st
‘𝐺)‘𝑦))〉)) |
| 117 | 111, 116,
9, 58, 89 | natcl 18001 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧) ∈ (((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧)(Hom ‘𝐸)((1st ‘((1st
‘𝐺)‘𝑦))‘𝑧))) |
| 118 | 14, 58, 48, 85, 103, 60, 110, 117 | catrid 17727 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → ((((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧)(〈((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧), ((1st ‘((1st
‘𝐺)‘𝑥))‘𝑧)〉(comp‘𝐸)((1st ‘((1st
‘𝐺)‘𝑦))‘𝑧))((Id‘𝐸)‘((1st
‘((1st ‘𝐺)‘𝑥))‘𝑧))) = (((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧)) |
| 119 | 95, 101, 118 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) ∧ 𝑧 ∈ (Base‘𝐷)) → (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)) = (((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧)) |
| 120 | 119 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))) = (𝑧 ∈ (Base‘𝐷) ↦ (((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧))) |
| 121 | 20 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐶 Func (𝐷 FuncCat 𝐸))(2nd ‘𝐺)) |
| 122 | 8, 33, 112, 121, 87, 90 | funcf2 17913 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑦))) |
| 123 | 122 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) ∈ (((1st ‘𝐺)‘𝑥)(𝐷 Nat 𝐸)((1st ‘𝐺)‘𝑦))) |
| 124 | 111, 123 | nat1st2nd 17999 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) ∈ (〈(1st
‘((1st ‘𝐺)‘𝑥)), (2nd ‘((1st
‘𝐺)‘𝑥))〉(𝐷 Nat 𝐸)〈(1st
‘((1st ‘𝐺)‘𝑦)), (2nd ‘((1st
‘𝐺)‘𝑦))〉)) |
| 125 | 111, 124,
9 | natfn 18002 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) Fn (Base‘𝐷)) |
| 126 | | dffn5 6967 |
. . . . . . . . . 10
⊢ (((𝑥(2nd ‘𝐺)𝑦)‘𝑔) Fn (Base‘𝐷) ↔ ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) = (𝑧 ∈ (Base‘𝐷) ↦ (((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧))) |
| 127 | 125, 126 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑔) = (𝑧 ∈ (Base‘𝐷) ↦ (((𝑥(2nd ‘𝐺)𝑦)‘𝑔)‘𝑧))) |
| 128 | 120, 127 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))) = ((𝑥(2nd ‘𝐺)𝑦)‘𝑔)) |
| 129 | 128 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘𝐺)𝑦)‘𝑔))) |
| 130 | 122 | feqmptd 6977 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦) = (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘𝐺)𝑦)‘𝑔))) |
| 131 | 129, 130 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))) = (𝑥(2nd ‘𝐺)𝑦)) |
| 132 | 131 | 3impb 1115 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))) = (𝑥(2nd ‘𝐺)𝑦)) |
| 133 | 132 | mpoeq3dva 7510 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘𝐺)𝑦))) |
| 134 | 8, 20 | funcfn2 17914 |
. . . . 5
⊢ (𝜑 → (2nd
‘𝐺) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
| 135 | | fnov 7564 |
. . . . 5
⊢
((2nd ‘𝐺) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (2nd ‘𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘𝐺)𝑦))) |
| 136 | 134, 135 | sylib 218 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘𝐺)𝑦))) |
| 137 | 133, 136 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧))))) = (2nd ‘𝐺)) |
| 138 | 83, 137 | opeq12d 4881 |
. 2
⊢ (𝜑 → 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))〉 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉) |
| 139 | | eqid 2737 |
. . 3
⊢
(〈𝐶, 𝐷〉 curryF
𝐹) = (〈𝐶, 𝐷〉 curryF 𝐹) |
| 140 | 1, 2, 4, 6 | uncfcl 18280 |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
| 141 | 139, 8, 40, 2, 140, 9, 34, 37, 33, 93 | curfval 18268 |
. 2
⊢ (𝜑 → (〈𝐶, 𝐷〉 curryF 𝐹) = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈(𝑦 ∈ (Base‘𝐷) ↦ (𝑥(1st ‘𝐹)𝑦)), (𝑦 ∈ (Base‘𝐷), 𝑧 ∈ (Base‘𝐷) ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(〈𝑥, 𝑦〉(2nd ‘𝐹)〈𝑥, 𝑧〉)𝑔)))〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ (Base‘𝐷) ↦ (𝑔(〈𝑥, 𝑧〉(2nd ‘𝐹)〈𝑦, 𝑧〉)((Id‘𝐷)‘𝑧)))))〉) |
| 142 | | 1st2nd 8064 |
. . 3
⊢ ((Rel
(𝐶 Func (𝐷 FuncCat 𝐸)) ∧ 𝐺 ∈ (𝐶 Func (𝐷 FuncCat 𝐸))) → 𝐺 = 〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
| 143 | 18, 6, 142 | sylancr 587 |
. 2
⊢ (𝜑 → 𝐺 = 〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
| 144 | 138, 141,
143 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (〈𝐶, 𝐷〉 curryF 𝐹) = 𝐺) |