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 )