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

Metamath Proof Explorer

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 𝑅 / 𝑅 ) = 𝐴 ) → ∼ 𝐴 = 𝑅 ) )