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	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )

Metamath Proof Explorer

Theorem erth

Proof