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