Theorem qsalrel

Description: The quotient set is equal to the singleton of A when all elements are related and A is nonempty. (Contributed by SN, 8-Jun-2023)

	Ref	Expression
Hypotheses	qsalrel.1	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to x\underset{\dot{}}{\sim }y$$
	qsalrel.2	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}A$$
	qsalrel.3	$$⊢\phi \to N\in A$$
Assertion	qsalrel	$$⊢\phi \to A/\underset{\dot{}}{\sim }=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		qsalrel.1	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to x\underset{\dot{}}{\sim }y$$
2		qsalrel.2	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}A$$
3		qsalrel.3	$$⊢\phi \to N\in A$$
4		dfqs2	$$⊢A/\underset{\dot{}}{\sim }=\mathrm{ran}\left(a\in A⟼\left[a\right]\underset{\dot{}}{\sim }\right)$$
5	2	adantr	$$⊢\left(\phi \wedge a\in A\right)\to \underset{\dot{}}{\sim }\mathrm{Er}A$$
6	1	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in Ax\underset{\dot{}}{\sim }y$$
7	6	adantr	$$⊢\left(\phi \wedge a\in A\right)\to \forall x\in A\forall y\in Ax\underset{\dot{}}{\sim }y$$
8		simpr	$$⊢\left(\phi \wedge a\in A\right)\to a\in A$$
9		breq1	$$⊢x=a\to \left(x\underset{\dot{}}{\sim }y\leftrightarrow a\underset{\dot{}}{\sim }y\right)$$
10	9	ralbidv	$$⊢x=a\to \left(\forall y\in Ax\underset{\dot{}}{\sim }y\leftrightarrow \forall y\in Aa\underset{\dot{}}{\sim }y\right)$$
11	10	adantl	$$⊢\left(\left(\phi \wedge a\in A\right)\wedge x=a\right)\to \left(\forall y\in Ax\underset{\dot{}}{\sim }y\leftrightarrow \forall y\in Aa\underset{\dot{}}{\sim }y\right)$$
12	8 11	rspcdv	$$⊢\left(\phi \wedge a\in A\right)\to \left(\forall x\in A\forall y\in Ax\underset{\dot{}}{\sim }y\to \forall y\in Aa\underset{\dot{}}{\sim }y\right)$$
13		breq2	$$⊢y=N\to \left(a\underset{\dot{}}{\sim }y\leftrightarrow a\underset{\dot{}}{\sim }N\right)$$
14	13	adantl	$$⊢\left(\phi \wedge y=N\right)\to \left(a\underset{\dot{}}{\sim }y\leftrightarrow a\underset{\dot{}}{\sim }N\right)$$
15	3 14	rspcdv	$$⊢\phi \to \left(\forall y\in Aa\underset{\dot{}}{\sim }y\to a\underset{\dot{}}{\sim }N\right)$$
16	15	adantr	$$⊢\left(\phi \wedge a\in A\right)\to \left(\forall y\in Aa\underset{\dot{}}{\sim }y\to a\underset{\dot{}}{\sim }N\right)$$
17	12 16	syld	$$⊢\left(\phi \wedge a\in A\right)\to \left(\forall x\in A\forall y\in Ax\underset{\dot{}}{\sim }y\to a\underset{\dot{}}{\sim }N\right)$$
18	7 17	mpd	$$⊢\left(\phi \wedge a\in A\right)\to a\underset{\dot{}}{\sim }N$$
19	5 18	erthi	$$⊢\left(\phi \wedge a\in A\right)\to \left[a\right]\underset{\dot{}}{\sim }=\left[N\right]\underset{\dot{}}{\sim }$$
20	19	mpteq2dva	$$⊢\phi \to \left(a\in A⟼\left[a\right]\underset{\dot{}}{\sim }\right)=\left(a\in A⟼\left[N\right]\underset{\dot{}}{\sim }\right)$$
21	20	rneqd	$$⊢\phi \to \mathrm{ran}\left(a\in A⟼\left[a\right]\underset{\dot{}}{\sim }\right)=\mathrm{ran}\left(a\in A⟼\left[N\right]\underset{\dot{}}{\sim }\right)$$
22		eqid	$$⊢\left(a\in A⟼\left[N\right]\underset{\dot{}}{\sim }\right)=\left(a\in A⟼\left[N\right]\underset{\dot{}}{\sim }\right)$$
23	3	ne0d	$$⊢\phi \to A\ne \varnothing$$
24	22 23	rnmptc	$$⊢\phi \to \mathrm{ran}\left(a\in A⟼\left[N\right]\underset{\dot{}}{\sim }\right)=\left\{\left[N\right]\underset{\dot{}}{\sim }\right\}$$
25	2	ecss	$$⊢\phi \to \left[N\right]\underset{\dot{}}{\sim }\subseteq A$$
26	5 18	ersym	$$⊢\left(\phi \wedge a\in A\right)\to N\underset{\dot{}}{\sim }a$$
27	3	adantr	$$⊢\left(\phi \wedge a\in A\right)\to N\in A$$
28		elecg	$$⊢\left(a\in A\wedge N\in A\right)\to \left(a\in \left[N\right]\underset{\dot{}}{\sim }\leftrightarrow N\underset{\dot{}}{\sim }a\right)$$
29	8 27 28	syl2anc	$$⊢\left(\phi \wedge a\in A\right)\to \left(a\in \left[N\right]\underset{\dot{}}{\sim }\leftrightarrow N\underset{\dot{}}{\sim }a\right)$$
30	26 29	mpbird	$$⊢\left(\phi \wedge a\in A\right)\to a\in \left[N\right]\underset{\dot{}}{\sim }$$
31	25 30	eqelssd	$$⊢\phi \to \left[N\right]\underset{\dot{}}{\sim }=A$$
32	31	sneqd	$$⊢\phi \to \left\{\left[N\right]\underset{\dot{}}{\sim }\right\}=\left\{A\right\}$$
33	21 24 32	3eqtrd	$$⊢\phi \to \mathrm{ran}\left(a\in A⟼\left[a\right]\underset{\dot{}}{\sim }\right)=\left\{A\right\}$$
34	4 33	syl5eq	$$⊢\phi \to A/\underset{\dot{}}{\sim }=\left\{A\right\}$$