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 R \to \exists^{*} u \in dom R t = [u] R$

Proof

Step	Hyp	Ref	Expression
1		disjimeceqim	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v)$
2		eqtr2	$⊢ (t = [u] R \land t = [v] R) \to [u] R = [v] R$
3	2	imim1i	$⊢ ([u] R = [v] R \to u = v) \to ((t = [u] R \land t = [v] R) \to u = v)$
4	3	2ralimi	$⊢ \forall u \in dom R \forall v \in dom R ([u] R = [v] R \to u = v) \to \forall u \in dom R \forall v \in dom R ((t = [u] R \land t = [v] R) \to u = v)$
5	1 4	syl	$⊢ Disj R \to \forall u \in dom R \forall v \in dom R ((t = [u] R \land t = [v] R) \to u = v)$
6		eceq1	$⊢ u = v \to [u] R = [v] R$
7	6	eqeq2d	$⊢ u = v \to (t = [u] R \leftrightarrow t = [v] R)$
8	7	rmo4	$⊢ \exists^{*} u \in dom R t = [u] R \leftrightarrow \forall u \in dom R \forall v \in dom R ((t = [u] R \land t = [v] R) \to u = v)$
9	5 8	sylibr	$⊢ Disj R \to \exists^{*} u \in dom R t = [u] R$

Metamath Proof Explorer

Theorem disjimrmoeqec

Proof