Metamath Proof Explorer

Theorem erth

Description: Basic property of equivalence relations. Theorem 73 of Suppes p. 82. (Contributed by NM, 23-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses erth.1 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
erth.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion erth ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )

Proof

Step Hyp Ref Expression
1 erth.1 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2 erth.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3 1 ersymb ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )
4 3 biimpa ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 𝑅 𝐴 )
5 1 ertr ⊢ ( 𝜑 → ( ( 𝐵 𝑅 𝐴 ∧ 𝐴 𝑅 𝑥 ) → 𝐵 𝑅 𝑥 ) )
6 5 impl ⊢ ( ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) ∧ 𝐴 𝑅 𝑥 ) → 𝐵 𝑅 𝑥 )
7 4 6 syldanl ⊢ ( ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐴 𝑅 𝑥 ) → 𝐵 𝑅 𝑥 )
8 1 ertr ⊢ ( 𝜑 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝑥 ) → 𝐴 𝑅 𝑥 ) )
9 8 impl ⊢ ( ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐵 𝑅 𝑥 ) → 𝐴 𝑅 𝑥 )
10 7 9 impbida ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 𝑅 𝑥 ↔ 𝐵 𝑅 𝑥 ) )
11 vex ⊢ 𝑥 ∈ V
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ 𝑋 )
13 elecg ⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
14 11 12 13 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
15 errel ⊢ ( 𝑅 Er 𝑋 → Rel 𝑅 )
16 1 15 syl ⊢ ( 𝜑 → Rel 𝑅 )
17 brrelex2 ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 ∈ V )
18 16 17 sylan ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 ∈ V )
19 elecg ⊢ ( ( 𝑥 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) )
20 11 18 19 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝑥 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝑥 ) )
21 10 14 20 3bitr4d ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝑥 ∈ [ 𝐵 ] 𝑅 ) )
22 21 eqrdv ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
23 1 adantr ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝑅 Er 𝑋 )
24 1 2 erref ⊢ ( 𝜑 → 𝐴 𝑅 𝐴 )
25 24 adantr ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 𝑅 𝐴 )
26 2 adantr ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 ∈ 𝑋 )
27 elecg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐴 ) )
28 26 26 27 syl2anc ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → ( 𝐴 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐴 ) )
29 25 28 mpbird ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 ∈ [ 𝐴 ] 𝑅 )
30 simpr ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
31 29 30 eleqtrd ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 ∈ [ 𝐵 ] 𝑅 )
32 23 30 ereldm ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → ( 𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋 ) )
33 26 32 mpbid ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐵 ∈ 𝑋 )
34 elecg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝐴 ) )
35 26 33 34 syl2anc ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝐴 ) )
36 31 35 mpbid ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐵 𝑅 𝐴 )
37 23 36 ersym ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 𝑅 𝐵 )
38 22 37 impbida ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )