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 ⊢ ( 𝜑 → 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 𝐴 )