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