supcvg

Description: Extract a sequence f in X such that the image of the points in the bounded set A converges to the supremum S of the set. Similar to Equation 4 of Kreyszig p. 144. The proof uses countable choice ax-cc . (Contributed by Mario Carneiro, 15-Feb-2013) (Proof shortened by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	supcvg.1	$⊢ X \in V$
	supcvg.2	$⊢ S = sup (A ℝ <)$
	supcvg.3	$⊢ R = (n \in ℕ ⟼ S - (\frac{1}{n}))$
	supcvg.4	$⊢ φ \to X \neq \emptyset$
	supcvg.5	$⊢ φ \to F : X \underset{onto}{⟶} A$
	supcvg.6	$⊢ φ \to A \subseteq ℝ$
	supcvg.7	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
Assertion	supcvg	$⊢ φ \to \exists f (f : ℕ ⟶ X \land (F \circ f) ⇝ S)$

Proof

Step	Hyp	Ref	Expression
1		supcvg.1	$⊢ X \in V$
2		supcvg.2	$⊢ S = sup (A ℝ <)$
3		supcvg.3	$⊢ R = (n \in ℕ ⟼ S - (\frac{1}{n}))$
4		supcvg.4	$⊢ φ \to X \neq \emptyset$
5		supcvg.5	$⊢ φ \to F : X \underset{onto}{⟶} A$
6		supcvg.6	$⊢ φ \to A \subseteq ℝ$
7		supcvg.7	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
8		oveq2	$⊢ n = k \to \frac{1}{n} = \frac{1}{k}$
9	8	oveq2d	$⊢ n = k \to S - (\frac{1}{n}) = S - (\frac{1}{k})$
10		ovex	$⊢ S - (\frac{1}{k}) \in V$
11	9 3 10	fvmpt	$⊢ k \in ℕ \to R (k) = S - (\frac{1}{k})$
12	11	adantl	$⊢ (φ \land k \in ℕ) \to R (k) = S - (\frac{1}{k})$
13		fof	$⊢ F : X \underset{onto}{⟶} A \to F : X ⟶ A$
14	5 13	syl	$⊢ φ \to F : X ⟶ A$
15		feq3	$⊢ A = \emptyset \to (F : X ⟶ A \leftrightarrow F : X ⟶ \emptyset)$
16	14 15	syl5ibcom	$⊢ φ \to (A = \emptyset \to F : X ⟶ \emptyset)$
17		f00	$⊢ F : X ⟶ \emptyset \leftrightarrow (F = \emptyset \land X = \emptyset)$
18	17	simprbi	$⊢ F : X ⟶ \emptyset \to X = \emptyset$
19	16 18	syl6	$⊢ φ \to (A = \emptyset \to X = \emptyset)$
20	19	necon3d	$⊢ φ \to (X \neq \emptyset \to A \neq \emptyset)$
21	4 20	mpd	$⊢ φ \to A \neq \emptyset$
22	6 21 7	suprcld	$⊢ φ \to sup (A ℝ <) \in ℝ$
23	2 22	eqeltrid	$⊢ φ \to S \in ℝ$
24		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
25	24	rpreccld	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ^{+}$
26		ltsubrp	$⊢ (S \in ℝ \land \frac{1}{k} \in ℝ^{+}) \to S - (\frac{1}{k}) < S$
27	23 25 26	syl2an	$⊢ (φ \land k \in ℕ) \to S - (\frac{1}{k}) < S$
28	12 27	eqbrtrd	$⊢ (φ \land k \in ℕ) \to R (k) < S$
29	28 2	breqtrdi	$⊢ (φ \land k \in ℕ) \to R (k) < sup (A ℝ <)$
30	6 21 7	3jca	$⊢ φ \to (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
31		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
32		resubcl	$⊢ (S \in ℝ \land \frac{1}{n} \in ℝ) \to S - (\frac{1}{n}) \in ℝ$
33	23 31 32	syl2an	$⊢ (φ \land n \in ℕ) \to S - (\frac{1}{n}) \in ℝ$
34	33 3	fmptd	$⊢ φ \to R : ℕ ⟶ ℝ$
35	34	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to R (k) \in ℝ$
36		suprlub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land R (k) \in ℝ) \to (R (k) < sup (A ℝ <) \leftrightarrow \exists z \in A R (k) < z)$
37	30 35 36	syl2an2r	$⊢ (φ \land k \in ℕ) \to (R (k) < sup (A ℝ <) \leftrightarrow \exists z \in A R (k) < z)$
38	29 37	mpbid	$⊢ (φ \land k \in ℕ) \to \exists z \in A R (k) < z$
39	6	adantr	$⊢ (φ \land k \in ℕ) \to A \subseteq ℝ$
40	39	sselda	$⊢ ((φ \land k \in ℕ) \land z \in A) \to z \in ℝ$
41		ltle	$⊢ (R (k) \in ℝ \land z \in ℝ) \to (R (k) < z \to R (k) \leq z)$
42	35 40 41	syl2an2r	$⊢ ((φ \land k \in ℕ) \land z \in A) \to (R (k) < z \to R (k) \leq z)$
43	42	reximdva	$⊢ (φ \land k \in ℕ) \to (\exists z \in A R (k) < z \to \exists z \in A R (k) \leq z)$
44	38 43	mpd	$⊢ (φ \land k \in ℕ) \to \exists z \in A R (k) \leq z$
45		forn	$⊢ F : X \underset{onto}{⟶} A \to ran F = A$
46	5 45	syl	$⊢ φ \to ran F = A$
47	46	rexeqdv	$⊢ φ \to (\exists z \in ran F R (k) \leq z \leftrightarrow \exists z \in A R (k) \leq z)$
48		ffn	$⊢ F : X ⟶ A \to F Fn X$
49		breq2	$⊢ z = F (x) \to (R (k) \leq z \leftrightarrow R (k) \leq F (x))$
50	49	rexrn	$⊢ F Fn X \to (\exists z \in ran F R (k) \leq z \leftrightarrow \exists x \in X R (k) \leq F (x))$
51	14 48 50	3syl	$⊢ φ \to (\exists z \in ran F R (k) \leq z \leftrightarrow \exists x \in X R (k) \leq F (x))$
52	47 51	bitr3d	$⊢ φ \to (\exists z \in A R (k) \leq z \leftrightarrow \exists x \in X R (k) \leq F (x))$
53	52	adantr	$⊢ (φ \land k \in ℕ) \to (\exists z \in A R (k) \leq z \leftrightarrow \exists x \in X R (k) \leq F (x))$
54	44 53	mpbid	$⊢ (φ \land k \in ℕ) \to \exists x \in X R (k) \leq F (x)$
55	54	ralrimiva	$⊢ φ \to \forall k \in ℕ \exists x \in X R (k) \leq F (x)$
56		nnenom	$⊢ ℕ \approx ω$
57		fveq2	$⊢ x = f (k) \to F (x) = F (f (k))$
58	57	breq2d	$⊢ x = f (k) \to (R (k) \leq F (x) \leftrightarrow R (k) \leq F (f (k)))$
59	1 56 58	axcc4	$⊢ \forall k \in ℕ \exists x \in X R (k) \leq F (x) \to \exists f (f : ℕ ⟶ X \land \forall k \in ℕ R (k) \leq F (f (k)))$
60	55 59	syl	$⊢ φ \to \exists f (f : ℕ ⟶ X \land \forall k \in ℕ R (k) \leq F (f (k)))$
61		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
62		1zzd	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to 1 \in ℤ$
63		1zzd	$⊢ φ \to 1 \in ℤ$
64	23	recnd	$⊢ φ \to S \in ℂ$
65		1z	$⊢ 1 \in ℤ$
66	61	eqimss2i	$⊢ ℤ_{\geq 1} \subseteq ℕ$
67		nnex	$⊢ ℕ \in V$
68	66 67	climconst2	$⊢ (S \in ℂ \land 1 \in ℤ) \to (ℕ \times \{S\}) ⇝ S$
69	64 65 68	sylancl	$⊢ φ \to (ℕ \times \{S\}) ⇝ S$
70	67	mptex	$⊢ (n \in ℕ ⟼ S - (\frac{1}{n})) \in V$
71	3 70	eqeltri	$⊢ R \in V$
72	71	a1i	$⊢ φ \to R \in V$
73		ax-1cn	$⊢ 1 \in ℂ$
74		divcnv	$⊢ 1 \in ℂ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
75	73 74	mp1i	$⊢ φ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
76		fvconst2g	$⊢ (S \in ℝ \land k \in ℕ) \to (ℕ \times \{S\}) (k) = S$
77	23 76	sylan	$⊢ (φ \land k \in ℕ) \to (ℕ \times \{S\}) (k) = S$
78	64	adantr	$⊢ (φ \land k \in ℕ) \to S \in ℂ$
79	77 78	eqeltrd	$⊢ (φ \land k \in ℕ) \to (ℕ \times \{S\}) (k) \in ℂ$
80		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{n}) = (n \in ℕ ⟼ \frac{1}{n})$
81		ovex	$⊢ \frac{1}{k} \in V$
82	8 80 81	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{1}{n}) (k) = \frac{1}{k}$
83	82	adantl	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (k) = \frac{1}{k}$
84		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
85	84	recnd	$⊢ k \in ℕ \to \frac{1}{k} \in ℂ$
86	85	adantl	$⊢ (φ \land k \in ℕ) \to \frac{1}{k} \in ℂ$
87	83 86	eqeltrd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (k) \in ℂ$
88	77 83	oveq12d	$⊢ (φ \land k \in ℕ) \to (ℕ \times \{S\}) (k) - (n \in ℕ ⟼ \frac{1}{n}) (k) = S - (\frac{1}{k})$
89	12 88	eqtr4d	$⊢ (φ \land k \in ℕ) \to R (k) = (ℕ \times \{S\}) (k) - (n \in ℕ ⟼ \frac{1}{n}) (k)$
90	61 63 69 72 75 79 87 89	climsub	$⊢ φ \to R ⇝ (S - 0)$
91	64	subid1d	$⊢ φ \to S - 0 = S$
92	90 91	breqtrd	$⊢ φ \to R ⇝ S$
93	92	ad2antrr	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to R ⇝ S$
94	14	ad2antrr	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to F : X ⟶ A$
95		fex	$⊢ (F : X ⟶ A \land X \in V) \to F \in V$
96	94 1 95	sylancl	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to F \in V$
97		vex	$⊢ f \in V$
98		coexg	$⊢ (F \in V \land f \in V) \to F \circ f \in V$
99	96 97 98	sylancl	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to F \circ f \in V$
100	34	ad2antrr	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to R : ℕ ⟶ ℝ$
101	100	ffvelcdmda	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to R (m) \in ℝ$
102	14 6	fssd	$⊢ φ \to F : X ⟶ ℝ$
103		fco	$⊢ (F : X ⟶ ℝ \land f : ℕ ⟶ X) \to (F \circ f) : ℕ ⟶ ℝ$
104	102 103	sylan	$⊢ (φ \land f : ℕ ⟶ X) \to (F \circ f) : ℕ ⟶ ℝ$
105	104	adantr	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to (F \circ f) : ℕ ⟶ ℝ$
106	105	ffvelcdmda	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to (F \circ f) (m) \in ℝ$
107		fveq2	$⊢ k = m \to R (k) = R (m)$
108		2fveq3	$⊢ k = m \to F (f (k)) = F (f (m))$
109	107 108	breq12d	$⊢ k = m \to (R (k) \leq F (f (k)) \leftrightarrow R (m) \leq F (f (m)))$
110	109	rspccva	$⊢ (\forall k \in ℕ R (k) \leq F (f (k)) \land m \in ℕ) \to R (m) \leq F (f (m))$
111	110	adantll	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to R (m) \leq F (f (m))$
112		simplr	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to f : ℕ ⟶ X$
113		fvco3	$⊢ (f : ℕ ⟶ X \land m \in ℕ) \to (F \circ f) (m) = F (f (m))$
114	112 113	sylan	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to (F \circ f) (m) = F (f (m))$
115	111 114	breqtrrd	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to R (m) \leq (F \circ f) (m)$
116	30	ad3antrrr	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x)$
117	112	ffvelcdmda	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to f (m) \in X$
118	94	ffvelcdmda	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land f (m) \in X) \to F (f (m)) \in A$
119	117 118	syldan	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to F (f (m)) \in A$
120		suprub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land F (f (m)) \in A) \to F (f (m)) \leq sup (A ℝ <)$
121	116 119 120	syl2anc	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to F (f (m)) \leq sup (A ℝ <)$
122	121 2	breqtrrdi	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to F (f (m)) \leq S$
123	114 122	eqbrtrd	$⊢ (((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \land m \in ℕ) \to (F \circ f) (m) \leq S$
124	61 62 93 99 101 106 115 123	climsqz	$⊢ ((φ \land f : ℕ ⟶ X) \land \forall k \in ℕ R (k) \leq F (f (k))) \to (F \circ f) ⇝ S$
125	124	ex	$⊢ (φ \land f : ℕ ⟶ X) \to (\forall k \in ℕ R (k) \leq F (f (k)) \to (F \circ f) ⇝ S)$
126	125	imdistanda	$⊢ φ \to ((f : ℕ ⟶ X \land \forall k \in ℕ R (k) \leq F (f (k))) \to (f : ℕ ⟶ X \land (F \circ f) ⇝ S))$
127	126	eximdv	$⊢ φ \to (\exists f (f : ℕ ⟶ X \land \forall k \in ℕ R (k) \leq F (f (k))) \to \exists f (f : ℕ ⟶ X \land (F \circ f) ⇝ S))$
128	60 127	mpd	$⊢ φ \to \exists f (f : ℕ ⟶ X \land (F \circ f) ⇝ S)$

Metamath Proof Explorer

Theorem supcvg

Proof