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 𝑅 𝑡 = [ 𝑢 ] 𝑅 )