Metamath Proof Explorer

Theorem eqvrelth

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) (Revised by Peter Mazsa, 2-Jun-2019)

Ref Expression
Hypotheses eqvrelth.1 ⊢ ( 𝜑 → EqvRel 𝑅 )
eqvrelth.2 ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )
Assertion eqvrelth ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )

Proof

Step Hyp Ref Expression
1 eqvrelth.1 ⊢ ( 𝜑 → EqvRel 𝑅 )
2 eqvrelth.2 ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )
3 1 eqvrelsymb ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )
4 3 biimpa ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 𝑅 𝐴 )
5 1 eqvreltr ⊢ ( 𝜑 → ( ( 𝐵 𝑅 𝐴 ∧ 𝐴 𝑅 𝑥 ) → 𝐵 𝑅 𝑥 ) )
6 5 impl ⊢ ( ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) ∧ 𝐴 𝑅 𝑥 ) → 𝐵 𝑅 𝑥 )
7 4 6 syldanl ⊢ ( ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐴 𝑅 𝑥 ) → 𝐵 𝑅 𝑥 )
8 1 eqvreltr ⊢ ( 𝜑 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝑥 ) → 𝐴 𝑅 𝑥 ) )
9 8 impl ⊢ ( ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) ∧ 𝐵 𝑅 𝑥 ) → 𝐴 𝑅 𝑥 )
10 7 9 impbida ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 𝑅 𝑥 ↔ 𝐵 𝑅 𝑥 ) )
11 vex ⊢ 𝑥 ∈ V
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 )
13 elecg ⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ dom 𝑅 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
14 11 12 13 sylancr ⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
15 eqvrelrel ⊢ ( EqvRel 𝑅 → 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 ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → EqvRel 𝑅 )
24 1 2 eqvrelref ⊢ ( 𝜑 → 𝐴 𝑅 𝐴 )
25 24 adantr ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 𝑅 𝐴 )
26 2 adantr ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 ∈ dom 𝑅 )
27 elecALTV ⊢ ( ( 𝐴 ∈ dom 𝑅 ∧ 𝐴 ∈ dom 𝑅 ) → ( 𝐴 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐴 ) )
28 26 26 27 syl2anc ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → ( 𝐴 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝐴 ) )
29 25 28 mpbird ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 ∈ [ 𝐴 ] 𝑅 )
30 simpr ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
31 29 30 eleqtrd ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 ∈ [ 𝐵 ] 𝑅 )
32 30 dmec2d ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → ( 𝐴 ∈ dom 𝑅 ↔ 𝐵 ∈ dom 𝑅 ) )
33 26 32 mpbid ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐵 ∈ dom 𝑅 )
34 elecALTV ⊢ ( ( 𝐵 ∈ dom 𝑅 ∧ 𝐴 ∈ dom 𝑅 ) → ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝐴 ) )
35 33 26 34 syl2anc ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → ( 𝐴 ∈ [ 𝐵 ] 𝑅 ↔ 𝐵 𝑅 𝐴 ) )
36 31 35 mpbid ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐵 𝑅 𝐴 )
37 23 36 eqvrelsym ⊢ ( ( 𝜑 ∧ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) → 𝐴 𝑅 𝐵 )
38 22 37 impbida ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )