Theorem 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	⊢ ( 𝑅 ∈ 𝑉 → ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ∼ 𝐴 = 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relcoels	⊢ Rel ∼ 𝐴
2	1	a1i	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → Rel ∼ 𝐴 )
3		eqvrelrel	⊢ ( EqvRel 𝑅 → Rel 𝑅 )
4	3	ad2antrl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → Rel 𝑅 )
5		brcoels	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝐴 𝑦 ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ) )
6	5	el2v	⊢ ( 𝑥 ∼ 𝐴 𝑦 ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) )
7		simpll	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → EqvRel 𝑅 )
8		simprl	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → 𝑢 ∈ 𝐴 )
9		simplr	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → ( dom 𝑅 / 𝑅 ) = 𝐴 )
10	8 9	eleqtrrd	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → 𝑢 ∈ ( dom 𝑅 / 𝑅 ) )
11		simprr	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → 𝑥 ∈ 𝑢 )
12		eqvrelqsel	⊢ ( ( EqvRel 𝑅 ∧ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑥 ∈ 𝑢 ) → 𝑢 = [ 𝑥 ] 𝑅 )
13	7 10 11 12	syl3anc	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → 𝑢 = [ 𝑥 ] 𝑅 )
14	13	eleq2d	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → ( 𝑦 ∈ 𝑢 ↔ 𝑦 ∈ [ 𝑥 ] 𝑅 ) )
15		elecALTV	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑦 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝑦 ) )
16	15	el2v	⊢ ( 𝑦 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝑦 )
17	14 16	bitrdi	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑥 ∈ 𝑢 ) ) → ( 𝑦 ∈ 𝑢 ↔ 𝑥 𝑅 𝑦 ) )
18	17	anassrs	⊢ ( ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑢 ) → ( 𝑦 ∈ 𝑢 ↔ 𝑥 𝑅 𝑦 ) )
19	18	pm5.32da	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑥 𝑅 𝑦 ) ) )
20	19	rexbidva	⊢ ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑥 𝑅 𝑦 ) ) )
21	20	adantl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑥 𝑅 𝑦 ) ) )
22		simpll	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ 𝑥 𝑅 𝑦 ) → EqvRel 𝑅 )
23		simpr	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 𝑅 𝑦 )
24	22 23	eqvrelcl	⊢ ( ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ dom 𝑅 )
25	24	adantll	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ dom 𝑅 )
26		eqvrelim	⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅 )
27	26	ad2antrl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → dom 𝑅 = ran 𝑅 )
28	27	eleq2d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ ran 𝑅 ) )
29		dmqseqim2	⊢ ( 𝑅 ∈ 𝑉 → ( Rel 𝑅 → ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ( 𝑥 ∈ ran 𝑅 ↔ 𝑥 ∈ ∪ 𝐴 ) ) ) )
30	3 29	syl5	⊢ ( 𝑅 ∈ 𝑉 → ( EqvRel 𝑅 → ( ( dom 𝑅 / 𝑅 ) = 𝐴 → ( 𝑥 ∈ ran 𝑅 ↔ 𝑥 ∈ ∪ 𝐴 ) ) ) )
31	30	imp32	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 ∈ ran 𝑅 ↔ 𝑥 ∈ ∪ 𝐴 ) )
32	28 31	bitrd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ ∪ 𝐴 ) )
33		eluni2	⊢ ( 𝑥 ∈ ∪ 𝐴 ↔ ∃ 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
34	32 33	bitrdi	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ) )
35	34	adantr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( 𝑥 ∈ dom 𝑅 ↔ ∃ 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ) )
36	25 35	mpbid	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 )
37	36	ex	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 𝑅 𝑦 → ∃ 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ) )
38	37	pm4.71rd	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ∧ 𝑥 𝑅 𝑦 ) ) )
39		r19.41v	⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑥 𝑅 𝑦 ) ↔ ( ∃ 𝑢 ∈ 𝐴 𝑥 ∈ 𝑢 ∧ 𝑥 𝑅 𝑦 ) )
40	38 39	bitr4di	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑥 𝑅 𝑦 ) ) )
41	21 40	bitr4d	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) ↔ 𝑥 𝑅 𝑦 ) )
42	6 41	bitrid	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ( 𝑥 ∼ 𝐴 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
43	2 4 42	eqbrrdv	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) ) → ∼ 𝐴 = 𝑅 )
44	43	ex	⊢ ( 𝑅 ∈ 𝑉 → ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ∼ 𝐴 = 𝑅 ) )