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

Theorem stoweidlem39 40755
 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 555 . . . . . 6 (𝜑 → (𝐷 𝑟𝐷 ≠ ∅))
4 ssn0 4115 . . . . . 6 ((𝐷 𝑟𝐷 ≠ ∅) → 𝑟 ≠ ∅)
5 unieq 4592 . . . . . . . 8 (𝑟 = ∅ → 𝑟 = ∅)
6 uni0 4613 . . . . . . . 8 ∅ = ∅
75, 6syl6eq 2806 . . . . . . 7 (𝑟 = ∅ → 𝑟 = ∅)
87necon3i 2960 . . . . . 6 ( 𝑟 ≠ ∅ → 𝑟 ≠ ∅)
93, 4, 83syl 18 . . . . 5 (𝜑𝑟 ≠ ∅)
109neneqd 2933 . . . 4 (𝜑 → ¬ 𝑟 = ∅)
11 stoweidlem39.7 . . . . . 6 (𝜑𝑟 ∈ (𝒫 𝑊 ∩ Fin))
12 elinel2 3939 . . . . . 6 (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ Fin)
1311, 12syl 17 . . . . 5 (𝜑𝑟 ∈ Fin)
14 fz1f1o 14636 . . . . 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 6817 . . . . . 6 (𝑚 = (♯‘𝑟) → (1...𝑚) = (1...(♯‘𝑟)))
19 f1oeq2 6285 . . . . . 6 ((1...𝑚) = (1...(♯‘𝑟)) → (𝑣:(1...𝑚)–1-1-onto𝑟𝑣:(1...(♯‘𝑟))–1-1-onto𝑟))
2018, 19syl 17 . . . . 5 (𝑚 = (♯‘𝑟) → (𝑣:(1...𝑚)–1-1-onto𝑟𝑣:(1...(♯‘𝑟))–1-1-onto𝑟))
2120exbidv 1995 . . . 4 (𝑚 = (♯‘𝑟) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟 ↔ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto𝑟))
2221rspcev 3445 . . 3 (((♯‘𝑟) ∈ ℕ ∧ ∃𝑣 𝑣:(1...(♯‘𝑟))–1-1-onto𝑟) → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟)
2317, 22syl 17 . 2 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟)
24 f1of 6294 . . . . . . . 8 (𝑣:(1...𝑚)–1-1-onto𝑟𝑣:(1...𝑚)⟶𝑟)
2524adantl 473 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑣:(1...𝑚)⟶𝑟)
26 simpll 807 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝜑)
27 elinel1 3938 . . . . . . . . 9 (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟 ∈ 𝒫 𝑊)
2827elpwid 4310 . . . . . . . 8 (𝑟 ∈ (𝒫 𝑊 ∩ Fin) → 𝑟𝑊)
2926, 11, 283syl 18 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑟𝑊)
3025, 29fssd 6214 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑣:(1...𝑚)⟶𝑊)
311ad2antrr 764 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐷 𝑟)
32 dff1o2 6299 . . . . . . . . . 10 (𝑣:(1...𝑚)–1-1-onto𝑟 ↔ (𝑣 Fn (1...𝑚) ∧ Fun 𝑣 ∧ ran 𝑣 = 𝑟))
3332simp3bi 1142 . . . . . . . . 9 (𝑣:(1...𝑚)–1-1-onto𝑟 → ran 𝑣 = 𝑟)
3433unieqd 4594 . . . . . . . 8 (𝑣:(1...𝑚)–1-1-onto𝑟 ran 𝑣 = 𝑟)
3534adantl 473 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → ran 𝑣 = 𝑟)
3631, 35sseqtr4d 3779 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐷 ran 𝑣)
37 stoweidlem39.1 . . . . . . . . 9 𝜑
38 nfv 1988 . . . . . . . . 9 𝑚 ∈ ℕ
3937, 38nfan 1973 . . . . . . . 8 (𝜑𝑚 ∈ ℕ)
40 nfv 1988 . . . . . . . 8 𝑣:(1...𝑚)–1-1-onto𝑟
4139, 40nfan 1973 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟)
42 stoweidlem39.2 . . . . . . . . 9 𝑡𝜑
43 nfv 1988 . . . . . . . . 9 𝑡 𝑚 ∈ ℕ
4442, 43nfan 1973 . . . . . . . 8 𝑡(𝜑𝑚 ∈ ℕ)
45 nfv 1988 . . . . . . . 8 𝑡 𝑣:(1...𝑚)–1-1-onto𝑟
4644, 45nfan 1973 . . . . . . 7 𝑡((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟)
47 stoweidlem39.3 . . . . . . . . 9 𝑤𝜑
48 nfv 1988 . . . . . . . . 9 𝑤 𝑚 ∈ ℕ
4947, 48nfan 1973 . . . . . . . 8 𝑤(𝜑𝑚 ∈ ℕ)
50 nfv 1988 . . . . . . . 8 𝑤 𝑣:(1...𝑚)–1-1-onto𝑟
5149, 50nfan 1973 . . . . . . 7 𝑤((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟)
52 stoweidlem39.5 . . . . . . 7 𝑌 = {𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)}
53 stoweidlem39.6 . . . . . . 7 𝑊 = {𝑤𝐽 ∣ ∀𝑒 ∈ ℝ+𝐴 (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − 𝑒) < (𝑡))}
54 eqid 2756 . . . . . . 7 (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))}) = (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))})
55 simplr 809 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑚 ∈ ℕ)
56 simpr 479 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑣:(1...𝑚)–1-1-onto𝑟)
57 stoweidlem39.10 . . . . . . . 8 (𝜑𝐸 ∈ ℝ+)
5857ad2antrr 764 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐸 ∈ ℝ+)
59 stoweidlem39.11 . . . . . . . . . . . 12 (𝜑𝐵𝑇)
6059sselda 3740 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → 𝑏𝑇)
61 notnot 136 . . . . . . . . . . . . . . 15 (𝑏𝐵 → ¬ ¬ 𝑏𝐵)
6261intnand 1000 . . . . . . . . . . . . . 14 (𝑏𝐵 → ¬ (𝑏𝑇 ∧ ¬ 𝑏𝐵))
6362adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑏𝐵) → ¬ (𝑏𝑇 ∧ ¬ 𝑏𝐵))
64 eldif 3721 . . . . . . . . . . . . 13 (𝑏 ∈ (𝑇𝐵) ↔ (𝑏𝑇 ∧ ¬ 𝑏𝐵))
6563, 64sylnibr 318 . . . . . . . . . . . 12 ((𝜑𝑏𝐵) → ¬ 𝑏 ∈ (𝑇𝐵))
66 stoweidlem39.4 . . . . . . . . . . . . 13 𝑈 = (𝑇𝐵)
6766eleq2i 2827 . . . . . . . . . . . 12 (𝑏𝑈𝑏 ∈ (𝑇𝐵))
6865, 67sylnibr 318 . . . . . . . . . . 11 ((𝜑𝑏𝐵) → ¬ 𝑏𝑈)
6960, 68eldifd 3722 . . . . . . . . . 10 ((𝜑𝑏𝐵) → 𝑏 ∈ (𝑇𝑈))
7069ralrimiva 3100 . . . . . . . . 9 (𝜑 → ∀𝑏𝐵 𝑏 ∈ (𝑇𝑈))
71 dfss3 3729 . . . . . . . . 9 (𝐵 ⊆ (𝑇𝑈) ↔ ∀𝑏𝐵 𝑏 ∈ (𝑇𝑈))
7270, 71sylibr 224 . . . . . . . 8 (𝜑𝐵 ⊆ (𝑇𝑈))
7372ad2antrr 764 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐵 ⊆ (𝑇𝑈))
74 stoweidlem39.12 . . . . . . . 8 (𝜑𝑊 ∈ V)
7574ad2antrr 764 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑊 ∈ V)
76 stoweidlem39.13 . . . . . . . 8 (𝜑𝐴 ∈ V)
7776ad2antrr 764 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝐴 ∈ V)
7813ad2antrr 764 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → 𝑟 ∈ Fin)
79 mptfi 8426 . . . . . . . 8 (𝑟 ∈ Fin → (𝑤𝑟 ↦ {𝐴 ∣ (∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1) ∧ ∀𝑡𝑤 (𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡 ∈ (𝑇𝑈)(1 − (𝐸 / 𝑚)) < (𝑡))}) ∈ Fin)
80 rnfi 8410 . . . . . . . 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 40747 . . . . . 6 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡))))
8330, 36, 823jca 1123 . . . . 5 (((𝜑𝑚 ∈ ℕ) ∧ 𝑣:(1...𝑚)–1-1-onto𝑟) → (𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡)))))
8483ex 449 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑣:(1...𝑚)–1-1-onto𝑟 → (𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡))))))
8584eximdv 1991 . . 3 ((𝜑𝑚 ∈ ℕ) → (∃𝑣 𝑣:(1...𝑚)–1-1-onto𝑟 → ∃𝑣(𝑣:(1...𝑚)⟶𝑊𝐷 ran 𝑣 ∧ ∃𝑥(𝑥:(1...𝑚)⟶𝑌 ∧ ∀𝑖 ∈ (1...𝑚)(∀𝑡 ∈ (𝑣𝑖)((𝑥𝑖)‘𝑡) < (𝐸 / 𝑚) ∧ ∀𝑡𝐵 (1 − (𝐸 / 𝑚)) < ((𝑥𝑖)‘𝑡))))))
8685reximdva 3151 . 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 1072   = wceq 1628  ∃wex 1849  Ⅎwnf 1853   ∈ wcel 2135   ≠ wne 2928  ∀wral 3046  ∃wrex 3047  {crab 3050  Vcvv 3336   ∖ cdif 3708   ∩ cin 3710   ⊆ wss 3711  ∅c0 4054  𝒫 cpw 4298  ∪ cuni 4584   class class class wbr 4800   ↦ cmpt 4877  ◡ccnv 5261  ran crn 5263  Fun wfun 6039   Fn wfn 6040  ⟶wf 6041  –1-1-onto→wf1o 6044  ‘cfv 6045  (class class class)co 6809  Fincfn 8117  0cc0 10124  1c1 10125   < clt 10262   ≤ cle 10263   − cmin 10454   / cdiv 10872  ℕcn 11208  ℝ+crp 12021  ...cfz 12515  ♯chash 13307 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-card 8951  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-n0 11481  df-z 11566  df-uz 11876  df-rp 12022  df-fz 12516  df-hash 13308 This theorem is referenced by:  stoweidlem57  40773
 Copyright terms: Public domain W3C validator