MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xpc Structured version   Visualization version   GIF version

Definition df-xpc 18123
Description: Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.)
Assertion
Ref Expression
df-xpc Γ—c = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ ⦋((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) / π‘β¦Œβ¦‹(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩})
Distinct variable group:   𝑓,𝑏,𝑔,β„Ž,π‘Ÿ,𝑠,𝑒,𝑣,π‘₯,𝑦

Detailed syntax breakdown of Definition df-xpc
StepHypRef Expression
1 cxpc 18119 . 2 class Γ—c
2 vr . . 3 setvar π‘Ÿ
3 vs . . 3 setvar 𝑠
4 cvv 3474 . . 3 class V
5 vb . . . 4 setvar 𝑏
62cv 1540 . . . . . 6 class π‘Ÿ
7 cbs 17143 . . . . . 6 class Base
86, 7cfv 6543 . . . . 5 class (Baseβ€˜π‘Ÿ)
93cv 1540 . . . . . 6 class 𝑠
109, 7cfv 6543 . . . . 5 class (Baseβ€˜π‘ )
118, 10cxp 5674 . . . 4 class ((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ ))
12 vh . . . . 5 setvar β„Ž
13 vu . . . . . 6 setvar 𝑒
14 vv . . . . . 6 setvar 𝑣
155cv 1540 . . . . . 6 class 𝑏
1613cv 1540 . . . . . . . . 9 class 𝑒
17 c1st 7972 . . . . . . . . 9 class 1st
1816, 17cfv 6543 . . . . . . . 8 class (1st β€˜π‘’)
1914cv 1540 . . . . . . . . 9 class 𝑣
2019, 17cfv 6543 . . . . . . . 8 class (1st β€˜π‘£)
21 chom 17207 . . . . . . . . 9 class Hom
226, 21cfv 6543 . . . . . . . 8 class (Hom β€˜π‘Ÿ)
2318, 20, 22co 7408 . . . . . . 7 class ((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£))
24 c2nd 7973 . . . . . . . . 9 class 2nd
2516, 24cfv 6543 . . . . . . . 8 class (2nd β€˜π‘’)
2619, 24cfv 6543 . . . . . . . 8 class (2nd β€˜π‘£)
279, 21cfv 6543 . . . . . . . 8 class (Hom β€˜π‘ )
2825, 26, 27co 7408 . . . . . . 7 class ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£))
2923, 28cxp 5674 . . . . . 6 class (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))
3013, 14, 15, 15, 29cmpo 7410 . . . . 5 class (𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£))))
31 cnx 17125 . . . . . . . 8 class ndx
3231, 7cfv 6543 . . . . . . 7 class (Baseβ€˜ndx)
3332, 15cop 4634 . . . . . 6 class ⟨(Baseβ€˜ndx), π‘βŸ©
3431, 21cfv 6543 . . . . . . 7 class (Hom β€˜ndx)
3512cv 1540 . . . . . . 7 class β„Ž
3634, 35cop 4634 . . . . . 6 class ⟨(Hom β€˜ndx), β„ŽβŸ©
37 cco 17208 . . . . . . . 8 class comp
3831, 37cfv 6543 . . . . . . 7 class (compβ€˜ndx)
39 vx . . . . . . . 8 setvar π‘₯
40 vy . . . . . . . 8 setvar 𝑦
4115, 15cxp 5674 . . . . . . . 8 class (𝑏 Γ— 𝑏)
42 vg . . . . . . . . 9 setvar 𝑔
43 vf . . . . . . . . 9 setvar 𝑓
4439cv 1540 . . . . . . . . . . 11 class π‘₯
4544, 24cfv 6543 . . . . . . . . . 10 class (2nd β€˜π‘₯)
4640cv 1540 . . . . . . . . . 10 class 𝑦
4745, 46, 35co 7408 . . . . . . . . 9 class ((2nd β€˜π‘₯)β„Žπ‘¦)
4844, 35cfv 6543 . . . . . . . . 9 class (β„Žβ€˜π‘₯)
4942cv 1540 . . . . . . . . . . . 12 class 𝑔
5049, 17cfv 6543 . . . . . . . . . . 11 class (1st β€˜π‘”)
5143cv 1540 . . . . . . . . . . . 12 class 𝑓
5251, 17cfv 6543 . . . . . . . . . . 11 class (1st β€˜π‘“)
5344, 17cfv 6543 . . . . . . . . . . . . . 14 class (1st β€˜π‘₯)
5453, 17cfv 6543 . . . . . . . . . . . . 13 class (1st β€˜(1st β€˜π‘₯))
5545, 17cfv 6543 . . . . . . . . . . . . 13 class (1st β€˜(2nd β€˜π‘₯))
5654, 55cop 4634 . . . . . . . . . . . 12 class ⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩
5746, 17cfv 6543 . . . . . . . . . . . 12 class (1st β€˜π‘¦)
586, 37cfv 6543 . . . . . . . . . . . 12 class (compβ€˜π‘Ÿ)
5956, 57, 58co 7408 . . . . . . . . . . 11 class (⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))
6050, 52, 59co 7408 . . . . . . . . . 10 class ((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“))
6149, 24cfv 6543 . . . . . . . . . . 11 class (2nd β€˜π‘”)
6251, 24cfv 6543 . . . . . . . . . . 11 class (2nd β€˜π‘“)
6353, 24cfv 6543 . . . . . . . . . . . . 13 class (2nd β€˜(1st β€˜π‘₯))
6445, 24cfv 6543 . . . . . . . . . . . . 13 class (2nd β€˜(2nd β€˜π‘₯))
6563, 64cop 4634 . . . . . . . . . . . 12 class ⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩
6646, 24cfv 6543 . . . . . . . . . . . 12 class (2nd β€˜π‘¦)
679, 37cfv 6543 . . . . . . . . . . . 12 class (compβ€˜π‘ )
6865, 66, 67co 7408 . . . . . . . . . . 11 class (⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))
6961, 62, 68co 7408 . . . . . . . . . 10 class ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))
7060, 69cop 4634 . . . . . . . . 9 class ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩
7142, 43, 47, 48, 70cmpo 7410 . . . . . . . 8 class (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)
7239, 40, 41, 15, 71cmpo 7410 . . . . . . 7 class (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))
7338, 72cop 4634 . . . . . 6 class ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩
7433, 36, 73ctp 4632 . . . . 5 class {⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩}
7512, 30, 74csb 3893 . . . 4 class ⦋(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩}
765, 11, 75csb 3893 . . 3 class ⦋((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) / π‘β¦Œβ¦‹(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩}
772, 3, 4, 4, 76cmpo 7410 . 2 class (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ ⦋((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) / π‘β¦Œβ¦‹(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩})
781, 77wceq 1541 1 wff Γ—c = (π‘Ÿ ∈ V, 𝑠 ∈ V ↦ ⦋((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ )) / π‘β¦Œβ¦‹(𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))) / β„Žβ¦Œ{⟨(Baseβ€˜ndx), π‘βŸ©, ⟨(Hom β€˜ndx), β„ŽβŸ©, ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  fnxpc  18127  xpcval  18128
  Copyright terms: Public domain W3C validator