# 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}={\mathrm{Base}}_{{C}}$
xpcbas.y ${⊢}{Y}={\mathrm{Base}}_{{D}}$
Assertion xpcbas ${⊢}{X}×{Y}={\mathrm{Base}}_{{T}}$

### Proof

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