This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )