Theorem xmeter

Description: The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypothesis	xmeter.1	⊢ ∼ = ( ◡ 𝐷 “ ℝ )
Assertion	xmeter	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∼ Er 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		xmeter.1	⊢ ∼ = ( ◡ 𝐷 “ ℝ )
2		cnvimass	⊢ ( ◡ 𝐷 “ ℝ ) ⊆ dom 𝐷
3	1 2	eqsstri	⊢ ∼ ⊆ dom 𝐷
4		xmetf	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
5	3 4	fssdm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∼ ⊆ ( 𝑋 × 𝑋 ) )
6		relxp	⊢ Rel ( 𝑋 × 𝑋 )
7		relss	⊢ ( ∼ ⊆ ( 𝑋 × 𝑋 ) → ( Rel ( 𝑋 × 𝑋 ) → Rel ∼ ) )
8	5 6 7	mpisyl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → Rel ∼ )
9	1	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) ) )
10	9	biimpa	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
11	10	simp2d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝑦 ∈ 𝑋 )
12	10	simp1d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝑥 ∈ 𝑋 )
13		simpl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
15	13 12 11 14	syl3anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
16	10	simp3d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
17	15 16	eqeltrrd	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑦 𝐷 𝑥 ) ∈ ℝ )
18	1	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑥 ) ∈ ℝ ) ) )
19	18	adantr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑥 ) ∈ ℝ ) ) )
20	11 12 17 19	mpbir3and	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝑦 ∼ 𝑥 )
21	12	adantrr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑥 ∈ 𝑋 )
22	1	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑦 ∼ 𝑧 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) ) )
23	22	biimpa	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∼ 𝑧 ) → ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) )
24	23	adantrl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) )
25	24	simp2d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑧 ∈ 𝑋 )
26		simpl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
27	16	adantrr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
28	24	simp3d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ )
29		rexadd	⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) → ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) = ( ( 𝑥 𝐷 𝑦 ) + ( 𝑦 𝐷 𝑧 ) ) )
30		readdcl	⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) → ( ( 𝑥 𝐷 𝑦 ) + ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ )
31	29 30	eqeltrd	⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) → ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ )
32	27 28 31	syl2anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ )
33	11	adantrr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑦 ∈ 𝑋 )
34		xmettri	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑧 ) ≤ ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) )
35	26 21 25 33 34	syl13anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 𝐷 𝑧 ) ≤ ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) )
36		xmetlecl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ ∧ ( 𝑥 𝐷 𝑧 ) ≤ ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ) ) → ( 𝑥 𝐷 𝑧 ) ∈ ℝ )
37	26 21 25 32 35 36	syl122anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 𝐷 𝑧 ) ∈ ℝ )
38	1	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑧 ) ∈ ℝ ) ) )
39	38	adantr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑧 ) ∈ ℝ ) ) )
40	21 25 37 39	mpbir3and	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑥 ∼ 𝑧 )
41		xmet0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑥 ) = 0 )
42		0re	⊢ 0 ∈ ℝ
43	41 42	eqeltrdi	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑥 ) ∈ ℝ )
44	43	ex	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 → ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) )
45	44	pm4.71rd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ ( ( 𝑥 𝐷 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ) )
46		df-3an	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) )
47		anidm	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ↔ 𝑥 ∈ 𝑋 )
48	47	anbi2ci	⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ↔ ( ( 𝑥 𝐷 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) )
49	46 48	bitri	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ↔ ( ( 𝑥 𝐷 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) )
50	45 49	bitr4di	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ) )
51	1	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ) )
52	50 51	bitr4d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∼ 𝑥 ) )
53	8 20 40 52	iserd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∼ Er 𝑋 )