HomeTheorem List (p. 371 of 512)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 371 of 512) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-31526) |
Hilbert Space Explorer
(31527-33049) |
Users' Mathboxes
(33050-51159) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | linedegen 37001 | When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝐴Line𝐴) = ∅ | ||
| Theorem | fvline 37002* | Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∣ 𝑥 Colinear ⟨𝐴, 𝐵⟩}) | ||
| Theorem | liness 37003 | A line is a subset of the space its two points lie in. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) ⊆ (𝔼‘𝑁)) | ||
| Theorem | fvline2 37004* | Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵)) → (𝐴Line𝐵) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑥 Colinear ⟨𝐴, 𝐵⟩}) | ||
| Theorem | lineunray 37005 | A line is composed of a point and the two rays emerging from it. Theorem 6.15 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 26-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 Btwn ⟨𝑄, 𝑅⟩ → (𝑃Line𝑄) = (((𝑃Ray𝑄) ∪ {𝑃}) ∪ (𝑃Ray𝑅)))) | ||
| Theorem | lineelsb2 37006 | If 𝑆 lies on 𝑃𝑄, then 𝑃𝑄 = 𝑃𝑆. Theorem 6.16 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄) ∧ (𝑆 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑆)) → (𝑆 ∈ (𝑃Line𝑄) → (𝑃Line𝑄) = (𝑃Line𝑆))) | ||
| Theorem | linerflx1 37007 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑃 ∈ (𝑃Line𝑄)) | ||
| Theorem | linecom 37008 | Commutativity law for lines. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → (𝑃Line𝑄) = (𝑄Line𝑃)) | ||
| Theorem | linerflx2 37009 | Reflexivity law for line membership. Part of theorem 6.17 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → 𝑄 ∈ (𝑃Line𝑄)) | ||
| Theorem | ellines 37010* | Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝐴 ∈ LinesEE ↔ ∃𝑛 ∈ ℕ ∃𝑝 ∈ (𝔼‘𝑛)∃𝑞 ∈ (𝔼‘𝑛)(𝑝 ≠ 𝑞 ∧ 𝐴 = (𝑝Line𝑞))) | ||
| Theorem | linethru 37011 | If 𝐴 is a line containing two distinct points 𝑃 and 𝑄, then 𝐴 is the line through 𝑃 and 𝑄. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ LinesEE ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → 𝐴 = (𝑃Line𝑄)) | ||
| Theorem | hilbert1.1 37012* | There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
| Theorem | hilbert1.2 37013* | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.) |
| ⊢ (𝑃 ≠ 𝑄 → ∃*𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
| Theorem | linethrueu 37014* | There is a unique line going through any two distinct points. Theorem 6.19 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝑄)) → ∃!𝑥 ∈ LinesEE (𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥)) | ||
| Theorem | lineintmo 37015* | Two distinct lines intersect in at most one point. Theorem 6.21 of [Schwabhauser] p. 46. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ ((𝐴 ∈ LinesEE ∧ 𝐵 ∈ LinesEE ∧ 𝐴 ≠ 𝐵) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
| Syntax | cfwddif 37016 | Declare the syntax for the forward difference operator. |
| class △ | ||
| Definition | df-fwddif 37017* | Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.) |
| ⊢ △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥)))) | ||
| Syntax | cfwddifn 37018 | Declare the syntax for the nth forward difference operator. |
| class △n | ||
| Definition | df-fwddifn 37019* | Define the nth forward difference operator. This works out to be the forward difference operator iterated 𝑛 times. (Contributed by Scott Fenton, 28-May-2020.) |
| ⊢ △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))) | ||
| Theorem | fwddifval 37020 | Calculate the value of the forward difference operator at a point. (Contributed by Scott Fenton, 18-May-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → (𝑋 + 1) ∈ 𝐴) ⇒ ⊢ (𝜑 → (( △ ‘𝐹)‘𝑋) = ((𝐹‘(𝑋 + 1)) − (𝐹‘𝑋))) | ||
| Theorem | fwddifnval 37021* | The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴) ⇒ ⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · (( -1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | ||
| Theorem | fwddifn0 37022 | The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ((0 △n 𝐹)‘𝑋) = (𝐹‘𝑋)) | ||
| Theorem | fwddifnp1 37023* | The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑋 + 𝑘) ∈ 𝐴) ⇒ ⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋))) | ||
| Theorem | rank0 37024 | The rank of the empty set is ∅. (Contributed by Scott Fenton, 17-Jul-2015.) |
| ⊢ (rank‘∅) = ∅ | ||
| Theorem | rankeq1o 37025 | The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015.) |
| ⊢ ((rank‘𝐴) = 1o ↔ 𝐴 = {∅}) | ||
| Theorem | hftr 37026 | The class of all hereditarily finite sets is transitive. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ Tr HF | ||
| Theorem | hfext 37027* | Extensionality for HF sets depends only on comparison of HF elements. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ ((𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ HF (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))) | ||
| Theorem | hfninf 37028 | ω is not hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015.) |
| ⊢ ¬ ω ∈ HF | ||
| Syntax | cnmul 37029 | Declare the syntax for natural multiplication. |
| class ·no | ||
| Definition | df-nmul 37030* | Define natural ordinal multiplication. This is the corresponding operation to df-nadd 8679. (Contributed by Scott Fenton, 2-Jun-2026.) |
| ⊢ ·no = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑝 ∈ V, 𝑚 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑎⦌⦋(2nd ‘𝑝) / 𝑏⦌∩ {𝑧 ∈ On ∣ ∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐𝑚𝑏) +no (𝑎𝑚𝑑)) ∈ (𝑧 +no (𝑐𝑚𝑑))})) | ||
| Theorem | nmulfn 37031 | Natural multiplication is a function over pairs of ordinals. (Contributed by Scott Fenton, 2-Jun-2026.) |
| ⊢ ·no Fn (On × On) | ||
| Theorem | nmulprop 37032* | Show closure and value of natural multiplication. (Contributed by Scott Fenton, 2-Jun-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})) | ||
| Theorem | nmulcl 37033 | Closure law for natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·no 𝐵) ∈ On) | ||
| Theorem | nmulval 37034* | Show the value of natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) | ||
| Theorem | nmulcld 37035 | Closure law for natural multiplication. Deduction form. (Contributed by Scott Fenton, 12-Jun-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 ·no 𝐵) ∈ On) | ||
| Theorem | nmulcom 37036 | Natural multiplication is commutative. (Contributed by Scott Fenton, 10-Jun-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·no 𝐵) = (𝐵 ·no 𝐴)) | ||
| Theorem | nmulr0 37037 | Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026.) |
| ⊢ (𝐴 ∈ On → (𝐴 ·no ∅) = ∅) | ||
| Theorem | nmull0 37038 | Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026.) |
| ⊢ (𝐴 ∈ On → (∅ ·no 𝐴) = ∅) | ||
| Theorem | nmulrid 37039 | Identity law for natural multiplication. (Contributed by Scott Fenton, 21-Jul-2026.) |
| ⊢ (𝐴 ∈ On → (𝐴 ·no 1o) = 𝐴) | ||
| Theorem | nmullid 37040 | Identity law for natural multiplication. (Contributed by Scott Fenton, 21-Jul-2026.) |
| ⊢ (𝐴 ∈ On → (1o ·no 𝐴) = 𝐴) | ||
| Theorem | onelond 37041 | An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. Lemma 1.3 of [Schloeder] p. 1. Deduction form. (Contributed by Scott Fenton, 31-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ On) | ||
| Theorem | ontr2d 37042 | Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. Deduction form. (Contributed by Scott Fenton, 31-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ∈ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝐶) | ||
| Theorem | onelssd 37043 | An element of an ordinal number is a subset of the number. Deduction form. (Contributed by Scott Fenton, 31-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | ||
| Theorem | nmulr0d 37044 | Natural multiplication by zero. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 ·no ∅) = ∅) | ||
| Theorem | nmull0d 37045 | Natural multiplication by zero. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → (∅ ·no 𝐴) = ∅) | ||
| Theorem | nmulridd 37046 | Identity law for natural multiplication. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 ·no 1o) = 𝐴) | ||
| Theorem | nmullidd 37047 | Identity law for natural multiplication. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → (1o ·no 𝐴) = 𝐴) | ||
| Theorem | nmulcomd 37048 | Natural multiplication commutes. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 ·no 𝐵) = (𝐵 ·no 𝐴)) | ||
| Theorem | naddridd 37049 | Identity law for natural addition. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 +no ∅) = 𝐴) | ||
| Theorem | naddlidd 37050 | Identity law for natural addition. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) ⇒ ⊢ (𝜑 → (∅ +no 𝐴) = 𝐴) | ||
| Theorem | naddcomd 37051 | Natural addition commutes. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 +no 𝐵) = (𝐵 +no 𝐴)) | ||
| Theorem | naddassd 37052 | Natural addition associates. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) ⇒ ⊢ (𝜑 → ((𝐴 +no 𝐵) +no 𝐶) = (𝐴 +no (𝐵 +no 𝐶))) | ||
| Theorem | nadd32d 37053 | Commutative/associative law that swaps the last two terms in a triple sum. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) ⇒ ⊢ (𝜑 → ((𝐴 +no 𝐵) +no 𝐶) = ((𝐴 +no 𝐶) +no 𝐵)) | ||
| Theorem | nmuladdel 37054 | Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026.) |
| ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) → ((𝐶 ·no 𝐵) +no (𝐴 ·no 𝐷)) ∈ ((𝐴 ·no 𝐵) +no (𝐶 ·no 𝐷))) | ||
| Theorem | nmuladdss 37055 | Ordering relationship for natural ordinal operations. (Contributed by Scott Fenton, 15-Jul-2026.) |
| ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵)) → ((𝐶 ·no 𝐵) +no (𝐴 ·no 𝐷)) ⊆ ((𝐴 ·no 𝐵) +no (𝐶 ·no 𝐷))) | ||
| Theorem | nmulss1 37056 | Natural multiplication preserves less-than or equal. (Contributed by Scott Fenton, 15-Jul-2026.) |
| ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ·no 𝐴) ⊆ (𝐶 ·no 𝐵)) | ||
| Theorem | nmulel1 37057 | Natural multiplication by a non-zero number preserves less-than. (Contributed by Scott Fenton, 15-Jul-2026.) |
| ⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ≠ ∅)) → (𝐶 ·no 𝐴) ∈ (𝐶 ·no 𝐵)) | ||
| Theorem | ltnmul 37058* | Characterize less-than a natural product. (Contributed by Scott Fenton, 15-Jul-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ (𝐵 ·no 𝐶) ↔ ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 (𝐴 +no (𝑏 ·no 𝑐)) ⊆ ((𝑏 ·no 𝐶) +no (𝐵 ·no 𝑐)))) | ||
| Theorem | nmulle 37059* | A condition for bounding a natural product above. Converse of ltnmul 37058. (Contributed by Scott Fenton, 16-Jul-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·no 𝐵) ⊆ 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝐶 +no (𝑎 ·no 𝑏)))) | ||
| Theorem | ltnadd 37060* | Condition for bounding a natural sum below. (Contributed by Scott Fenton, 21-Jul-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ (𝐵 +no 𝐶) ↔ (∃𝑏 ∈ 𝐵 𝐴 ⊆ (𝑏 +no 𝐶) ∨ ∃𝑐 ∈ 𝐶 𝐴 ⊆ (𝐵 +no 𝑐)))) | ||
| Theorem | naddle 37061* | Condition for bounding natural addition above. (Contributed by Scott Fenton, 21-Jul-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) ⊆ 𝐶 ↔ (∀𝑎 ∈ 𝐴 (𝑎 +no 𝐵) ∈ 𝐶 ∧ ∀𝑏 ∈ 𝐵 (𝐴 +no 𝑏) ∈ 𝐶))) | ||
| Theorem | nadddilem1 37062* | Lemma for nadddi 37066. Prove a subcase of the reverse implication. (Contributed by Scott Fenton, 31-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑓 ∈ 𝐶 (𝐴 ·no (𝐵 +no 𝑓)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝑓))) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑓 ∈ 𝐶 (𝑑 ·no (𝐵 +no 𝑓)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝑓))) ⇒ ⊢ ((𝜑 ∧ 𝑌 ∈ (𝐴 ·no 𝐶)) → ((𝐴 ·no 𝐵) +no 𝑌) ∈ (𝐴 ·no (𝐵 +no 𝐶))) | ||
| Theorem | nadddilem2 37063* | Lemma for nadddi 37066. Prove the reverse implication. (Contributed by Scott Fenton, 31-Jul-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑒 ∈ 𝐵 (𝐴 ·no (𝑒 +no 𝐶)) = ((𝐴 ·no 𝑒) +no (𝐴 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑓 ∈ 𝐶 (𝐴 ·no (𝐵 +no 𝑓)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝑓))) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑒 ∈ 𝐵 (𝑑 ·no (𝑒 +no 𝐶)) = ((𝑑 ·no 𝑒) +no (𝑑 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑓 ∈ 𝐶 (𝑑 ·no (𝐵 +no 𝑓)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝑓))) ⇒ ⊢ (𝜑 → ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶)) ⊆ (𝐴 ·no (𝐵 +no 𝐶))) | ||
| Theorem | nadddilem3 37064* | Lemma for nadddi 37066. Prove a subcase of the forward implication. (Contributed by Scott Fenton, 3-Aug-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ (𝐵 +no 𝐶)) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ⊆ (𝑍 +no 𝐶)) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑒 ∈ 𝐵 (𝐴 ·no (𝑒 +no 𝐶)) = ((𝐴 ·no 𝑒) +no (𝐴 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑒 ∈ 𝐵 (𝑑 ·no (𝑒 +no 𝐶)) = ((𝑑 ·no 𝑒) +no (𝑑 ·no 𝐶))) ⇒ ⊢ (𝜑 → ((𝑋 ·no (𝐵 +no 𝐶)) +no (𝐴 ·no 𝑌)) ∈ (((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶)) +no (𝑋 ·no 𝑌))) | ||
| Theorem | nadddilem4 37065* | Lemma for nadddi 37066. Prove the forward implication. (Contributed by Scott Fenton, 3-Aug-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 (𝑑 ·no (𝐵 +no 𝐶)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑒 ∈ 𝐵 (𝐴 ·no (𝑒 +no 𝐶)) = ((𝐴 ·no 𝑒) +no (𝐴 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑓 ∈ 𝐶 (𝐴 ·no (𝐵 +no 𝑓)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝑓))) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑒 ∈ 𝐵 (𝑑 ·no (𝑒 +no 𝐶)) = ((𝑑 ·no 𝑒) +no (𝑑 ·no 𝐶))) & ⊢ (𝜑 → ∀𝑑 ∈ 𝐴 ∀𝑓 ∈ 𝐶 (𝑑 ·no (𝐵 +no 𝑓)) = ((𝑑 ·no 𝐵) +no (𝑑 ·no 𝑓))) ⇒ ⊢ (𝜑 → (𝐴 ·no (𝐵 +no 𝐶)) ⊆ ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶))) | ||
| Theorem | nadddi 37066 | Natural multiplication distributes over natural addition. (Contributed by Scott Fenton, 27-Jul-2026.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·no (𝐵 +no 𝐶)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶))) | ||
| Theorem | nadddid 37067 | Natural multiplication distributes over natural addition. Deduction form. (Contributed by Scott Fenton, 3-Aug-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) ⇒ ⊢ (𝜑 → (𝐴 ·no (𝐵 +no 𝐶)) = ((𝐴 ·no 𝐵) +no (𝐴 ·no 𝐶))) | ||
| Theorem | nadddird 37068 | Natural multiplication distributes over natural addition. Deduction form. (Contributed by Scott Fenton, 3-Aug-2026.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐶 ∈ On) ⇒ ⊢ (𝜑 → ((𝐴 +no 𝐵) ·no 𝐶) = ((𝐴 ·no 𝐶) +no (𝐵 ·no 𝐶))) | ||
| Theorem | rmoeqi 37069 | Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓) | ||
| Theorem | rmoeqbii 37070 | Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒) | ||
| Theorem | reueqi 37071 | Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜓) | ||
| Theorem | reueqbii 37072 | Equality inference for restricted existential uniqueness quantifier. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃!𝑥 ∈ 𝐴 𝜓 ↔ ∃!𝑥 ∈ 𝐵 𝜒) | ||
| Theorem | sbceqbii 37073 | Formula-building inference for class substitution. General version of sbcbii 3794. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]𝜑 ↔ [𝐵 / 𝑥]𝜓) | ||
| Theorem | disjeq1i 37074 | Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐶) | ||
| Theorem | disjeq12i 37075 | Equality theorem for disjoint collection. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷) | ||
| Theorem | rabeqbii 37076 | Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐵 ∣ 𝜓} | ||
| Theorem | iuneq12i 37077 | Equality theorem for indexed union. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | iineq1i 37078 | Equality theorem for indexed intersection. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐶 | ||
| Theorem | iineq12i 37079 | Equality theorem for indexed intersection. Inference version. General version of iineq1i 37078. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | riotaeqbii 37080 | Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜓) | ||
| Theorem | riotaeqi 37081 | Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥 ∈ 𝐵 𝜑) | ||
| Theorem | ixpeq1i 37082 | Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶 | ||
| Theorem | ixpeq12i 37083 | Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | sumeq2si 37084 | Equality inference for sum. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐵 = 𝐶 ⇒ ⊢ Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | sumeq12si 37085 | Equality inference for sum. General version of sumeq2si 37084. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ Σ𝑥 ∈ 𝐴 𝐶 = Σ𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | prodeq2si 37086 | Equality inference for product. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐵 = 𝐶 ⇒ ⊢ ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶 | ||
| Theorem | prodeq12si 37087 | Equality inference for product. General version of prodeq2si 37086. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∏𝑥 ∈ 𝐴 𝐶 = ∏𝑥 ∈ 𝐵 𝐷 | ||
| Theorem | itgeq12i 37088 | Equality inference for an integral. General version of itgeq1i 37089 and itgeq2i 37090. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐷 d𝑥 | ||
| Theorem | itgeq1i 37089 | Equality inference for an integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥 | ||
| Theorem | itgeq2i 37090 | Equality inference for an integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐵 = 𝐶 ⇒ ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥 | ||
| Theorem | ditgeq123i 37091 | Equality inference for the directed integral. General version of ditgeq12i 37092 and ditgeq3i 37093. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 & ⊢ 𝐸 = 𝐹 ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐹 d𝑥 | ||
| Theorem | ditgeq12i 37092 | Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐶]𝐸 d𝑥 = ⨜[𝐵 → 𝐷]𝐸 d𝑥 | ||
| Theorem | ditgeq3i 37093 | Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025.) |
| ⊢ 𝐶 = 𝐷 ⇒ ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑥 | ||
| Theorem | rmoeqdv 37094* | Formula-building rule for restricted at-most-one quantifier. Deduction form. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜓)) | ||
| Theorem | rmoeqbidv 37095* | Formula-building rule for restricted at-most-one quantifier. Deduction form. General version of rmobidv 3380. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥 ∈ 𝐴 𝜓 ↔ ∃*𝑥 ∈ 𝐵 𝜒)) | ||
| Theorem | sbequbidv 37096* | Deduction substituting both sides of a biconditional. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝑢 = 𝑣) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑢 / 𝑥]𝜓 ↔ [𝑣 / 𝑥]𝜒)) | ||
| Theorem | disjeq12dv 37097* | Equality theorem for disjoint collection. Deduction version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (Disj 𝑥 ∈ 𝐴 𝐶 ↔ Disj 𝑥 ∈ 𝐵 𝐷)) | ||
| Theorem | ixpeq12dv 37098* | Equality theorem for infinite Cartesian product. Deduction version. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐷) | ||
| Theorem | sumeq12sdv 37099* | Equality deduction for sum. General version of sumeq2sdv 15876. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐷) | ||
| Theorem | prodeq12sdv 37100* | Equality deduction for product. General version of prodeq2sdv 16097. (Contributed by GG, 1-Sep-2025.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐶 = ∏𝑘 ∈ 𝐵 𝐷) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |