Home | Metamath
Proof Explorer Theorem List (p. 75 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rdgfnon 7401 | The recursive definition generator is a function on ordinal numbers. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ rec(𝐹, 𝐴) Fn On | ||
Theorem | rdgvalg 7402* | Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐴) ↾ 𝐵))) | ||
Theorem | rdgval 7403* | Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐵 ∈ On → (rec(𝐹, 𝐴)‘𝐵) = ((𝑔 ∈ V ↦ if(𝑔 = ∅, 𝐴, if(Lim dom 𝑔, ∪ ran 𝑔, (𝐹‘(𝑔‘∪ dom 𝑔)))))‘(rec(𝐹, 𝐴) ↾ 𝐵))) | ||
Theorem | rdg0 7404 | The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (rec(𝐹, 𝐴)‘∅) = 𝐴 | ||
Theorem | rdgseg 7405 | The initial segments of the recursive definition generator are sets. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴) ↾ 𝐵) ∈ V) | ||
Theorem | rdgsucg 7406 | The value of the recursive definition generator at a successor. (Contributed by NM, 16-Nov-2014.) |
⊢ (𝐵 ∈ dom rec(𝐹, 𝐴) → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | rdgsuc 7407 | The value of the recursive definition generator at a successor. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ (𝐵 ∈ On → (rec(𝐹, 𝐴)‘suc 𝐵) = (𝐹‘(rec(𝐹, 𝐴)‘𝐵))) | ||
Theorem | rdglimg 7408 | The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 16-Nov-2014.) |
⊢ ((𝐵 ∈ dom rec(𝐹, 𝐴) ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵)) | ||
Theorem | rdglim 7409 | The value of the recursive definition generator at a limit ordinal. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ (rec(𝐹, 𝐴) “ 𝐵)) | ||
Theorem | rdg0g 7410 | The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.) |
⊢ (𝐴 ∈ 𝐶 → (rec(𝐹, 𝐴)‘∅) = 𝐴) | ||
Theorem | rdgsucmptf 7411 | The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | rdgsucmptnf 7412 | The value of the recursive definition generator at a successor (special case where the characteristic function is an ordered-pair class abstraction and where the mapping class 𝐷 is a proper class). This is a technical lemma that can be used together with rdgsucmptf 7411 to help eliminate redundant sethood antecedents. (Contributed by NM, 22-Oct-2003.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (¬ 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅) | ||
Theorem | rdgsucmpt2 7413* | This version of rdgsucmpt 7414 avoids the not-free hypothesis of rdgsucmptf 7411 by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶) & ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | rdgsucmpt 7414* | The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by Mario Carneiro, 9-Sep-2013.) |
⊢ 𝐹 = rec((𝑥 ∈ V ↦ 𝐶), 𝐴) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | rdglim2 7415* | The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values. (Contributed by NM, 23-Apr-1995.) |
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 = (rec(𝐹, 𝐴)‘𝑥)}) | ||
Theorem | rdglim2a 7416* | The value of the recursive definition generator at a limit ordinal, in terms of indexed union of all smaller values. (Contributed by NM, 28-Jun-1998.) |
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (rec(𝐹, 𝐴)‘𝐵) = ∪ 𝑥 ∈ 𝐵 (rec(𝐹, 𝐴)‘𝑥)) | ||
Theorem | frfnom 7417 | The function generated by finite recursive definition generation is a function on omega. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ (rec(𝐹, 𝐴) ↾ ω) Fn ω | ||
Theorem | fr0g 7418 | The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) |
⊢ (𝐴 ∈ 𝐵 → ((rec(𝐹, 𝐴) ↾ ω)‘∅) = 𝐴) | ||
Theorem | frsuc 7419 | The successor value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐵 ∈ ω → ((rec(𝐹, 𝐴) ↾ ω)‘suc 𝐵) = (𝐹‘((rec(𝐹, 𝐴) ↾ ω)‘𝐵))) | ||
Theorem | frsucmpt 7420 | The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003.) (Revised by Scott Fenton, 2-Nov-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ ((𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | frsucmptn 7421 | The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class 𝐷 is a proper class). This is a technical lemma that can be used together with frsucmpt 7420 to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011.) (Revised by Mario Carneiro, 11-Sep-2015.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝐷 & ⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) & ⊢ (𝑥 = (𝐹‘𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (¬ 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅) | ||
Theorem | frsucmpt2 7422* | The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) & ⊢ (𝑦 = 𝑥 → 𝐸 = 𝐶) & ⊢ (𝑦 = (𝐹‘𝐵) → 𝐸 = 𝐷) ⇒ ⊢ ((𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉) → (𝐹‘suc 𝐵) = 𝐷) | ||
Theorem | tz7.48lem 7423* | A way of showing an ordinal function is one-to-one. (Contributed by NM, 9-Feb-1997.) |
⊢ 𝐹 Fn On ⇒ ⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ 𝐴)) | ||
Theorem | tz7.48-2 7424* | Proposition 7.48(2) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) (Revised by David Abernethy, 5-May-2013.) |
⊢ 𝐹 Fn On ⇒ ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → Fun ◡𝐹) | ||
Theorem | tz7.48-1 7425* | Proposition 7.48(1) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) |
⊢ 𝐹 Fn On ⇒ ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ran 𝐹 ⊆ 𝐴) | ||
Theorem | tz7.48-3 7426* | Proposition 7.48(3) of [TakeutiZaring] p. 51. (Contributed by NM, 9-Feb-1997.) |
⊢ 𝐹 Fn On ⇒ ⊢ (∀𝑥 ∈ On (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ 𝐴 ∈ V) | ||
Theorem | tz7.49 7427* | Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 10-Jan-2013.) |
⊢ 𝐹 Fn On & ⊢ (𝜑 ↔ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜑) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴 ∖ (𝐹 “ 𝑦)) ≠ ∅ ∧ (𝐹 “ 𝑥) = 𝐴 ∧ Fun ◡(𝐹 ↾ 𝑥))) | ||
Theorem | tz7.49c 7428* | Corollary of Proposition 7.49 of [TakeutiZaring] p. 51. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 19-Jan-2013.) |
⊢ 𝐹 Fn On ⇒ ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ On ((𝐴 ∖ (𝐹 “ 𝑥)) ≠ ∅ → (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)))) → ∃𝑥 ∈ On (𝐹 ↾ 𝑥):𝑥–1-1-onto→𝐴) | ||
Syntax | cseqom 7429 | Extend class notation to include index-aware recursive definitions. |
class seq𝜔(𝐹, 𝐼) | ||
Definition | df-seqom 7430* | Index-aware recursive definitions over ω. A mashup of df-rdg 7393 and df-seq 12664, this allows for recursive definitions that use an index in the recursion in cases where Infinity is not admitted. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ seq𝜔(𝐹, 𝐼) = (rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) “ ω) | ||
Theorem | seqomlem0 7431* | Lemma for seq𝜔. Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ rec((𝑎 ∈ ω, 𝑏 ∈ V ↦ 〈suc 𝑎, (𝑎𝐹𝑏)〉), 〈∅, ( I ‘𝐼)〉) = rec((𝑐 ∈ ω, 𝑑 ∈ V ↦ 〈suc 𝑐, (𝑐𝐹𝑑)〉), 〈∅, ( I ‘𝐼)〉) | ||
Theorem | seqomlem1 7432* | Lemma for seq𝜔. The underlying recursion generates a sequence of pairs with the expected first values. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ (𝐴 ∈ ω → (𝑄‘𝐴) = 〈𝐴, (2nd ‘(𝑄‘𝐴))〉) | ||
Theorem | seqomlem2 7433* | Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ (𝑄 “ ω) Fn ω | ||
Theorem | seqomlem3 7434* | Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ ((𝑄 “ ω)‘∅) = ( I ‘𝐼) | ||
Theorem | seqomlem4 7435* | Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.) |
⊢ 𝑄 = rec((𝑖 ∈ ω, 𝑣 ∈ V ↦ 〈suc 𝑖, (𝑖𝐹𝑣)〉), 〈∅, ( I ‘𝐼)〉) ⇒ ⊢ (𝐴 ∈ ω → ((𝑄 “ ω)‘suc 𝐴) = (𝐴𝐹((𝑄 “ ω)‘𝐴))) | ||
Theorem | seqomeq12 7436 | Equality theorem for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → seq𝜔(𝐴, 𝐶) = seq𝜔(𝐵, 𝐷)) | ||
Theorem | fnseqom 7437 | An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝐺 = seq𝜔(𝐹, 𝐼) ⇒ ⊢ 𝐺 Fn ω | ||
Theorem | seqom0g 7438 | Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revise by AV, 17-Sep-2021.) |
⊢ 𝐺 = seq𝜔(𝐹, 𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝐺‘∅) = 𝐼) | ||
Theorem | seqomsuc 7439 | Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.) |
⊢ 𝐺 = seq𝜔(𝐹, 𝐼) ⇒ ⊢ (𝐴 ∈ ω → (𝐺‘suc 𝐴) = (𝐴𝐹(𝐺‘𝐴))) | ||
Syntax | c1o 7440 | Extend the definition of a class to include the ordinal number 1. |
class 1𝑜 | ||
Syntax | c2o 7441 | Extend the definition of a class to include the ordinal number 2. |
class 2𝑜 | ||
Syntax | c3o 7442 | Extend the definition of a class to include the ordinal number 3. |
class 3𝑜 | ||
Syntax | c4o 7443 | Extend the definition of a class to include the ordinal number 4. |
class 4𝑜 | ||
Syntax | coa 7444 | Extend the definition of a class to include the ordinal addition operation. |
class +𝑜 | ||
Syntax | comu 7445 | Extend the definition of a class to include the ordinal multiplication operation. |
class ·𝑜 | ||
Syntax | coe 7446 | Extend the definition of a class to include the ordinal exponentiation operation. |
class ↑𝑜 | ||
Definition | df-1o 7447 | Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.) |
⊢ 1𝑜 = suc ∅ | ||
Definition | df-2o 7448 | Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.) |
⊢ 2𝑜 = suc 1𝑜 | ||
Definition | df-3o 7449 | Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 3𝑜 = suc 2𝑜 | ||
Definition | df-4o 7450 | Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.) |
⊢ 4𝑜 = suc 3𝑜 | ||
Definition | df-oadd 7451* | Define the ordinal addition operation. (Contributed by NM, 3-May-1995.) |
⊢ +𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ suc 𝑧), 𝑥)‘𝑦)) | ||
Definition | df-omul 7452* | Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.) |
⊢ ·𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ (rec((𝑧 ∈ V ↦ (𝑧 +𝑜 𝑥)), ∅)‘𝑦)) | ||
Definition | df-oexp 7453* | Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.) |
⊢ ↑𝑜 = (𝑥 ∈ On, 𝑦 ∈ On ↦ if(𝑥 = ∅, (1𝑜 ∖ 𝑦), (rec((𝑧 ∈ V ↦ (𝑧 ·𝑜 𝑥)), 1𝑜)‘𝑦))) | ||
Theorem | 1on 7454 | Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.) |
⊢ 1𝑜 ∈ On | ||
Theorem | 2on 7455 | Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ 2𝑜 ∈ On | ||
Theorem | 2on0 7456 | Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.) |
⊢ 2𝑜 ≠ ∅ | ||
Theorem | 3on 7457 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 3𝑜 ∈ On | ||
Theorem | 4on 7458 | Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.) |
⊢ 4𝑜 ∈ On | ||
Theorem | df1o2 7459 | Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
⊢ 1𝑜 = {∅} | ||
Theorem | df2o3 7460 | Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 2𝑜 = {∅, 1𝑜} | ||
Theorem | df2o2 7461 | Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.) |
⊢ 2𝑜 = {∅, {∅}} | ||
Theorem | 1n0 7462 | Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.) |
⊢ 1𝑜 ≠ ∅ | ||
Theorem | xp01disj 7463 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.) |
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1𝑜})) = ∅ | ||
Theorem | ordgt0ge1 7464 | Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1𝑜 ⊆ 𝐴)) | ||
Theorem | ordge1n0 7465 | An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004.) |
⊢ (Ord 𝐴 → (1𝑜 ⊆ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | el1o 7466 | Membership in ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ 1𝑜 ↔ 𝐴 = ∅) | ||
Theorem | dif1o 7467 | Two ways to say that 𝐴 is a nonzero number of the set 𝐵. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ∖ 1𝑜) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) | ||
Theorem | ondif1 7468 | Two ways to say that 𝐴 is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 1𝑜) ↔ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) | ||
Theorem | ondif2 7469 | Two ways to say that 𝐴 is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 2𝑜) ↔ (𝐴 ∈ On ∧ 1𝑜 ∈ 𝐴)) | ||
Theorem | 2oconcl 7470 | Closure of the pair swapping function on 2𝑜. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ (𝐴 ∈ 2𝑜 → (1𝑜 ∖ 𝐴) ∈ 2𝑜) | ||
Theorem | 0lt1o 7471 | Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
⊢ ∅ ∈ 1𝑜 | ||
Theorem | dif20el 7472 | An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015.) |
⊢ (𝐴 ∈ (On ∖ 2𝑜) → ∅ ∈ 𝐴) | ||
Theorem | 0we1 7473 | The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015.) |
⊢ ∅ We 1𝑜 | ||
Theorem | brwitnlem 7474 | Lemma for relations which assert the existence of a witness in a two-parameter set. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ 𝑅 = (◡𝑂 “ (V ∖ 1𝑜)) & ⊢ 𝑂 Fn 𝑋 ⇒ ⊢ (𝐴𝑅𝐵 ↔ (𝐴𝑂𝐵) ≠ ∅) | ||
Theorem | fnoa 7475 | Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ +𝑜 Fn (On × On) | ||
Theorem | fnom 7476 | Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ·𝑜 Fn (On × On) | ||
Theorem | fnoe 7477 | Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ ↑𝑜 Fn (On × On) | ||
Theorem | oav 7478* | Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) | ||
Theorem | omv 7479* | Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +𝑜 𝐴)), ∅)‘𝐵)) | ||
Theorem | oe0lem 7480 | A helper lemma for oe0 7489 and others. (Contributed by NM, 6-Jan-2005.) |
⊢ ((𝜑 ∧ 𝐴 = ∅) → 𝜓) & ⊢ (((𝐴 ∈ On ∧ 𝜑) ∧ ∅ ∈ 𝐴) → 𝜓) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝜑) → 𝜓) | ||
Theorem | oev 7481* | Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜 𝐵) = if(𝐴 = ∅, (1𝑜 ∖ 𝐵), (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵))) | ||
Theorem | oevn0 7482* | Value of ordinal exponentiation at a nonzero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵)) | ||
Theorem | oa0 7483 | Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 +𝑜 ∅) = 𝐴) | ||
Theorem | om0 7484 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 ·𝑜 ∅) = ∅) | ||
Theorem | oe0m 7485 | Ordinal exponentiation with zero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (∅ ↑𝑜 𝐴) = (1𝑜 ∖ 𝐴)) | ||
Theorem | om0x 7486 | Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. Unlike om0 7484, this version works whether or not 𝐴 is an ordinal. However, since it is an artifact of our particular function value definition outside the domain, we will not use it in order to be conventional and present it only as a curiosity. (Contributed by NM, 1-Feb-1996.) |
⊢ (𝐴 ·𝑜 ∅) = ∅ | ||
Theorem | oe0m0 7487 | Ordinal exponentiation with zero mantissa and zero exponent. Proposition 8.31 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) |
⊢ (∅ ↑𝑜 ∅) = 1𝑜 | ||
Theorem | oe0m1 7488 | Ordinal exponentiation with zero mantissa and nonzero exponent. Proposition 8.31(2) of [TakeutiZaring] p. 67 and its converse. (Contributed by NM, 5-Jan-2005.) |
⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ (∅ ↑𝑜 𝐴) = ∅)) | ||
Theorem | oe0 7489 | Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ (𝐴 ∈ On → (𝐴 ↑𝑜 ∅) = 1𝑜) | ||
Theorem | oev2 7490* | Alternate value of ordinal exponentiation. Compare oev 7481. (Contributed by NM, 2-Jan-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜 𝐵) = ((rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵) ∩ ((V ∖ ∩ 𝐴) ∪ ∩ 𝐵))) | ||
Theorem | oasuc 7491 | Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 suc 𝐵) = suc (𝐴 +𝑜 𝐵)) | ||
Theorem | oesuclem 7492* | Lemma for oesuc 7494. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ Lim 𝑋 & ⊢ (𝐵 ∈ 𝑋 → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵))) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) → (𝐴 ↑𝑜 suc 𝐵) = ((𝐴 ↑𝑜 𝐵) ·𝑜 𝐴)) | ||
Theorem | omsuc 7493 | Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 suc 𝐵) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐴)) | ||
Theorem | oesuc 7494 | Ordinal exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜 suc 𝐵) = ((𝐴 ↑𝑜 𝐵) ·𝑜 𝐴)) | ||
Theorem | onasuc 7495 | Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Note that this version of oasuc 7491 does not need Replacement.) (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +𝑜 suc 𝐵) = suc (𝐴 +𝑜 𝐵)) | ||
Theorem | onmsuc 7496 | Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜 suc 𝐵) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐴)) | ||
Theorem | onesuc 7497 | Exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by Mario Carneiro, 14-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ↑𝑜 suc 𝐵) = ((𝐴 ↑𝑜 𝐵) ·𝑜 𝐴)) | ||
Theorem | oa1suc 7498 | Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson] p. 266. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ∈ On → (𝐴 +𝑜 1𝑜) = suc 𝐴) | ||
Theorem | oalim 7499* | Ordinal addition with a limit ordinal. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 +𝑜 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 +𝑜 𝑥)) | ||
Theorem | omlim 7500* | Ordinal multiplication with a limit ordinal. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ·𝑜 𝐵) = ∪ 𝑥 ∈ 𝐵 (𝐴 ·𝑜 𝑥)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |