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

Metamath Proof Explorer

Theorem disjimrmoeqec

Description: Under Disj , every block has a unique generator ( E* form). If t is a block in the quotient sense, then there is a uniquely determined u in dom R such that t = [ u ] R . This is the existence+uniqueness engine behind Disjs and QMap characterizations: it is the "representative theorem" from which the E! forms are obtained. (Contributed by Peter Mazsa, 5-Feb-2026)

Ref Expression
Assertion disjimrmoeqec ( Disj 𝑅 → ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 )

Proof

Step Hyp Ref Expression
1 disjimeceqim ⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) )
2 eqtr2 ⊢ ( ( 𝑡 = [ 𝑢 ] 𝑅 ∧ 𝑡 = [ 𝑣 ] 𝑅 ) → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 )
3 2 imim1i ⊢ ( ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) → ( ( 𝑡 = [ 𝑢 ] 𝑅 ∧ 𝑡 = [ 𝑣 ] 𝑅 ) → 𝑢 = 𝑣 ) )
4 3 2ralimi ⊢ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 → 𝑢 = 𝑣 ) → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( 𝑡 = [ 𝑢 ] 𝑅 ∧ 𝑡 = [ 𝑣 ] 𝑅 ) → 𝑢 = 𝑣 ) )
5 1 4 syl ⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( 𝑡 = [ 𝑢 ] 𝑅 ∧ 𝑡 = [ 𝑣 ] 𝑅 ) → 𝑢 = 𝑣 ) )
6 eceq1 ⊢ ( 𝑢 = 𝑣 → [ 𝑢 ] 𝑅 = [ 𝑣 ] 𝑅 )
7 6 eqeq2d ⊢ ( 𝑢 = 𝑣 → ( 𝑡 = [ 𝑢 ] 𝑅 ↔ 𝑡 = [ 𝑣 ] 𝑅 ) )
8 7 rmo4 ⊢ ( ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 ↔ ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑣 ∈ dom 𝑅 ( ( 𝑡 = [ 𝑢 ] 𝑅 ∧ 𝑡 = [ 𝑣 ] 𝑅 ) → 𝑢 = 𝑣 ) )
9 5 8 sylibr ⊢ ( Disj 𝑅 → ∃* 𝑢 ∈ dom 𝑅 𝑡 = [ 𝑢 ] 𝑅 )