Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem39 Structured version   Visualization version   GIF version

Theorem stoweidlem39 40574
Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that 𝑟 is a finite subset of 𝑊, 𝑥 indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on 𝐵. Here 𝐷 is used to represent A in the paper's Lemma 2 (because 𝐴 is used for the subalgebra), 𝑀 is used to represent m in the paper, 𝐸 is used to represent ε, and vi is used to represent V(ti). 𝑊 is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem39.1 𝜑
stoweidlem39.2 𝑡𝜑
stoweidlem39.3 𝑤𝜑
stoweidlem39.4 𝑈 = (𝑇𝐵)
stoweidlem39.5 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
stoweidlem39.6 𝑊 = {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
stoweidlem39.7 (𝜑𝑟 ∈ (𝒫 𝑊 ∩ Fin))
stoweidlem39.8 (𝜑𝐷 𝑟)
stoweidlem39.9 (𝜑𝐷 ≠ ∅)
stoweidlem39.10 (𝜑𝐸 ∈ ℝ+)
stoweidlem39.11 (𝜑𝐵𝑇)
stoweidlem39.12 (𝜑𝑊 ∈ V)
stoweidlem39.13 (𝜑𝐴 ∈ V)
Assertion
Ref Expression
stoweidlem39 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡)))))
Distinct variable groups:   𝑒,,𝑚,𝑡,𝑤   𝐴,𝑒,,𝑡,𝑤   𝑒,𝐸,,𝑡,𝑤   𝑇,𝑒,,𝑤   𝑈,𝑒,,𝑤   ,𝑖,𝑟,𝑣,𝑥,𝑚,𝑡,𝑤   𝐴,𝑖,𝑥   𝑖,𝐸,𝑥   𝑇,𝑖,𝑥   𝑈,𝑖,𝑥   𝜑,𝑖,𝑚,𝑣   𝑤,𝑌,𝑥   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥,𝑤,𝑡,𝑒,,𝑟)   𝐴(𝑣,𝑚,𝑟)   𝐵(𝑤,𝑣,𝑡,𝑒,,𝑖,𝑚,𝑟)   𝐷(𝑥,𝑤,𝑣,𝑡,𝑒,,𝑖,𝑚,𝑟)   𝑇(𝑣,𝑡,𝑚,𝑟)   𝑈(𝑣,𝑡,𝑚,𝑟)   𝐸(𝑣,𝑚,𝑟)   𝐽(𝑥,𝑤,𝑣,𝑡,𝑒,,𝑖,𝑚,𝑟)   𝑊(𝑥,𝑤,𝑣,𝑡,𝑒,,𝑖,𝑚,𝑟)   𝑌(𝑣,𝑡,𝑒,,𝑖,𝑚,𝑟)

