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 18065
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 18061 . 2 class Γ—c
2 vr . . 3 setvar π‘Ÿ
3 vs . . 3 setvar 𝑠
4 cvv 3444 . . 3 class V
5 vb . . . 4 setvar 𝑏
62cv 1541 . . . . . 6 class π‘Ÿ
7 cbs 17088 . . . . . 6 class Base
86, 7cfv 6497 . . . . 5 class (Baseβ€˜π‘Ÿ)
93cv 1541 . . . . . 6 class 𝑠
109, 7cfv 6497 . . . . 5 class (Baseβ€˜π‘ )
118, 10cxp 5632 . . . 4 class ((Baseβ€˜π‘Ÿ) Γ— (Baseβ€˜π‘ ))
12 vh . . . . 5 setvar β„Ž
13 vu . . . . . 6 setvar 𝑒
14 vv . . . . . 6 setvar 𝑣
155cv 1541 . . . . . 6 class 𝑏
1613cv 1541 . . . . . . . . 9 class 𝑒
17 c1st 7920 . . . . . . . . 9 class 1st
1816, 17cfv 6497 . . . . . . . 8 class (1st β€˜π‘’)
1914cv 1541 . . . . . . . . 9 class 𝑣
2019, 17cfv 6497 . . . . . . . 8 class (1st β€˜π‘£)
21 chom 17149 . . . . . . . . 9 class Hom
226, 21cfv 6497 . . . . . . . 8 class (Hom β€˜π‘Ÿ)
2318, 20, 22co 7358 . . . . . . 7 class ((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£))
24 c2nd 7921 . . . . . . . . 9 class 2nd
2516, 24cfv 6497 . . . . . . . 8 class (2nd β€˜π‘’)
2619, 24cfv 6497 . . . . . . . 8 class (2nd β€˜π‘£)
279, 21cfv 6497 . . . . . . . 8 class (Hom β€˜π‘ )
2825, 26, 27co 7358 . . . . . . 7 class ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£))
2923, 28cxp 5632 . . . . . 6 class (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£)))
3013, 14, 15, 15, 29cmpo 7360 . . . . 5 class (𝑒 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st β€˜π‘’)(Hom β€˜π‘Ÿ)(1st β€˜π‘£)) Γ— ((2nd β€˜π‘’)(Hom β€˜π‘ )(2nd β€˜π‘£))))
31 cnx 17070 . . . . . . . 8 class ndx
3231, 7cfv 6497 . . . . . . 7 class (Baseβ€˜ndx)
3332, 15cop 4593 . . . . . 6 class ⟨(Baseβ€˜ndx), π‘βŸ©
3431, 21cfv 6497 . . . . . . 7 class (Hom β€˜ndx)
3512cv 1541 . . . . . . 7 class β„Ž
3634, 35cop 4593 . . . . . 6 class ⟨(Hom β€˜ndx), β„ŽβŸ©
37 cco 17150 . . . . . . . 8 class comp
3831, 37cfv 6497 . . . . . . 7 class (compβ€˜ndx)
39 vx . . . . . . . 8 setvar π‘₯
40 vy . . . . . . . 8 setvar 𝑦
4115, 15cxp 5632 . . . . . . . 8 class (𝑏 Γ— 𝑏)
42 vg . . . . . . . . 9 setvar 𝑔
43 vf . . . . . . . . 9 setvar 𝑓
4439cv 1541 . . . . . . . . . . 11 class π‘₯
4544, 24cfv 6497 . . . . . . . . . 10 class (2nd β€˜π‘₯)
4640cv 1541 . . . . . . . . . 10 class 𝑦
4745, 46, 35co 7358 . . . . . . . . 9 class ((2nd β€˜π‘₯)β„Žπ‘¦)
4844, 35cfv 6497 . . . . . . . . 9 class (β„Žβ€˜π‘₯)
4942cv 1541 . . . . . . . . . . . 12 class 𝑔
5049, 17cfv 6497 . . . . . . . . . . 11 class (1st β€˜π‘”)
5143cv 1541 . . . . . . . . . . . 12 class 𝑓
5251, 17cfv 6497 . . . . . . . . . . 11 class (1st β€˜π‘“)
5344, 17cfv 6497 . . . . . . . . . . . . . 14 class (1st β€˜π‘₯)
5453, 17cfv 6497 . . . . . . . . . . . . 13 class (1st β€˜(1st β€˜π‘₯))
5545, 17cfv 6497 . . . . . . . . . . . . 13 class (1st β€˜(2nd β€˜π‘₯))
5654, 55cop 4593 . . . . . . . . . . . 12 class ⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩
5746, 17cfv 6497 . . . . . . . . . . . 12 class (1st β€˜π‘¦)
586, 37cfv 6497 . . . . . . . . . . . 12 class (compβ€˜π‘Ÿ)
5956, 57, 58co 7358 . . . . . . . . . . 11 class (⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))
6050, 52, 59co 7358 . . . . . . . . . 10 class ((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“))
6149, 24cfv 6497 . . . . . . . . . . 11 class (2nd β€˜π‘”)
6251, 24cfv 6497 . . . . . . . . . . 11 class (2nd β€˜π‘“)
6353, 24cfv 6497 . . . . . . . . . . . . 13 class (2nd β€˜(1st β€˜π‘₯))
6445, 24cfv 6497 . . . . . . . . . . . . 13 class (2nd β€˜(2nd β€˜π‘₯))
6563, 64cop 4593 . . . . . . . . . . . 12 class ⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩
6646, 24cfv 6497 . . . . . . . . . . . 12 class (2nd β€˜π‘¦)
679, 37cfv 6497 . . . . . . . . . . . 12 class (compβ€˜π‘ )
6865, 66, 67co 7358 . . . . . . . . . . 11 class (⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))
6961, 62, 68co 7358 . . . . . . . . . 10 class ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))
7060, 69cop 4593 . . . . . . . . 9 class ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩
7142, 43, 47, 48, 70cmpo 7360 . . . . . . . 8 class (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩)
7239, 40, 41, 15, 71cmpo 7360 . . . . . . 7 class (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))
7338, 72cop 4593 . . . . . 6 class ⟨(compβ€˜ndx), (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd β€˜π‘₯)β„Žπ‘¦), 𝑓 ∈ (β„Žβ€˜π‘₯) ↦ ⟨((1st β€˜π‘”)(⟨(1st β€˜(1st β€˜π‘₯)), (1st β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘Ÿ)(1st β€˜π‘¦))(1st β€˜π‘“)), ((2nd β€˜π‘”)(⟨(2nd β€˜(1st β€˜π‘₯)), (2nd β€˜(2nd β€˜π‘₯))⟩(compβ€˜π‘ )(2nd β€˜π‘¦))(2nd β€˜π‘“))⟩))⟩
7433, 36, 73ctp 4591 . . . . 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 3856 . . . 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 3856 . . 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 7360 . 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 1542 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  18069  xpcval  18070
  Copyright terms: Public domain W3C validator