erimeq2

Description: Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 in a more convenient form , see also erimeq ). (Contributed by Rodolfo Medina, 19-Oct-2010) (Proof shortened by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 29-Dec-2021)

		Ref	Expression
	Assertion	erimeq2	$⊢ R \in V \to ((EqvRel R \land dom R / R = A) \to \sim A = R)$

Proof

Step	Hyp	Ref	Expression
1		relcoels	$⊢ Rel \sim A$
2	1	a1i	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to Rel \sim A$
3		eqvrelrel	$⊢ EqvRel R \to Rel R$
4	3	ad2antrl	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to Rel R$
5		brcoels	$⊢ (x \in V \land y \in V) \to (x \sim A y \leftrightarrow \exists u \in A (x \in u \land y \in u))$
6	5	el2v	$⊢ x \sim A y \leftrightarrow \exists u \in A (x \in u \land y \in u)$
7		simpll	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to EqvRel R$
8		simprl	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to u \in A$
9		simplr	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to dom R / R = A$
10	8 9	eleqtrrd	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to u \in (dom R / R)$
11		simprr	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to x \in u$
12		eqvrelqsel	$⊢ (EqvRel R \land u \in (dom R / R) \land x \in u) \to u = [x] R$
13	7 10 11 12	syl3anc	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to u = [x] R$
14	13	eleq2d	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to (y \in u \leftrightarrow y \in [x] R)$
15		elecALTV	$⊢ (x \in V \land y \in V) \to (y \in [x] R \leftrightarrow x R y)$
16	15	el2v	$⊢ y \in [x] R \leftrightarrow x R y$
17	14 16	bitrdi	$⊢ ((EqvRel R \land dom R / R = A) \land (u \in A \land x \in u)) \to (y \in u \leftrightarrow x R y)$
18	17	anassrs	$⊢ (((EqvRel R \land dom R / R = A) \land u \in A) \land x \in u) \to (y \in u \leftrightarrow x R y)$
19	18	pm5.32da	$⊢ ((EqvRel R \land dom R / R = A) \land u \in A) \to ((x \in u \land y \in u) \leftrightarrow (x \in u \land x R y))$
20	19	rexbidva	$⊢ (EqvRel R \land dom R / R = A) \to (\exists u \in A (x \in u \land y \in u) \leftrightarrow \exists u \in A (x \in u \land x R y))$
21	20	adantl	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (\exists u \in A (x \in u \land y \in u) \leftrightarrow \exists u \in A (x \in u \land x R y))$
22		simpll	$⊢ ((EqvRel R \land dom R / R = A) \land x R y) \to EqvRel R$
23		simpr	$⊢ ((EqvRel R \land dom R / R = A) \land x R y) \to x R y$
24	22 23	eqvrelcl	$⊢ ((EqvRel R \land dom R / R = A) \land x R y) \to x \in dom R$
25	24	adantll	$⊢ ((R \in V \land (EqvRel R \land dom R / R = A)) \land x R y) \to x \in dom R$
26		eqvrelim	$⊢ EqvRel R \to dom R = ran R$
27	26	ad2antrl	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to dom R = ran R$
28	27	eleq2d	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x \in dom R \leftrightarrow x \in ran R)$
29		dmqseqim2	$⊢ R \in V \to (Rel R \to (dom R / R = A \to (x \in ran R \leftrightarrow x \in ⋃ A)))$
30	3 29	syl5	$⊢ R \in V \to (EqvRel R \to (dom R / R = A \to (x \in ran R \leftrightarrow x \in ⋃ A)))$
31	30	imp32	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x \in ran R \leftrightarrow x \in ⋃ A)$
32	28 31	bitrd	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x \in dom R \leftrightarrow x \in ⋃ A)$
33		eluni2	$⊢ x \in ⋃ A \leftrightarrow \exists u \in A x \in u$
34	32 33	bitrdi	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x \in dom R \leftrightarrow \exists u \in A x \in u)$
35	34	adantr	$⊢ ((R \in V \land (EqvRel R \land dom R / R = A)) \land x R y) \to (x \in dom R \leftrightarrow \exists u \in A x \in u)$
36	25 35	mpbid	$⊢ ((R \in V \land (EqvRel R \land dom R / R = A)) \land x R y) \to \exists u \in A x \in u$
37	36	ex	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x R y \to \exists u \in A x \in u)$
38	37	pm4.71rd	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x R y \leftrightarrow (\exists u \in A x \in u \land x R y))$
39		r19.41v	$⊢ \exists u \in A (x \in u \land x R y) \leftrightarrow (\exists u \in A x \in u \land x R y)$
40	38 39	bitr4di	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x R y \leftrightarrow \exists u \in A (x \in u \land x R y))$
41	21 40	bitr4d	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (\exists u \in A (x \in u \land y \in u) \leftrightarrow x R y)$
42	6 41	bitrid	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to (x \sim A y \leftrightarrow x R y)$
43	2 4 42	eqbrrdv	$⊢ (R \in V \land (EqvRel R \land dom R / R = A)) \to \sim A = R$
44	43	ex	$⊢ R \in V \to ((EqvRel R \land dom R / R = A) \to \sim A = R)$

Metamath Proof Explorer

Theorem erimeq2

Proof