xlebnum

Description: Generalize lebnum to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015)

	Ref	Expression
Hypotheses	xlebnum.j	$⊢ J = MetOpen (D)$
	xlebnum.d	$⊢ φ \to D \in ∞Met (X)$
	xlebnum.c	$⊢ φ \to J \in Comp$
	xlebnum.s	$⊢ φ \to U \subseteq J$
	xlebnum.u	$⊢ φ \to X = ⋃ U$
Assertion	xlebnum	$⊢ φ \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$

Proof

Step	Hyp	Ref	Expression
1		xlebnum.j	$⊢ J = MetOpen (D)$
2		xlebnum.d	$⊢ φ \to D \in ∞Met (X)$
3		xlebnum.c	$⊢ φ \to J \in Comp$
4		xlebnum.s	$⊢ φ \to U \subseteq J$
5		xlebnum.u	$⊢ φ \to X = ⋃ U$
6		eqid	$⊢ MetOpen ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) = MetOpen ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)))$
7		1rp	$⊢ 1 \in ℝ^{+}$
8		eqid	$⊢ (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) = (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))$
9	8	stdbdmet	$⊢ (D \in ∞Met (X) \land 1 \in ℝ^{+}) \to (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) \in Met (X)$
10	2 7 9	sylancl	$⊢ φ \to (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) \in Met (X)$
11		rpxr	$⊢ 1 \in ℝ^{+} \to 1 \in ℝ^{*}$
12	7 11	mp1i	$⊢ φ \to 1 \in ℝ^{*}$
13		0lt1	$⊢ 0 < 1$
14	13	a1i	$⊢ φ \to 0 < 1$
15	8 1	stdbdmopn	$⊢ (D \in ∞Met (X) \land 1 \in ℝ^{*} \land 0 < 1) \to J = MetOpen ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)))$
16	2 12 14 15	syl3anc	$⊢ φ \to J = MetOpen ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)))$
17	16 3	eqeltrrd	$⊢ φ \to MetOpen ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) \in Comp$
18	4 16	sseqtrd	$⊢ φ \to U \subseteq MetOpen ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)))$
19	6 10 17 18 5	lebnum	$⊢ φ \to \exists r \in ℝ^{+} \forall x \in X \exists u \in U x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \subseteq u$
20		simpr	$⊢ (φ \land r \in ℝ^{+}) \to r \in ℝ^{+}$
21		ifcl	$⊢ (r \in ℝ^{+} \land 1 \in ℝ^{+}) \to if (r \leq 1, r, 1) \in ℝ^{+}$
22	20 7 21	sylancl	$⊢ (φ \land r \in ℝ^{+}) \to if (r \leq 1, r, 1) \in ℝ^{+}$
23	2	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to D \in ∞Met (X)$
24	7 11	mp1i	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to 1 \in ℝ^{*}$
25	13	a1i	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to 0 < 1$
26		simpr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to x \in X$
27	22	adantr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to if (r \leq 1, r, 1) \in ℝ^{+}$
28		rpxr	$⊢ if (r \leq 1, r, 1) \in ℝ^{+} \to if (r \leq 1, r, 1) \in ℝ^{*}$
29	27 28	syl	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to if (r \leq 1, r, 1) \in ℝ^{*}$
30		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
31	30	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to r \in ℝ$
32		1re	$⊢ 1 \in ℝ$
33		min2	$⊢ (r \in ℝ \land 1 \in ℝ) \to if (r \leq 1, r, 1) \leq 1$
34	31 32 33	sylancl	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to if (r \leq 1, r, 1) \leq 1$
35	8	stdbdbl	$⊢ ((D \in ∞Met (X) \land 1 \in ℝ^{} \land 0 < 1) \land (x \in X \land if (r \leq 1, r, 1) \in ℝ^{} \land if (r \leq 1, r, 1) \leq 1)) \to x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) if (r \leq 1, r, 1) = x ball (D) if (r \leq 1, r, 1)$
36	23 24 25 26 29 34 35	syl33anc	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) if (r \leq 1, r, 1) = x ball (D) if (r \leq 1, r, 1)$
37	10	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) \in Met (X)$
38		metxmet	$⊢ (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) \in Met (X) \to (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) \in ∞Met (X)$
39	37 38	syl	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to (y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) \in ∞Met (X)$
40		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
41	40	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to r \in ℝ^{*}$
42		min1	$⊢ (r \in ℝ \land 1 \in ℝ) \to if (r \leq 1, r, 1) \leq r$
43	31 32 42	sylancl	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to if (r \leq 1, r, 1) \leq r$
44		ssbl	$⊢ (((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1)) \in ∞Met (X) \land x \in X) \land (if (r \leq 1, r, 1) \in ℝ^{} \land r \in ℝ^{}) \land if (r \leq 1, r, 1) \leq r) \to x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) if (r \leq 1, r, 1) \subseteq x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r$
45	39 26 29 41 43 44	syl221anc	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) if (r \leq 1, r, 1) \subseteq x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r$
46	36 45	eqsstrrd	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to x ball (D) if (r \leq 1, r, 1) \subseteq x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r$
47		sstr2	$⊢ x ball (D) if (r \leq 1, r, 1) \subseteq x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \to (x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \subseteq u \to x ball (D) if (r \leq 1, r, 1) \subseteq u)$
48	46 47	syl	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to (x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \subseteq u \to x ball (D) if (r \leq 1, r, 1) \subseteq u)$
49	48	reximdv	$⊢ ((φ \land r \in ℝ^{+}) \land x \in X) \to (\exists u \in U x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \subseteq u \to \exists u \in U x ball (D) if (r \leq 1, r, 1) \subseteq u)$
50	49	ralimdva	$⊢ (φ \land r \in ℝ^{+}) \to (\forall x \in X \exists u \in U x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \subseteq u \to \forall x \in X \exists u \in U x ball (D) if (r \leq 1, r, 1) \subseteq u)$
51		oveq2	$⊢ d = if (r \leq 1, r, 1) \to x ball (D) d = x ball (D) if (r \leq 1, r, 1)$
52	51	sseq1d	$⊢ d = if (r \leq 1, r, 1) \to (x ball (D) d \subseteq u \leftrightarrow x ball (D) if (r \leq 1, r, 1) \subseteq u)$
53	52	rexbidv	$⊢ d = if (r \leq 1, r, 1) \to (\exists u \in U x ball (D) d \subseteq u \leftrightarrow \exists u \in U x ball (D) if (r \leq 1, r, 1) \subseteq u)$
54	53	ralbidv	$⊢ d = if (r \leq 1, r, 1) \to (\forall x \in X \exists u \in U x ball (D) d \subseteq u \leftrightarrow \forall x \in X \exists u \in U x ball (D) if (r \leq 1, r, 1) \subseteq u)$
55	54	rspcev	$⊢ (if (r \leq 1, r, 1) \in ℝ^{+} \land \forall x \in X \exists u \in U x ball (D) if (r \leq 1, r, 1) \subseteq u) \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$
56	22 50 55	syl6an	$⊢ (φ \land r \in ℝ^{+}) \to (\forall x \in X \exists u \in U x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \subseteq u \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u)$
57	56	rexlimdva	$⊢ φ \to (\exists r \in ℝ^{+} \forall x \in X \exists u \in U x ball ((y \in X, z \in X ⟼ if (y D z \leq 1, y D z, 1))) r \subseteq u \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u)$
58	19 57	mpd	$⊢ φ \to \exists d \in ℝ^{+} \forall x \in X \exists u \in U x ball (D) d \subseteq u$

Metamath Proof Explorer

Theorem xlebnum

Proof