metdscnlem

	Ref	Expression
Hypotheses	metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
	metdscn.j	$⊢ J = MetOpen (D)$
	metdscn.c	$⊢ C = dist (ℝ_{𝑠}^{*})$
	metdscn.k	$⊢ K = MetOpen (C)$
	metdscnlem.1	$⊢ φ \to D \in ∞Met (X)$
	metdscnlem.2	$⊢ φ \to S \subseteq X$
	metdscnlem.3	$⊢ φ \to A \in X$
	metdscnlem.4	$⊢ φ \to B \in X$
	metdscnlem.5	$⊢ φ \to R \in ℝ^{+}$
	metdscnlem.6	$⊢ φ \to A D B < R$
Assertion	metdscnlem	$⊢ φ \to F (A) +_{𝑒} (- F (B)) < R$

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	$⊢ F = (x \in X ⟼ sup (ran (y \in S ⟼ x D y) ℝ^{*} <))$
2		metdscn.j	$⊢ J = MetOpen (D)$
3		metdscn.c	$⊢ C = dist (ℝ_{𝑠}^{*})$
4		metdscn.k	$⊢ K = MetOpen (C)$
5		metdscnlem.1	$⊢ φ \to D \in ∞Met (X)$
6		metdscnlem.2	$⊢ φ \to S \subseteq X$
7		metdscnlem.3	$⊢ φ \to A \in X$
8		metdscnlem.4	$⊢ φ \to B \in X$
9		metdscnlem.5	$⊢ φ \to R \in ℝ^{+}$
10		metdscnlem.6	$⊢ φ \to A D B < R$
11	1	metdsf	$⊢ (D \in ∞Met (X) \land S \subseteq X) \to F : X ⟶ [0, +∞]$
12	5 6 11	syl2anc	$⊢ φ \to F : X ⟶ [0, +∞]$
13	12 7	ffvelrnd	$⊢ φ \to F (A) \in [0, +∞]$
14		eliccxr	$⊢ F (A) \in [0, +∞] \to F (A) \in ℝ^{*}$
15	13 14	syl	$⊢ φ \to F (A) \in ℝ^{*}$
16	12 8	ffvelrnd	$⊢ φ \to F (B) \in [0, +∞]$
17		eliccxr	$⊢ F (B) \in [0, +∞] \to F (B) \in ℝ^{*}$
18	16 17	syl	$⊢ φ \to F (B) \in ℝ^{*}$
19	18	xnegcld	$⊢ φ \to - F (B) \in ℝ^{*}$
20	15 19	xaddcld	$⊢ φ \to F (A) +_{𝑒} (- F (B)) \in ℝ^{*}$
21		xmetcl	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to A D B \in ℝ^{*}$
22	5 7 8 21	syl3anc	$⊢ φ \to A D B \in ℝ^{*}$
23	9	rpxrd	$⊢ φ \to R \in ℝ^{*}$
24	1	metdstri	$⊢ ((D \in ∞Met (X) \land S \subseteq X) \land (A \in X \land B \in X)) \to F (A) \leq (A D B) +_{𝑒} F (B)$
25	5 6 7 8 24	syl22anc	$⊢ φ \to F (A) \leq (A D B) +_{𝑒} F (B)$
26		elxrge0	$⊢ F (A) \in [0, +∞] \leftrightarrow (F (A) \in ℝ^{*} \land 0 \leq F (A))$
27	26	simprbi	$⊢ F (A) \in [0, +∞] \to 0 \leq F (A)$
28	13 27	syl	$⊢ φ \to 0 \leq F (A)$
29		elxrge0	$⊢ F (B) \in [0, +∞] \leftrightarrow (F (B) \in ℝ^{*} \land 0 \leq F (B))$
30	29	simprbi	$⊢ F (B) \in [0, +∞] \to 0 \leq F (B)$
31	16 30	syl	$⊢ φ \to 0 \leq F (B)$
32		ge0nemnf	$⊢ (F (B) \in ℝ^{*} \land 0 \leq F (B)) \to F (B) \neq −∞$
33	18 31 32	syl2anc	$⊢ φ \to F (B) \neq −∞$
34		xmetge0	$⊢ (D \in ∞Met (X) \land A \in X \land B \in X) \to 0 \leq A D B$
35	5 7 8 34	syl3anc	$⊢ φ \to 0 \leq A D B$
36		xlesubadd	$⊢ ((F (A) \in ℝ^{} \land F (B) \in ℝ^{} \land A D B \in ℝ^{*}) \land (0 \leq F (A) \land F (B) \neq −∞ \land 0 \leq A D B)) \to (F (A) +_{𝑒} (- F (B)) \leq A D B \leftrightarrow F (A) \leq (A D B) +_{𝑒} F (B))$
37	15 18 22 28 33 35 36	syl33anc	$⊢ φ \to (F (A) +_{𝑒} (- F (B)) \leq A D B \leftrightarrow F (A) \leq (A D B) +_{𝑒} F (B))$
38	25 37	mpbird	$⊢ φ \to F (A) +_{𝑒} (- F (B)) \leq A D B$
39	20 22 23 38 10	xrlelttrd	$⊢ φ \to F (A) +_{𝑒} (- F (B)) < R$

Metamath Proof Explorer

Theorem metdscnlem

Proof