Proof of Theorem fuccofval
Step | Hyp | Ref
| Expression |
1 | | fucval.q |
. . . 4
⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
2 | | fucval.b |
. . . 4
⊢ 𝐵 = (𝐶 Func 𝐷) |
3 | | fucval.n |
. . . 4
⊢ 𝑁 = (𝐶 Nat 𝐷) |
4 | | fucval.a |
. . . 4
⊢ 𝐴 = (Base‘𝐶) |
5 | | fucval.o |
. . . 4
⊢ · =
(comp‘𝐷) |
6 | | fucval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
7 | | fucval.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
8 | | eqidd 2611 |
. . . 4
⊢ (𝜑 → (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | fucval 16441 |
. . 3
⊢ (𝜑 → 𝑄 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝑁〉,
〈(comp‘ndx), (𝑣
∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉}) |
10 | 9 | fveq2d 6107 |
. 2
⊢ (𝜑 → (comp‘𝑄) =
(comp‘{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝑁〉, 〈(comp‘ndx),
(𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉})) |
11 | | fuccofval.x |
. 2
⊢ ∙ =
(comp‘𝑄) |
12 | | ovex 6577 |
. . . . . 6
⊢ (𝐶 Func 𝐷) ∈ V |
13 | 2, 12 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
14 | 13, 13 | xpex 6860 |
. . . 4
⊢ (𝐵 × 𝐵) ∈ V |
15 | 14, 13 | mpt2ex 7136 |
. . 3
⊢ (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ V |
16 | | catstr 16440 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx), 𝑁〉, 〈(comp‘ndx),
(𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉} Struct 〈1, ;15〉 |
17 | | ccoid 15900 |
. . . 4
⊢ comp =
Slot (comp‘ndx) |
18 | | snsstp3 4289 |
. . . 4
⊢
{〈(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉} ⊆ {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝑁〉,
〈(comp‘ndx), (𝑣
∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉} |
19 | 16, 17, 18 | strfv 15735 |
. . 3
⊢ ((𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ V → (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (comp‘{〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝑁〉,
〈(comp‘ndx), (𝑣
∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉})) |
20 | 15, 19 | ax-mp 5 |
. 2
⊢ (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (comp‘{〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝑁〉,
〈(comp‘ndx), (𝑣
∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉}) |
21 | 10, 11, 20 | 3eqtr4g 2669 |
1
⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉 · ((1st
‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |