Theorem qsxpid

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

	Ref	Expression
Assertion	qsxpid	|- ( A =/= (/) -> ( A /. ( A X. A ) ) = { A } )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( x e. A /\ y = [ x ] ( A X. A ) ) -> y = [ x ] ( A X. A ) )
2		ecxpid	|- ( x e. A -> [ x ] ( A X. A ) = A )
3	2	adantr	|- ( ( x e. A /\ y = [ x ] ( A X. A ) ) -> [ x ] ( A X. A ) = A )
4	1 3	eqtrd	|- ( ( x e. A /\ y = [ x ] ( A X. A ) ) -> y = A )
5	4	rexlimiva	|- ( E. x e. A y = [ x ] ( A X. A ) -> y = A )
6	5	adantl	|- ( ( A =/= (/) /\ E. x e. A y = [ x ] ( A X. A ) ) -> y = A )
7		n0	|- ( A =/= (/) <-> E. x x e. A )
8	7	biimpi	|- ( A =/= (/) -> E. x x e. A )
9		simpl	|- ( ( y = A /\ x e. A ) -> y = A )
10	2	adantl	|- ( ( y = A /\ x e. A ) -> [ x ] ( A X. A ) = A )
11	9 10	eqtr4d	|- ( ( y = A /\ x e. A ) -> y = [ x ] ( A X. A ) )
12	11	ex	|- ( y = A -> ( x e. A -> y = [ x ] ( A X. A ) ) )
13	12	ancld	|- ( y = A -> ( x e. A -> ( x e. A /\ y = [ x ] ( A X. A ) ) ) )
14	13	eximdv	|- ( y = A -> ( E. x x e. A -> E. x ( x e. A /\ y = [ x ] ( A X. A ) ) ) )
15	8 14	mpan9	|- ( ( A =/= (/) /\ y = A ) -> E. x ( x e. A /\ y = [ x ] ( A X. A ) ) )
16		df-rex	|- ( E. x e. A y = [ x ] ( A X. A ) <-> E. x ( x e. A /\ y = [ x ] ( A X. A ) ) )
17	15 16	sylibr	|- ( ( A =/= (/) /\ y = A ) -> E. x e. A y = [ x ] ( A X. A ) )
18	6 17	impbida	|- ( A =/= (/) -> ( E. x e. A y = [ x ] ( A X. A ) <-> y = A ) )
19		vex	|- y e. _V
20	19	elqs	|- ( y e. ( A /. ( A X. A ) ) <-> E. x e. A y = [ x ] ( A X. A ) )
21		velsn	|- ( y e. { A } <-> y = A )
22	18 20 21	3bitr4g	|- ( A =/= (/) -> ( y e. ( A /. ( A X. A ) ) <-> y e. { A } ) )
23	22	eqrdv	|- ( A =/= (/) -> ( A /. ( A X. A ) ) = { A } )