Theorem qseq

Description: The quotient set equal to a class.

This theorem is used when a class A is identified with a quotient ( dom R /. R ) . In such a situation, every element u e. A is an R-coset [ v ] R for some v e. dom R , but there is no requirement that the "witness" v be equal to its own block [ v ] R . A is a set of blocks (equivalence classes), not a set of raw witnesses. In particular, when ( dom R /. R ) = A is read together with a partition hypothesis R Part A (defined as dfpart2 ), A is being treated as the set of blocks [ v ] R ; it does not assert any fixed-point condition v = [ v ] R such as would arise from the mistaken reading u e. A <-> u = [ u ] R . Cf. dmqsblocks . (Contributed by Peter Mazsa, 19-Oct-2018)

	Ref	Expression
Assertion	qseq	⊢ ( ( 𝐵 / 𝑅 ) = 𝐴 ↔ ∀ 𝑢 ( 𝑢 ∈ 𝐴 ↔ ∃ 𝑣 ∈ 𝐵 𝑢 = [ 𝑣 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		df-qs	⊢ ( 𝐵 / 𝑅 ) = { 𝑢 ∣ ∃ 𝑣 ∈ 𝐵 𝑢 = [ 𝑣 ] 𝑅 }
2	1	eqeq2i	⊢ ( 𝐴 = ( 𝐵 / 𝑅 ) ↔ 𝐴 = { 𝑢 ∣ ∃ 𝑣 ∈ 𝐵 𝑢 = [ 𝑣 ] 𝑅 } )
3		eqcom	⊢ ( 𝐴 = ( 𝐵 / 𝑅 ) ↔ ( 𝐵 / 𝑅 ) = 𝐴 )
4		eqabb	⊢ ( 𝐴 = { 𝑢 ∣ ∃ 𝑣 ∈ 𝐵 𝑢 = [ 𝑣 ] 𝑅 } ↔ ∀ 𝑢 ( 𝑢 ∈ 𝐴 ↔ ∃ 𝑣 ∈ 𝐵 𝑢 = [ 𝑣 ] 𝑅 ) )
5	2 3 4	3bitr3i	⊢ ( ( 𝐵 / 𝑅 ) = 𝐴 ↔ ∀ 𝑢 ( 𝑢 ∈ 𝐴 ↔ ∃ 𝑣 ∈ 𝐵 𝑢 = [ 𝑣 ] 𝑅 ) )