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×cD
xpcbas.x ⊢X=BaseC
xpcbas.y ⊢Y=BaseD
Assertion xpcbas ⊢X×Y=BaseT

Proof

Step Hyp Ref Expression
1 xpcbas.t ⊢T=C×cD
2 xpcbas.x ⊢X=BaseC
3 xpcbas.y ⊢Y=BaseD
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⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡v=u∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡v
12 eqidd ⊢C∈V∧D∈V→x∈X×Y×X×Y,y∈X×Y⟼g∈2nd⁡xu∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡vy,f∈u∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡v⁡x⟼1st⁡g1st⁡1st⁡x1st⁡2nd⁡xcomp⁡C1st⁡y1st⁡f2nd⁡g2nd⁡1st⁡x2nd⁡2nd⁡xcomp⁡D2nd⁡y2nd⁡f=x∈X×Y×X×Y,y∈X×Y⟼g∈2nd⁡xu∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡vy,f∈u∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡v⁡x⟼1st⁡g1st⁡1st⁡x1st⁡2nd⁡xcomp⁡C1st⁡y1st⁡f2nd⁡g2nd⁡1st⁡x2nd⁡2nd⁡xcomp⁡D2nd⁡y2nd⁡f
13 1 2 3 4 5 6 7 8 9 10 11 12 xpcval ⊢C∈V∧D∈V→T=BasendxX×YHom⁡ndxu∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡vcomp⁡ndxx∈X×Y×X×Y,y∈X×Y⟼g∈2nd⁡xu∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡vy,f∈u∈X×Y,v∈X×Y⟼1st⁡uHom⁡C1st⁡v×2nd⁡uHom⁡D2nd⁡v⁡x⟼1st⁡g1st⁡1st⁡x1st⁡2nd⁡xcomp⁡C1st⁡y1st⁡f2nd⁡g2nd⁡1st⁡x2nd⁡2nd⁡xcomp⁡D2nd⁡y2nd⁡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=BaseT
19 base0 ⊢∅=Base∅
20 fvprc ⊢¬C∈V→BaseC=∅
21 2 20 eqtrid ⊢¬C∈V→X=∅
22 fvprc ⊢¬D∈V→BaseD=∅
23 3 22 eqtrid ⊢¬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 ⊢×cFnV×V
29 fndm ⊢×cFnV×V→dom⁡×c=V×V
30 28 29 ax-mp ⊢dom⁡×c=V×V
31 30 ndmov ⊢¬C∈V∧D∈V→C×cD=∅
32 1 31 eqtrid ⊢¬C∈V∧D∈V→T=∅
33 32 fveq2d ⊢¬C∈V∧D∈V→BaseT=Base∅
34 19 27 33 3eqtr4a ⊢¬C∈V∧D∈V→X×Y=BaseT
35 18 34 pm2.61i ⊢X×Y=BaseT