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 ( 𝐴 ≠ ∅ → ( 𝐴 / ( 𝐴 × 𝐴 ) ) = { 𝐴 } )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) → 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) )
2 ecxpid ⊢ ( 𝑥 ∈ 𝐴 → [ 𝑥 ] ( 𝐴 × 𝐴 ) = 𝐴 )
3 2 adantr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) → [ 𝑥 ] ( 𝐴 × 𝐴 ) = 𝐴 )
4 1 3 eqtrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) → 𝑦 = 𝐴 )
5 4 rexlimiva ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) → 𝑦 = 𝐴 )
6 5 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) → 𝑦 = 𝐴 )
7 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
8 7 biimpi ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐴 )
9 simpl ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 = 𝐴 )
10 2 adantl ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑥 ] ( 𝐴 × 𝐴 ) = 𝐴 )
11 9 10 eqtr4d ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) )
12 11 ex ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) )
13 12 ancld ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) ) )
14 13 eximdv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) ) )
15 8 14 mpan9 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝑦 = 𝐴 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) )
16 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ) )
17 15 16 sylibr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝑦 = 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) )
18 6 17 impbida ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) ↔ 𝑦 = 𝐴 ) )
19 vex ⊢ 𝑦 ∈ V
20 19 elqs ⊢ ( 𝑦 ∈ ( 𝐴 / ( 𝐴 × 𝐴 ) ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] ( 𝐴 × 𝐴 ) )
21 velsn ⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
22 18 20 21 3bitr4g ⊢ ( 𝐴 ≠ ∅ → ( 𝑦 ∈ ( 𝐴 / ( 𝐴 × 𝐴 ) ) ↔ 𝑦 ∈ { 𝐴 } ) )
23 22 eqrdv ⊢ ( 𝐴 ≠ ∅ → ( 𝐴 / ( 𝐴 × 𝐴 ) ) = { 𝐴 } )