Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Bad symbols? Use Mozilla (or GIF version for IE).

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Color key:

Metamath Proof Explorer (1-4957)

Hilbert Space Explorer (4958-5787)

**Statement List for Metamath Proof Explorer -** 4901-5000 - Page 50 of 58
Type	Label	Description
Statement

Theorem	ruclem17 4901	Lemma for ruc 4924. A helper lemma showing our constructed function G maps ℕ to real numbers.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) ⇒ ⊢ G:ℕ–→ℝ

Theorem	ruclem18 4902	Lemma for ruc 4924. The value of our constructed function G when the value of the input function F lies between the previous values of G and H. This assignment to G defines a new interval between G and H (see also ruclem19 4903) that avoids the value of F.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)) → (G ‘(A + 1)) = (((2 · (F ‘(A + 1))) + (H ‘A)) / 3))

Theorem	ruclem19 4903	Lemma for ruc 4924. The value of our constructed function H when the value of the input function F lies between the previous values of G and H. This assignment to H defines a new interval between G and H (see also ruclem18 4902) that avoids the value of F.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)) → (H ‘(A + 1)) = (((F ‘(A + 1)) + (2 · (H ‘A))) / 3))

Theorem	ruclem20 4904	Lemma for ruc 4924. The value of our constructed function G when the value of the input function F does not lie between the previous values of G and H. This assignment to G just shrinks the interval between G and H by some arbitrary amount.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (¬ ((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)) → (G ‘(A + 1)) = (((2 · (G ‘A)) + (H ‘A)) / 3))

Theorem	ruclem21 4905	Lemma for ruc 4924. The value of our constructed function H when the value of the input function F does not lie between the previous values of G and H. This assignment to H just shrinks the interval between G and H by some arbitrary amount.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (¬ ((G ‘A) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘A)) → (H ‘(A + 1)) = (((G ‘A) + (2 · (H ‘A))) / 3))

Theorem	ruclem22 4906	Lemma for ruc 4924. Each value of our constructed function G is a real number.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (G ‘A) ∈ ℝ

Theorem	ruclem23 4907	Lemma for ruc 4924. Each value of our constructed function H is a real number.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (H ‘A) ∈ ℝ

Theorem	ruclem24 4908	Lemma for ruc 4924. A helper lemma for the induction hypothesis in ruclem25 4909.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ ((G ‘A) < (H ‘A) → (G ‘(A + 1)) < (H ‘(A + 1)))

Theorem	ruclem25 4909	Lemma for ruc 4924. At any index A, the value of G is less than the value of H.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (G ‘A) < (H ‘A)

Theorem	ruclem26 4910	Lemma for ruc 4924. Our constructed function G has an ever-increasing set of values.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (G ‘A) < (G ‘(A + 1))

Theorem	ruclem27 4911	Lemma for ruc 4924. Our constructed function H has an ever-decreasing set of values.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ (H ‘(A + 1)) < (H ‘A)

Theorem	ruclem28 4912	Lemma for ruc 4924. A helper lemma for ruclem29 4913.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ ¬ ((G ‘(A + 1)) < (F ‘(A + 1)) ∧ (F ‘(A + 1)) < (H ‘(A + 1)))

Theorem	ruclem29 4913	Lemma for ruc 4924. At any index A, the interval between our constructed functions G and H does not include the corresponding value of input function F. In other words, our constructed functions define, by ruclem26 4910 and ruclem27 4911, an ever-shrinking interval that eventually squeezes out all values of F.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ ⇒ ⊢ ¬ ((G ‘A) < (F ‘A) ∧ (F ‘A) < (H ‘A))

Theorem	ruclem30 4914	Lemma for ruc 4924. A helper lemma for ruclem32 4916.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ & ⊢ B ∈ ℕ ⇒ ⊢ ((G ‘A) < (G ‘(A + B)) → (G ‘A) < (G ‘(A + (B + 1))))

Theorem	ruclem31 4915	Lemma for ruc 4924. A helper lemma for ruclem32 4916.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ & ⊢ B ∈ ℕ ⇒ ⊢ ((H ‘(A + B)) < (H ‘B) → (H ‘((A + 1) + B)) < (H ‘B))

Theorem	ruclem32 4916	Lemma for ruc 4924. All values of function G are less than all values of function H.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ A ∈ ℕ & ⊢ B ∈ ℕ ⇒ ⊢ (G ‘A) < (H ‘B)

Theorem	ruclem33 4917	Lemma for ruc 4924. The set of values of our constructed function G is a non-empty subset of ℝ. This is a helper lemma for theorems involving supremum.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) ⇒ ⊢ (ran G ⊆ ℝ ∧ ¬ ran G = ∅ ∧ ∃w ∈ ℝ ∀v ∈ ran Gv ≤ w)

Theorem	ruclem34 4918	Lemma for ruc 4924. The supremum of the set of values of our constructed function G is a real number.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ S = sup(ran G, ℝ, < ) ⇒ ⊢ S ∈ ℝ

Theorem	ruclem35 4919	Lemma for ruc 4924. The supremum we have constructed lies between all values of the G and H functions. Compare ruclem29 4913, which states the opposite for the input function F.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ S = sup(ran G, ℝ, < ) & ⊢ A ∈ ℕ ⇒ ⊢ ((G ‘A) < S ∧ S < (H ‘A))

Theorem	ruclem36 4920	Lemma for ruc 4924. No value of F is equal to the supremum we have constructed.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ S = sup(ran G, ℝ, < ) & ⊢ A ∈ ℕ ⇒ ⊢ ¬ (F ‘A) = S

Theorem	ruclem37 4921	Lemma for ruc 4924. If F is any function that maps ℕ into ℝ, then F cannot be onto ℝ.
⊢ F:ℕ–→ℝ & ⊢ C = ({⟨1, ⟨((F ‘1) + 1), ((F ‘1) + 2)⟩⟩} ∪ (F ↾ (ℕ ∖ {1}))) & ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (ℝ × ℝ) ∧ y ∈ ℝ) ∧ z = if(((1^st ‘x) < y ∧ y < (2^nd ‘x)), ⟨(((2 · y) + (2^nd ‘x)) / 3), ((y + (2 · (2^nd ‘x))) / 3)⟩, ⟨(((2 · (1^st ‘x)) + (2^nd ‘x)) / 3), (((1^st ‘x) + (2 · (2^nd ‘x))) / 3)⟩))} & ⊢ G = (1^st ∘ (DseqC)) & ⊢ H = (2^nd ∘ (DseqC)) & ⊢ S = sup(ran G, ℝ, < ) ⇒ ⊢ ¬ F:ℕ–onto→ℝ

Theorem	ruclem38 4922	Lemma for ruc 4924. If F is any function that maps ℕ into ℝ, then F cannot be onto ℝ. Using cleqid 1102, this lemma eliminates those hypotheses of ruclem37 4921 that are no longer needed.
⊢ F:ℕ–→ℝ ⇒ ⊢ ¬ F:ℕ–onto→ℝ

Theorem	ruclem39 4923	Lemma for ruc 4924. There is no function that maps ℕ onto ℝ.
⊢ ¬ F:ℕ–onto→ℝ

Theorem	ruc 4924	The set of natural numbers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 4885 through ruclem39 4923 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114.
⊢ ℕ ≺ ℝ

Theorem	nn0ennn 4925	The nonnegative integers are equinumerous to the natural numbers.
⊢ ℕ₀ ≈ ℕ

Theorem	nnenom 4926	The set of natural numbers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers).
⊢ ℕ ≈ ω

Theorem	xpnnen 4927	The cross product of the set of natural numbers with itself is equinumerous to the set of natural numbers. The key idea is to use nn0opth2t 4726 to show that the mapping from natural numbers z and w to ((z + w)↑2) + w is one-to-one.
⊢ (ℕ × ℕ) ≈ ℕ

Theorem	xpomen 4928	The cross product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133 (which proves this with a direct, but longer, proof; ours uses instead the Schroeder-Bernstein Theorem sbth 3359 in xpnnen 4927).
⊢ (ω × ω) ≈ ω

Theorem	znnenlem 4929	Lemma for znnen 4930.
⊢ (((0 ≤ x ∧ ¬ 0 ≤ y) ∧ (x ∈ ℤ ∧ y ∈ ℤ)) → (y = x ↔ (2 · x) = ((-2 · y) + 1)))

Theorem	znnen 4930	The set of integers and the set of natural numbers are equinumerous.
⊢ ℤ ≈ ℕ

Theorem	qnnen 4931	The set of rationals and the set of natural numbers are equinumerous. (We use the Axiom of Choice via fodom 3613 to give us a shorter proof, but this theorem can also be proved without it. See, for example, Exercise 2 of [Enderton] p. 133.)
⊢ ℚ ≈ ℕ

Theorem	resdomq 4932	The set of rationals is strictly less equinumerous than the set of reals (ℝ strictly dominates ℚ).
⊢ ℚ ≺ ℝ

Theorem	infxpidmlem1 4933	Lemma for infxpidm 4945. An infinite idempotent set x is equinumerous to the union of any two sets A and B equinumerous to it.
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ((ω ≼ x ∧ x ≈ (x × x)) → ((x ≈ A ∧ x ≈ B) → x ≈ (A ∪ B)))

Theorem	infxpidmlem2 4934	Lemma for infxpidm 4945. A necessary and sufficient condition for a set B to belong to H.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ B ∈ V ⇒ ⊢ (B ∈ H ↔ (B = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ B:(x × x)–1-1-onto→x)))

Theorem	infxpidmlem3 4935	Lemma for infxpidm 4945. A sufficient condition for a set B to belong to H.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ B ∈ V & ⊢ D ∈ V ⇒ ⊢ (((ω ≼ D ∧ D ⊆ A) ∧ B:(D × D)–1-1-onto→D) → B ∈ H)

Theorem	infxpidmlem4 4936	Lemma for infxpidm 4945. The domain of a member of H is the cross product of its range.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} ⇒ ⊢ (g ∈ H → dom g = (ran g × ran g))

Theorem	infxpidmlem5 4937	Lemma for infxpidm 4945. Two members in the range of a member of a subset of H form an ordered pair belonging to the domain of the union of the subset.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} ⇒ ⊢ ((C ⊆ H ∧ g ∈ C) → ((y ∈ ran g ∧ z ∈ ran g) → ⟨y, z⟩ ∈ dom ∪C))

Theorem	infxpidmlem6 4938	Lemma for infxpidm 4945. A simple but frequently used fact.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ B = ran ∪C ⇒ ⊢ (y ∈ B ↔ ∃g ∈ C y ∈ ran g)

Theorem	infxpidmlem7 4939	Lemma for infxpidm 4945. The union of a collection C of chains in H is a bijection.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ B = ran ∪C ⇒ ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ∪C:(B × B)–1-1-onto→B)

Theorem	infxpidmlem8 4940	Lemma for infxpidm 4945. The union of a collection of chains C in the collection of bijections H belongs to H. This property will be needed to apply Zorn's Lemma in infxpidmlem9 4941.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ B = ran ∪C & ⊢ C ∈ V ⇒ ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ∪C ∈ H)

Theorem	infxpidmlem9 4941	Lemma for infxpidm 4945. By Zorn's Lemma zorn2 3612, the collection H (which we show here to be a set) has a maximal element.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ A ∈ V ⇒ ⊢ ∃g ∈ H ∀h ∈ H ¬ g ⊂ h

Theorem	infxpidmlem10 4942	Lemma for infxpidm 4945. A maximal bijection g in H is non-empty.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ A ∈ V ⇒ ⊢ (∀h ∈ H ¬ g ⊂ h → (ω ≼ A → ¬ g = ∅))

Theorem	infxpidmlem11 4943	Lemma for infxpidm 4945. We show that the union of a bijection g in H with a disjoint bijection u is a member h of H that is larger than (properly extends) g. Thus if the antecedent is true then g cannot be maximal.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ A ∈ V ⇒ ⊢ (((((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) ∧ (x ≈ y ∧ y ⊆ (A ∖ x))) ∧ u:((x × y) ∪ ((y × x) ∪ (y × y)))–1-1-onto→y) → ∃h ∈ H g ⊂ h)

Theorem	infxpidmlem12 4944	Lemma for infxpidm 4945. Letting x be the range of a maximal bijection g in H, infxpidmlem11 4943 lets us show that assuming x ≼ (A ∖ x) leads to the contradiction ∃h ∈ Hg ⊂ h meaning g is not maximal. Thus (A ∖ x) ≺ x. This allows us to show that x is as big as A. Since x is idempotent, and g exists by Zorn's Lemma in infxpidmlem9 4941, A is also idempotent.
⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))} & ⊢ A ∈ V ⇒ ⊢ (ω ≼ A → (A × A) ≈ A)

Theorem	infxpidm 4945	The cross product of an infinite set with itself is idempotent. This theorem provides the basis for infinite cardinal arithmetic. Lemma 6R of [Enderton] p. 162, whose proof we closely follow. The main proof consists of infxpidmlem1 4933 through infxpidmlem12 4944. This proof eliminates the hypothesis of infxpidmlem12 4944.
⊢ A ∈ V ⇒ ⊢ (ω ≼ A → (A × A) ≈ A)

Theorem	infunabs 4946	An infinite set is equinumerous to its union with a smaller one.
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ((ω ≼ A ∧ B ≼ A) → (A ∪ B) ≈ A)

Theorem	infcdaabs 4947	Absorption law for addition to an infinite cardinal.
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ((ω ≼ A ∧ B ≼ A) → (A +_c B) ≈ A)

Theorem	infdif 4948	The cardinality of an infinite set does not change after subtracting a strictly smaller one. Example in [Enderton] p. 164.
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ((ω ≼ A ∧ B ≺ A) → (A ∖ B) ≈ A)

Theorem	infxpabs 4949	Absorption law for multiplication with an infinite cardinal.
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((ω ≼ A ∧ ¬ B = ∅) ∧ B ≼ A) → (A × B) ≈ A)

Theorem	infmap1 4950	An exponentiation law for infinite cardinals. Exercise 34 of [Enderton] p. 165.
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((2_o ≼ A ∧ ω ≼ B) ∧ A ≼ B) → (A ↑_m B) ≈ (2_o ↑_m B))

Theorem	infmap2lem1 4951	Lemma for infmap2 4953. Technical result that is used several times.
⊢ A ∈ V & ⊢ B ∈ V & ⊢ R = {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)} ⇒ ⊢ ((f ⊆ R ∧ f Fn dom R) → (v ∈ {x∣(x ⊆ A ∧ x ≈ B)} → (v ⊆ A ∧ (f ‘v):B–onto→v)))

Theorem	infmap2lem2 4952	Lemma for infmap2 4953. Given the relation R, we use the Axiom of Choice ac7g 3570 to extract a function f that provides the one-to-one mapping for the dominance relation.
⊢ A ∈ V & ⊢ B ∈ V & ⊢ R = {⟨z, w⟩∣((z ⊆ A ∧ z ≈ B) ∧ w:B–onto→z)} ⇒ ⊢ {x∣(x ⊆ A ∧ x ≈ B)} ≼ (A ↑_m B)

Theorem	infmap2 4953	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. We start with infmap2lem2 4952 and also prove the other direction of the dominance relation. We obtain equinumerosity with Schroeder-Bernstein sbth 3359 and finally eliminate the degenerate case B = ∅.
⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ ((ω ≼ A ∧ B ≼ A) → (A ↑_m B) ≈ {x∣(x ⊆ A ∧ x ≈ B)})

Theorem	alephexp1 4954	An exponentiation law for alephs. Lemma 6.1 of [Jech] p. 42.
⊢ (((A ∈ On ∧ B ∈ On) ∧ A ⊆ B) → ((ℵ ‘A) ↑_m (ℵ ‘B)) ≈ (2_o ↑_m (ℵ ‘B)))

Theorem	alephsuc3 4955	An alternate representation of a successor aleph. Compare alephsuc 3672 and alephsuc2 3686. Equality can be obtained by taking the card of the right-hand side then using alephcard 3673 and carden 3638.
⊢ (A ∈ On → (ℵ ‘suc A) ≈ {x ∈ On∣x ≈ (ℵ ‘A)})

Theorem	alephexp2 4956	An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 4954 (which works if the base is less than or equal to the exponent) and infmap2 4953 (which works if the exponent is less than or equal to the base). They can be equated only when the base is equal to the exponent, and this is the result.
⊢ (A ∈ On → (2_o ↑_m (ℵ ‘A)) ≈ {x∣(x ⊆ (ℵ ‘A) ∧ x ≈ (ℵ ‘A))})

Theorem	gch-kn 4957	The equivalence of two versions of the Generalized Continuum Hypothesis. The right-hand side is the standard version in the literature. The left-hand side is a version devised by Kannan Nambiar, which he calls the Axiom of Combinatorial Sets. For the notation and motivation behind this axiom, see his paper, "Derivation of Continuum Hypothesis from Axiom of Combinatorial Sets," available at http://www.rci.rutgers.edu/~kannan/science/derivation_ch.pdf . This theorem provides a negative answer to Open Problem 2 in http://www.rci.rutgers.edu/~kannan/science/open_problem_print.pdf . The key idea in the proof below is to equate both sides of alephexp2 4956 to the successor aleph using enen2 3376.
⊢ (A ∈ On → ((ℵ ‘suc A) ≈ {x∣(x ⊆ (ℵ ‘A) ∧ x ≈ (ℵ ‘A))} ↔ (ℵ ‘suc A) ≈ (2_o ↑_m (ℵ ‘A))))

Syntax	chil 4958	Extend cla