Theorem qusbas

Description: Base set of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	qusbas.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qusbas.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qusbas.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
	qusbas.r	$$⊢\phi \to R\in Z$$
Assertion	qusbas	$$⊢\phi \to V/\underset{\dot{}}{\sim }={\mathrm{Base}}_U$$

Proof

Step	Hyp	Ref	Expression
1		qusbas.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
2		qusbas.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qusbas.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
4		qusbas.r	$$⊢\phi \to R\in Z$$
5		eqid	$$⊢\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
6	1 2 5 3 4	qusval	$$⊢\phi \to U=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right){“}_{𝑠}R$$
7	1 2 5 3 4	quslem	$$⊢\phi \to \left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right):V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$
8	6 2 7 4	imasbas	$$⊢\phi \to V/\underset{\dot{}}{\sim }={\mathrm{Base}}_U$$