Metamath Proof Explorer


Theorem xpcbas

Description: Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Hypotheses xpcbas.t T = C × c D
xpcbas.x X = Base C
xpcbas.y Y = Base D
Assertion xpcbas X × Y = Base T

Proof

Step Hyp Ref Expression
1 xpcbas.t T = C × c D
2 xpcbas.x X = Base C
3 xpcbas.y Y = Base D
4 eqid Hom C = Hom C
5 eqid Hom D = Hom D
6 eqid comp C = comp C
7 eqid comp D = comp D
8 simpl C V D V C V
9 simpr C V D V D V
10 eqidd C V D V X × Y = X × Y
11 eqidd C V D V u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v = u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v
12 eqidd C V D V x X × Y × X × Y , y X × Y g 2 nd x u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v y , f u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v x 1 st g 1 st 1 st x 1 st 2 nd x comp C 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp D 2 nd y 2 nd f = x X × Y × X × Y , y X × Y g 2 nd x u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v y , f u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v x 1 st g 1 st 1 st x 1 st 2 nd x comp C 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp D 2 nd y 2 nd f
13 1 2 3 4 5 6 7 8 9 10 11 12 xpcval C V D V T = Base ndx X × Y Hom ndx u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v comp ndx x X × Y × X × Y , y X × Y g 2 nd x u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v y , f u X × Y , v X × Y 1 st u Hom C 1 st v × 2 nd u Hom D 2 nd v x 1 st g 1 st 1 st x 1 st 2 nd x comp C 1 st y 1 st f 2 nd g 2 nd 1 st x 2 nd 2 nd x comp D 2 nd y 2 nd f
14 2 fvexi X V
15 3 fvexi Y V
16 14 15 xpex X × Y V
17 16 a1i C V D V X × Y V
18 13 17 estrreslem1 C V D V X × Y = Base T
19 base0 = Base
20 fvprc ¬ C V Base C =
21 2 20 syl5eq ¬ C V X =
22 fvprc ¬ D V Base D =
23 3 22 syl5eq ¬ D V Y =
24 21 23 orim12i ¬ C V ¬ D V X = Y =
25 ianor ¬ C V D V ¬ C V ¬ D V
26 xpeq0 X × Y = X = Y =
27 24 25 26 3imtr4i ¬ C V D V X × Y =
28 fnxpc × c Fn V × V
29 fndm × c Fn V × V dom × c = V × V
30 28 29 ax-mp dom × c = V × V
31 30 ndmov ¬ C V D V C × c D =
32 1 31 syl5eq ¬ C V D V T =
33 32 fveq2d ¬ C V D V Base T = Base
34 19 27 33 3eqtr4a ¬ C V D V X × Y = Base T
35 18 34 pm2.61i X × Y = Base T