Proof of Theorem stoweidlem39
Dummy variable 𝑏 is distinct from all other variables.
StepHypRef Expression
1 stoweidlem39.8 . . . . . . 7 (𝜑𝐷 𝑟)
2 stoweidlem39.9 . . . . . . 7 (𝜑𝐷 ≠ ∅)
31, 2jca 553 . . . . . 6 (𝜑 → (𝐷 𝑟𝐷 ≠ ∅))
4 ssn0 4009 . . . . . 6 ((𝐷 𝑟𝐷 ≠ ∅) → 𝑟 ≠ ∅)
5 unieq 4476 . . . . . . . 8 (𝑟 = ∅ → 𝑟 = ∅)
6 uni0 4497 . . . . . . . 8 ∅ = ∅
75, 6syl6eq 2701 . . . . . . 7 (𝑟 = ∅ → 𝑟 = ∅)
87necon3i 2855 . . . . . 6 ( 𝑟 ≠ ∅ → 𝑟 ≠ ∅)
93, 4, 83syl 18 . . . . 5 (𝜑𝑟 ≠ ∅)
109neneqd 2828 . . . 4 (𝜑 → ¬ 𝑟 = ∅)
11 stoweidlem39.7 . . . . . 6 (𝜑𝑟 ∈ (𝒫 𝑊 ∩ Fin))
12 elinel2 3833 . . . . . 6 (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ Fin)
1311, 12syl 17 . . . . 5 (𝜑𝑟 ∈ Fin)
14 fz1f1o 14485 . . . . 5 (𝑟 ∈ Fin → (𝑟 = ∅ ∨ ((#‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto𝑟)))
15 pm2.53 387 . . . . 5 ((𝑟 = ∅ ∨ ((#‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto𝑟)) → (¬ 𝑟 = ∅ → ((#‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto𝑟)))
1613, 14, 153syl 18 . . . 4 (𝜑 → (¬ 𝑟 = ∅ → ((#‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto𝑟)))
1710, 16mpd 15 . . 3 (𝜑 → ((#‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto𝑟))
18 oveq2 6698 . . . . . 6 (𝑚 = (#‘𝑟) → (1...𝑚) = (1...(#‘𝑟)))
19 f1oeq2 6166 . . . . . 6 ((1...𝑚) = (1...(#‘𝑟)) → (𝑣:(1...𝑚)–1-1-onto𝑟𝑣:(1...(#‘𝑟))–1-1-onto𝑟))
2018, 19syl 17 . . . . 5 (𝑚 = (#‘𝑟) → (𝑣:(1...𝑚)–1-1-onto𝑟𝑣:(1...(#‘𝑟))–1-1-onto𝑟))
2120exbidv 1890 . . . 4 (𝑚 = (#‘𝑟) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟 ↔ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto𝑟))
2221rspcev 3340 . . 3 (((#‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(#‘𝑟))–1-1-onto𝑟) → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟)
2317, 22syl 17 . 2 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟)
24 f1of 6175 . . . . . . . 8 (𝑣:(1...𝑚)–1-1-onto𝑟𝑣:(1...𝑚)⟶𝑟)
2524adantl 481 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑣:(1...𝑚)⟶𝑟)
26 simpll 805 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝜑)
27 elinel1 3832 . . . . . . . . 9 (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ 𝒫 𝑊)
2827elpwid 4203 . . . . . . . 8 (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟𝑊)
2926, 11, 283syl 18 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑟𝑊)
3025, 29fssd 6095 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑣:(1...𝑚)⟶𝑊)
311ad2antrr 762 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐷 𝑟)
32 dff1o2 6180 . . . . . . . . . 10 (𝑣:(1...𝑚)–1-1-onto𝑟 ↔ (𝑣 Fn (1...𝑚) ∧ Fun 𝑣 ∧ ran 𝑣 = 𝑟))
3332simp3bi 1098 . . . . . . . . 9 (𝑣:(1...𝑚)–1-1-onto𝑟 → ran 𝑣 = 𝑟)
3433unieqd 4478 . . . . . . . 8 (𝑣:(1...𝑚)–1-1-onto𝑟 ran 𝑣 = 𝑟)
3534adantl 481 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → ran 𝑣 = 𝑟)
3631, 35sseqtr4d 3675 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐷 ran 𝑣)
37 stoweidlem39.1 . . . . . . . . 9 𝜑
38 nfv 1883 . . . . . . . . 9 𝑚 ∈ ℕ
3937, 38nfan 1868 . . . . . . . 8 (𝜑𝑚 ∈ ℕ)
40 nfv 1883 . . . . . . . 8 𝑣:(1...𝑚)–1-1-onto𝑟
4139, 40nfan 1868 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟)
42 stoweidlem39.2 . . . . . . . . 9 𝑡𝜑
43 nfv 1883 . . . . . . . . 9 𝑡 𝑚 ∈ ℕ
4442, 43nfan 1868 . . . . . . . 8 𝑡(𝜑𝑚 ∈ ℕ)
45 nfv 1883 . . . . . . . 8 𝑡 𝑣:(1...𝑚)–1-1-onto𝑟
4644, 45nfan 1868 . . . . . . 7 𝑡((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟)
47 stoweidlem39.3 . . . . . . . . 9 𝑤𝜑
48 nfv 1883 . . . . . . . . 9 𝑤 𝑚 ∈ ℕ
4947, 48nfan 1868 . . . . . . . 8 𝑤(𝜑𝑚 ∈ ℕ)
50 nfv 1883 . . . . . . . 8 𝑤 𝑣:(1...𝑚)–1-1-onto𝑟
5149, 50nfan 1868 . . . . . . 7 𝑤((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟)
52 stoweidlem39.5 . . . . . . 7 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
53 stoweidlem39.6 . . . . . . 7 𝑊 = {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
54 eqid 2651 . . . . . . 7 (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))}) = (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))})
55 simplr 807 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑚 ∈ ℕ)
56 simpr 476 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑣:(1...𝑚)–1-1-onto𝑟)
57 stoweidlem39.10 . . . . . . . 8 (𝜑𝐸 ∈ ℝ+)
5857ad2antrr 762 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐸 ∈ ℝ+)
59 stoweidlem39.11 . . . . . . . . . . . 12 (𝜑𝐵𝑇)
6059sselda 3636 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → 𝑏𝑇)
61 notnot 136 . . . . . . . . . . . . . . 15 (𝑏𝐵 → ¬ ¬ 𝑏𝐵)
6261intnand 982 . . . . . . . . . . . . . 14 (𝑏𝐵 → ¬ (𝑏𝑇 ∧ ¬ 𝑏𝐵))
6362adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ¬ (𝑏𝑇 ∧ ¬ 𝑏𝐵))
64 eldif 3617 . . . . . . . . . . . . 13 (𝑏 ∈ (𝑇𝐵) ↔ (𝑏𝑇 ∧ ¬ 𝑏𝐵))
6563, 64sylnibr 318 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ¬ 𝑏 ∈ (𝑇𝐵))
66 stoweidlem39.4 . . . . . . . . . . . . 13 𝑈 = (𝑇𝐵)
6766eleq2i 2722 . . . . . . . . . . . 12 (𝑏𝑈𝑏 ∈ (𝑇𝐵))
6865, 67sylnibr 318 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → ¬ 𝑏𝑈)
6960, 68eldifd 3618 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝑏 ∈ (𝑇𝑈))
7069ralrimiva 2995 . . . . . . . . 9 (𝜑 → ∀𝑏𝐵 𝑏 ∈ (𝑇𝑈))
71 dfss3 3625 . . . . . . . . 9 (𝐵 ⊆ (𝑇𝑈) ↔ ∀𝑏𝐵 𝑏 ∈ (𝑇𝑈))
7270, 71sylibr 224 . . . . . . . 8 (𝜑𝐵 ⊆ (𝑇𝑈))
7372ad2antrr 762 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐵 ⊆ (𝑇𝑈))
74 stoweidlem39.12 . . . . . . . 8 (𝜑𝑊 ∈ V)
7574ad2antrr 762 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑊 ∈ V)
76 stoweidlem39.13 . . . . . . . 8 (𝜑𝐴 ∈ V)
7776ad2antrr 762 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐴 ∈ V)
7813ad2antrr 762 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑟 ∈ Fin)
79 mptfi 8306 . . . . . . . 8 (𝑟 ∈ Fin → (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))}) ∈ Fin)
80 rnfi 8290 . . . . . . . 8 ((𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))}) ∈ Fin → ran (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))}) ∈ Fin)
8178, 79, 803syl 18 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → ran (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))}) ∈ Fin)
8241, 46, 51, 52, 53, 54, 29, 55, 56, 58, 73, 75, 77, 81stoweidlem31 40566 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡))))
8330, 36, 823jca 1261 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → (𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡)))))
8483ex 449 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑣:(1...𝑚)–1-1-onto𝑟 → (𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡))))))
8584eximdv 1886 . . 3 ((𝜑𝑚 ∈ ℕ) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟 → ∃𝑣(𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡))))))
8685reximdva 3046 . 2 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡))))))
8723, 86mpd 15 1 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣(𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wex 1744  wnf 1748  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191   cuni 4468   class class class wbr 4685  cmpt 4762  ccnv 5142  ran crn 5144  Fun wfun 5920   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  Fincfn 7997  0cc0 9974  1c1 9975   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  +crp 11870  ...cfz 12364  #chash 13157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-hash 13158
This theorem is referenced by:  stoweidlem57  40592
  Copyright terms: Public domain W3C validator