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

Metamath Proof Explorer

Theorem disjimdmqseq

Description: Disjointness implies unique-generation of quotient blocks. Converts existence-quotient comprehension (see df-qs ) into a uniqueness-comprehension under disjointness; rewrites ( dom R /. R ) carriers as exactly the class of blocks with a unique representative. This is the "unique generator per block" content in a carrier-normal form. (Contributed by Peter Mazsa, 5-Feb-2026)

Ref Expression
Assertion disjimdmqseq 
|- ( Disj R -> ( dom R /. R ) = { t | E! u e. dom R t = [ u ] R } )

Proof

Step Hyp Ref Expression
1 disjimrmoeqec 
 |-  ( Disj R -> E* u e. dom R t = [ u ] R )
2 1 biantrud 
 |-  ( Disj R -> ( t e. ( dom R /. R ) <-> ( t e. ( dom R /. R ) /\ E* u e. dom R t = [ u ] R ) ) )
3 elqsg 
 |-  ( t e. _V -> ( t e. ( dom R /. R ) <-> E. u e. dom R t = [ u ] R ) )
4 3 elv 
 |-  ( t e. ( dom R /. R ) <-> E. u e. dom R t = [ u ] R )
5 4 anbi1i 
 |-  ( ( t e. ( dom R /. R ) /\ E* u e. dom R t = [ u ] R ) <-> ( E. u e. dom R t = [ u ] R /\ E* u e. dom R t = [ u ] R ) )
6 reu5 
 |-  ( E! u e. dom R t = [ u ] R <-> ( E. u e. dom R t = [ u ] R /\ E* u e. dom R t = [ u ] R ) )
7 5 6 bitr4i 
 |-  ( ( t e. ( dom R /. R ) /\ E* u e. dom R t = [ u ] R ) <-> E! u e. dom R t = [ u ] R )
8 2 7 bitrdi 
 |-  ( Disj R -> ( t e. ( dom R /. R ) <-> E! u e. dom R t = [ u ] R ) )
9 8 eqabdv 
 |-  ( Disj R -> ( dom R /. R ) = { t | E! u e. dom R t = [ u ] R } )