Theorem xpsbas

Description: The base set of the binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

	Ref	Expression
Hypotheses	xpsval.t	$$⊢T=R{\times }_{𝑠}S$$
	xpsval.x	$$⊢X={\mathrm{Base}}_R$$
	xpsval.y	$$⊢Y={\mathrm{Base}}_S$$
	xpsval.1	$$⊢\phi \to R\in V$$
	xpsval.2	$$⊢\phi \to S\in W$$
Assertion	xpsbas	$$⊢\phi \to X\times Y={\mathrm{Base}}_T$$

Proof

Step	Hyp	Ref	Expression
1		xpsval.t	$$⊢T=R{\times }_{𝑠}S$$
2		xpsval.x	$$⊢X={\mathrm{Base}}_R$$
3		xpsval.y	$$⊢Y={\mathrm{Base}}_S$$
4		xpsval.1	$$⊢\phi \to R\in V$$
5		xpsval.2	$$⊢\phi \to S\in W$$
6		eqid	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)=\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
7		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
8		eqid	$$⊢\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}=\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}$$
9	1 2 3 4 5 6 7 8	xpsval	$$⊢\phi \to T={\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}{“}_{𝑠}\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)$$
10	1 2 3 4 5 6 7 8	xpsrnbas	$$⊢\phi \to \mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)={\mathrm{Base}}_{\left(\mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\right)}$$
11	6	xpsff1o2	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)$$
12		f1ocnv	$$⊢\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right):X\times Y\underset{1-1\; onto}{⟶}\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y$$
13	11 12	ax-mp	$$⊢{\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y$$
14		f1ofo	$$⊢{\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{1-1\; onto}{⟶}X\times Y\to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}X\times Y$$
15	13 14	mp1i	$$⊢\phi \to {\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)}^{-1}:\mathrm{ran}\left(x\in X,y\in Y⟼\left\{⟨\varnothing ,x⟩,⟨1_{𝑜},y⟩\right\}\right)\underset{onto}{⟶}X\times Y$$
16		ovexd	$$⊢\phi \to \mathrm{Scalar}\left(R\right){⨉}_{𝑠}\left\{⟨\varnothing ,R⟩,⟨1_{𝑜},S⟩\right\}\in \mathrm{V}$$
17	9 10 15 16	imasbas	$$⊢\phi \to X\times Y={\mathrm{Base}}_T$$