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

Metamath Proof Explorer

Theorem iserd

Description: A reflexive, symmetric, transitive relation is an equivalence relation on its domain. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses iserd.1 
|- ( ph -> Rel R )
iserd.2 
|- ( ( ph /\ x R y ) -> y R x )
iserd.3 
|- ( ( ph /\ ( x R y /\ y R z ) ) -> x R z )
iserd.4 
|- ( ph -> ( x e. A <-> x R x ) )
Assertion iserd 
|- ( ph -> R Er A )

Proof

Step Hyp Ref Expression
1 iserd.1 
 |-  ( ph -> Rel R )
2 iserd.2 
 |-  ( ( ph /\ x R y ) -> y R x )
3 iserd.3 
 |-  ( ( ph /\ ( x R y /\ y R z ) ) -> x R z )
4 iserd.4 
 |-  ( ph -> ( x e. A <-> x R x ) )
5 eqidd 
 |-  ( ph -> dom R = dom R )
6 2 ex 
 |-  ( ph -> ( x R y -> y R x ) )
7 3 ex 
 |-  ( ph -> ( ( x R y /\ y R z ) -> x R z ) )
8 6 7 jca 
 |-  ( ph -> ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) )
9 8 alrimiv 
 |-  ( ph -> A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) )
10 9 alrimiv 
 |-  ( ph -> A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) )
11 10 alrimiv 
 |-  ( ph -> A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) )
12 dfer2 
 |-  ( R Er dom R <-> ( Rel R /\ dom R = dom R /\ A. x A. y A. z ( ( x R y -> y R x ) /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
13 1 5 11 12 syl3anbrc 
 |-  ( ph -> R Er dom R )
14 13 adantr 
 |-  ( ( ph /\ x e. dom R ) -> R Er dom R )
15 simpr 
 |-  ( ( ph /\ x e. dom R ) -> x e. dom R )
16 14 15 erref 
 |-  ( ( ph /\ x e. dom R ) -> x R x )
17 16 ex 
 |-  ( ph -> ( x e. dom R -> x R x ) )
18 vex 
 |-  x e. _V
19 18 18 breldm 
 |-  ( x R x -> x e. dom R )
20 17 19 impbid1 
 |-  ( ph -> ( x e. dom R <-> x R x ) )
21 20 4 bitr4d 
 |-  ( ph -> ( x e. dom R <-> x e. A ) )
22 21 eqrdv 
 |-  ( ph -> dom R = A )
23 ereq2 
 |-  ( dom R = A -> ( R Er dom R <-> R Er A ) )
24 22 23 syl 
 |-  ( ph -> ( R Er dom R <-> R Er A ) )
25 13 24 mpbid 
 |-  ( ph -> R Er A )