Theorem qsxpid

Description: The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024)

	Ref	Expression
Assertion	qsxpid	$$⊢A\ne \varnothing \to A/\left(A\times A\right)=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(x\in A\wedge y=\left[x\right]\left(A\times A\right)\right)\to y=\left[x\right]\left(A\times A\right)$$
2		ecxpid	$$⊢x\in A\to \left[x\right]\left(A\times A\right)=A$$
3	2	adantr	$$⊢\left(x\in A\wedge y=\left[x\right]\left(A\times A\right)\right)\to \left[x\right]\left(A\times A\right)=A$$
4	1 3	eqtrd	$$⊢\left(x\in A\wedge y=\left[x\right]\left(A\times A\right)\right)\to y=A$$
5	4	rexlimiva	$$⊢\exists x\in Ay=\left[x\right]\left(A\times A\right)\to y=A$$
6	5	adantl	$$⊢\left(A\ne \varnothing \wedge \exists x\in Ay=\left[x\right]\left(A\times A\right)\right)\to y=A$$
7		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
8	7	biimpi	$$⊢A\ne \varnothing \to \exists xx\in A$$
9		simpl	$$⊢\left(y=A\wedge x\in A\right)\to y=A$$
10	2	adantl	$$⊢\left(y=A\wedge x\in A\right)\to \left[x\right]\left(A\times A\right)=A$$
11	9 10	eqtr4d	$$⊢\left(y=A\wedge x\in A\right)\to y=\left[x\right]\left(A\times A\right)$$
12	11	ex	$$⊢y=A\to \left(x\in A\to y=\left[x\right]\left(A\times A\right)\right)$$
13	12	ancld	$$⊢y=A\to \left(x\in A\to \left(x\in A\wedge y=\left[x\right]\left(A\times A\right)\right)\right)$$
14	13	eximdv	$$⊢y=A\to \left(\exists xx\in A\to \exists x\left(x\in A\wedge y=\left[x\right]\left(A\times A\right)\right)\right)$$
15	8 14	mpan9	$$⊢\left(A\ne \varnothing \wedge y=A\right)\to \exists x\left(x\in A\wedge y=\left[x\right]\left(A\times A\right)\right)$$
16		df-rex	$$⊢\exists x\in Ay=\left[x\right]\left(A\times A\right)\leftrightarrow \exists x\left(x\in A\wedge y=\left[x\right]\left(A\times A\right)\right)$$
17	15 16	sylibr	$$⊢\left(A\ne \varnothing \wedge y=A\right)\to \exists x\in Ay=\left[x\right]\left(A\times A\right)$$
18	6 17	impbida	$$⊢A\ne \varnothing \to \left(\exists x\in Ay=\left[x\right]\left(A\times A\right)\leftrightarrow y=A\right)$$
19		vex	$$⊢y\in \mathrm{V}$$
20	19	elqs	$$⊢y\in \left(A/\left(A\times A\right)\right)\leftrightarrow \exists x\in Ay=\left[x\right]\left(A\times A\right)$$
21		velsn	$$⊢y\in \left\{A\right\}\leftrightarrow y=A$$
22	18 20 21	3bitr4g	$$⊢A\ne \varnothing \to \left(y\in \left(A/\left(A\times A\right)\right)\leftrightarrow y\in \left\{A\right\}\right)$$
23	22	eqrdv	$$⊢A\ne \varnothing \to A/\left(A\times A\right)=\left\{A\right\}$$