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	⊢ ( 𝜑 → Rel 𝑅 )
	iserd.2	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 𝑅 𝑥 )
	iserd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 )
	iserd.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 ) )
Assertion	iserd	⊢ ( 𝜑 → 𝑅 Er 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		iserd.1	⊢ ( 𝜑 → Rel 𝑅 )
2		iserd.2	⊢ ( ( 𝜑 ∧ 𝑥 𝑅 𝑦 ) → 𝑦 𝑅 𝑥 )
3		iserd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 )
4		iserd.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 ) )
5		eqidd	⊢ ( 𝜑 → dom 𝑅 = dom 𝑅 )
6	2	ex	⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) )
7	3	ex	⊢ ( 𝜑 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
8	6 7	jca	⊢ ( 𝜑 → ( ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
9	8	alrimiv	⊢ ( 𝜑 → ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
10	9	alrimiv	⊢ ( 𝜑 → ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
11	10	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
12		dfer2	⊢ ( 𝑅 Er dom 𝑅 ↔ ( Rel 𝑅 ∧ dom 𝑅 = dom 𝑅 ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 ) ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
13	1 5 11 12	syl3anbrc	⊢ ( 𝜑 → 𝑅 Er dom 𝑅 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝑅 ) → 𝑅 Er dom 𝑅 )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝑅 ) → 𝑥 ∈ dom 𝑅 )
16	14 15	erref	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝑅 ) → 𝑥 𝑅 𝑥 )
17	16	ex	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝑅 → 𝑥 𝑅 𝑥 ) )
18		vex	⊢ 𝑥 ∈ V
19	18 18	breldm	⊢ ( 𝑥 𝑅 𝑥 → 𝑥 ∈ dom 𝑅 )
20	17 19	impbid1	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝑅 ↔ 𝑥 𝑅 𝑥 ) )
21	20 4	bitr4d	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ 𝐴 ) )
22	21	eqrdv	⊢ ( 𝜑 → dom 𝑅 = 𝐴 )
23		ereq2	⊢ ( dom 𝑅 = 𝐴 → ( 𝑅 Er dom 𝑅 ↔ 𝑅 Er 𝐴 ) )
24	22 23	syl	⊢ ( 𝜑 → ( 𝑅 Er dom 𝑅 ↔ 𝑅 Er 𝐴 ) )
25	13 24	mpbid	⊢ ( 𝜑 → 𝑅 Er 𝐴 )