| Step | Hyp | Ref
| Expression |
| 1 | | fucval.q |
. 2
⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
| 2 | | df-fuc 17992 |
. . . 4
⊢ FuncCat
= (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦
{〈(Base‘ndx), (𝑡
Func 𝑢)〉, 〈(Hom
‘ndx), (𝑡 Nat 𝑢)〉, 〈(comp‘ndx),
(𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉}) |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → FuncCat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {〈(Base‘ndx),
(𝑡 Func 𝑢)〉, 〈(Hom ‘ndx), (𝑡 Nat 𝑢)〉, 〈(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉})) |
| 4 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → 𝑡 = 𝐶) |
| 5 | | simprr 773 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → 𝑢 = 𝐷) |
| 6 | 4, 5 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑡 Func 𝑢) = (𝐶 Func 𝐷)) |
| 7 | | fucval.b |
. . . . . 6
⊢ 𝐵 = (𝐶 Func 𝐷) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑡 Func 𝑢) = 𝐵) |
| 9 | 8 | opeq2d 4880 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → 〈(Base‘ndx), (𝑡 Func 𝑢)〉 = 〈(Base‘ndx), 𝐵〉) |
| 10 | 4, 5 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑡 Nat 𝑢) = (𝐶 Nat 𝐷)) |
| 11 | | fucval.n |
. . . . . 6
⊢ 𝑁 = (𝐶 Nat 𝐷) |
| 12 | 10, 11 | eqtr4di 2795 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑡 Nat 𝑢) = 𝑁) |
| 13 | 12 | opeq2d 4880 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → 〈(Hom ‘ndx), (𝑡 Nat 𝑢)〉 = 〈(Hom ‘ndx), 𝑁〉) |
| 14 | 8 | sqxpeqd 5717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)) = (𝐵 × 𝐵)) |
| 15 | 12 | oveqd 7448 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑔(𝑡 Nat 𝑢)ℎ) = (𝑔𝑁ℎ)) |
| 16 | 12 | oveqd 7448 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑓(𝑡 Nat 𝑢)𝑔) = (𝑓𝑁𝑔)) |
| 17 | 4 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (Base‘𝑡) = (Base‘𝐶)) |
| 18 | | fucval.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (Base‘𝐶) |
| 19 | 17, 18 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (Base‘𝑡) = 𝐴) |
| 20 | 5 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (comp‘𝑢) = (comp‘𝐷)) |
| 21 | | fucval.o |
. . . . . . . . . . . . . 14
⊢ · =
(comp‘𝐷) |
| 22 | 20, 21 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (comp‘𝑢) = · ) |
| 23 | 22 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (〈((1st
‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥)) = (〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))) |
| 24 | 23 | oveqd 7448 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) = ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))) |
| 25 | 19, 24 | mpteq12dv 5233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))) = (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))) |
| 26 | 15, 16, 25 | mpoeq123dv 7508 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) |
| 27 | 26 | csbeq2dv 3906 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → ⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) = ⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) |
| 28 | 27 | csbeq2dv 3906 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) = ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) |
| 29 | 14, 8, 28 | mpoeq123dv 7508 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |
| 30 | | fucval.x |
. . . . . . 7
⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |
| 31 | 30 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |
| 32 | 29, 31 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) = ∙ ) |
| 33 | 32 | opeq2d 4880 |
. . . 4
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → 〈(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉 = 〈(comp‘ndx), ∙
〉) |
| 34 | 9, 13, 33 | tpeq123d 4748 |
. . 3
⊢ ((𝜑 ∧ (𝑡 = 𝐶 ∧ 𝑢 = 𝐷)) → {〈(Base‘ndx), (𝑡 Func 𝑢)〉, 〈(Hom ‘ndx), (𝑡 Nat 𝑢)〉, 〈(comp‘ndx), (𝑣 ∈ ((𝑡 Func 𝑢) × (𝑡 Func 𝑢)), ℎ ∈ (𝑡 Func 𝑢) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑡 Nat 𝑢)ℎ), 𝑎 ∈ (𝑓(𝑡 Nat 𝑢)𝑔) ↦ (𝑥 ∈ (Base‘𝑡) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑢)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉} = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝑁〉,
〈(comp‘ndx), ∙
〉}) |
| 35 | | fucval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 36 | | fucval.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 37 | | tpex 7766 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝑁〉, 〈(comp‘ndx),
∙
〉} ∈ V |
| 38 | 37 | a1i 11 |
. . 3
⊢ (𝜑 → {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝑁〉,
〈(comp‘ndx), ∙ 〉} ∈
V) |
| 39 | 3, 34, 35, 36, 38 | ovmpod 7585 |
. 2
⊢ (𝜑 → (𝐶 FuncCat 𝐷) = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝑁〉,
〈(comp‘ndx), ∙
〉}) |
| 40 | 1, 39 | eqtrid 2789 |
1
⊢ (𝜑 → 𝑄 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝑁〉,
〈(comp‘ndx), ∙
〉}) |