![]() |
Metamath
Proof Explorer Theorem List (p. 78 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ofexg 7701 | A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → ( ∘f 𝑅 ↾ 𝐴) ∈ V) | ||
Theorem | nfof 7702 | Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘f 𝑅 | ||
Theorem | nfofr 7703 | Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘r 𝑅 | ||
Theorem | ofrfvalg 7704* | Value of a relation applied to two functions. Originally part of ofrfval 7706, this version assumes the functions are sets rather than their domains, avoiding ax-rep 5284. (Contributed by SN, 5-Aug-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) | ||
Theorem | offval 7705* | Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) | ||
Theorem | ofrfval 7706* | Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) | ||
Theorem | ofval 7707 | Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) | ||
Theorem | ofrval 7708 | Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∘r 𝑅𝐺 ∧ 𝑋 ∈ 𝑆) → 𝐶𝑅𝐷) | ||
Theorem | offn 7709 | The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) Fn 𝑆) | ||
Theorem | offun 7710 | The function operation produces a function. (Contributed by SN, 23-Jul-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → Fun (𝐹 ∘f 𝑅𝐺)) | ||
Theorem | offval2f 7711* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofmresval 7712 | Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹( ∘f 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹 ∘f 𝑅𝐺)) | ||
Theorem | fnfvof 7713 | Function value of a pointwise composition. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Jun-2015.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) ∧ (𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) | ||
Theorem | off 7714* | The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) | ||
Theorem | ofres 7715 | Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = ((𝐹 ↾ 𝐶) ∘f 𝑅(𝐺 ↾ 𝐶))) | ||
Theorem | offval2 7716* | The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofrfval2 7717* | The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) | ||
Theorem | offvalfv 7718* | The function operation expressed as a mapping with function values. (Contributed by AV, 6-Apr-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) | ||
Theorem | ofmpteq 7719* | Value of a pointwise operation on two functions defined using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ↦ 𝐶) Fn 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∘f 𝑅(𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | coof 7720* | The composition of a homomorphism with a function operation. (Contributed by SN, 20-May-2025.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐻 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑏𝑅𝑐) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝐻‘(𝑏𝑅𝑐)) = ((𝐻‘𝑏)𝑆(𝐻‘𝑐))) ⇒ ⊢ (𝜑 → (𝐻 ∘ (𝐹 ∘f 𝑅𝐺)) = ((𝐻 ∘ 𝐹) ∘f 𝑆(𝐻 ∘ 𝐺))) | ||
Theorem | ofco 7721 | The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐻:𝐷⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘f 𝑅(𝐺 ∘ 𝐻))) | ||
Theorem | offveq 7722* | Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐻 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵𝑅𝐶) = (𝐻‘𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = 𝐻) | ||
Theorem | offveqb 7723* | Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐴) & ⊢ (𝜑 → 𝐻 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = 𝐶) ⇒ ⊢ (𝜑 → (𝐻 = (𝐹 ∘f 𝑅𝐺) ↔ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐵𝑅𝐶))) | ||
Theorem | ofc1 7724 | Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘f 𝑅𝐹)‘𝑋) = (𝐵𝑅𝐶)) | ||
Theorem | ofc2 7725 | Right operation by a constant. (Contributed by NM, 7-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f 𝑅(𝐴 × {𝐵}))‘𝑋) = (𝐶𝑅𝐵)) | ||
Theorem | ofc12 7726 | Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) | ||
Theorem | caofref 7727* | Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘r 𝑅𝐹) | ||
Theorem | caofinvl 7728* | Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑁:𝑆⟶𝑆) & ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘f 𝑅𝐹) = (𝐴 × {𝐵})) | ||
Theorem | caofid0l 7729* | Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝑥) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = 𝐹) | ||
Theorem | caofid0r 7730* | Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝑥) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = 𝐹) | ||
Theorem | caofid1 7731* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = (𝐴 × {𝐶})) | ||
Theorem | caofid2 7732* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = (𝐴 × {𝐶})) | ||
Theorem | caofcom 7733* | Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐺 ∘f 𝑅𝐹)) | ||
Theorem | caofrss 7734* | Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 → 𝐹 ∘r 𝑇𝐺)) | ||
Theorem | caofass 7735* | Transfer an associative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦)𝑇𝑧) = (𝑥𝑂(𝑦𝑃𝑧))) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘f 𝑇𝐻) = (𝐹 ∘f 𝑂(𝐺 ∘f 𝑃𝐻))) | ||
Theorem | caoftrn 7736* | Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘r 𝑅𝐺 ∧ 𝐺 ∘r 𝑇𝐻) → 𝐹 ∘r 𝑈𝐻)) | ||
Theorem | caofdi 7737* | Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑇(𝑦𝑅𝑧)) = ((𝑥𝑇𝑦)𝑂(𝑥𝑇𝑧))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑇(𝐺 ∘f 𝑅𝐻)) = ((𝐹 ∘f 𝑇𝐺) ∘f 𝑂(𝐹 ∘f 𝑇𝐻))) | ||
Theorem | caofdir 7738* | Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝑅𝑦)𝑇𝑧) = ((𝑥𝑇𝑧)𝑂(𝑦𝑇𝑧))) ⇒ ⊢ (𝜑 → ((𝐺 ∘f 𝑅𝐻) ∘f 𝑇𝐹) = ((𝐺 ∘f 𝑇𝐹) ∘f 𝑂(𝐻 ∘f 𝑇𝐹))) | ||
Theorem | caonncan 7739* | Transfer nncan 11535-shaped laws to vectors of numbers. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴:𝐼⟶𝑆) & ⊢ (𝜑 → 𝐵:𝐼⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) ⇒ ⊢ (𝜑 → (𝐴 ∘f 𝑀(𝐴 ∘f 𝑀𝐵)) = 𝐵) | ||
Syntax | crpss 7740 | Extend class notation to include the reified proper subset relation. |
class [⊊] | ||
Definition | df-rpss 7741* | Define a relation which corresponds to proper subsethood df-pss 3982 on sets. This allows to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss 7746. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] = {〈𝑥, 𝑦〉 ∣ 𝑥 ⊊ 𝑦} | ||
Theorem | relrpss 7742 | The proper subset relation is a relation. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ Rel [⊊] | ||
Theorem | brrpssg 7743 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | brrpss 7744 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵) | ||
Theorem | porpss 7745 | Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] Po 𝐴 | ||
Theorem | sorpss 7746* | Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥)) | ||
Theorem | sorpssi 7747 | Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) | ||
Theorem | sorpssun 7748 | A chain of sets is closed under binary union. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∪ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssin 7749 | A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∩ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssuni 7750* | In a chain of sets, a maximal element is the union of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝑌 → (∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑢 ⊊ 𝑣 ↔ ∪ 𝑌 ∈ 𝑌)) | ||
Theorem | sorpssint 7751* | In a chain of sets, a minimal element is the intersection of the chain. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝑌 → (∃𝑢 ∈ 𝑌 ∀𝑣 ∈ 𝑌 ¬ 𝑣 ⊊ 𝑢 ↔ ∩ 𝑌 ∈ 𝑌)) | ||
Theorem | sorpsscmpl 7752* | The componentwise complement of a chain of sets is also a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ( [⊊] Or 𝑌 → [⊊] Or {𝑢 ∈ 𝒫 𝐴 ∣ (𝐴 ∖ 𝑢) ∈ 𝑌}) | ||
Axiom | ax-un 7753* |
Axiom of Union. An axiom of Zermelo-Fraenkel set theory. It states
that a set 𝑦 exists that includes the union of a
given set 𝑥
i.e. the collection of all members of the members of 𝑥. The
variant axun2 7755 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 7756. A version using class
notation is uniex 7759.
The union of a class df-uni 4912 should not be confused with the union of two classes df-un 3967. Their relationship is shown in unipr 4928. (Contributed by NM, 23-Dec-1993.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfun 7754* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) Use ax-un 7753 instead. (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axun2 7755* | A variant of the Axiom of Union ax-un 7753. For any set 𝑥, there exists a set 𝑦 whose members are exactly the members of the members of 𝑥 i.e. the union of 𝑥. Axiom Union of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) | ||
Theorem | uniex2 7756* | The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | vuniex 7757 | The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) (Revised by BJ, 6-Apr-2024.) |
⊢ ∪ 𝑥 ∈ V | ||
Theorem | uniexg 7758 | The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | ||
Theorem | uniex 7759 | The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3491), then the union of 𝐴 is also a set. Same as Axiom 3 of [TakeutiZaring] p. 16. (Contributed by NM, 11-Aug-1993.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∪ 𝐴 ∈ V | ||
Theorem | uniexd 7760 | Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ V) | ||
Theorem | unexg 7761 | The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) Prove unexg 7761 first and then unex 7762 and unexb 7765 from it. (Revised by BJ, 21-Jul-2025.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | unex 7762 | The union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 1-Jul-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ V | ||
Theorem | unexOLD 7763 | Obsolete version of unex 7762 as of 21-Jul-2025. (Contributed by NM, 1-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∪ 𝐵) ∈ V | ||
Theorem | tpex 7764 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} ∈ V | ||
Theorem | unexb 7765 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | unexbOLD 7766 | Obsolete version of unexb 7765 as of 21-Jul-2025. (Contributed by NM, 11-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | unexgOLD 7767 | Obsolete version of unexg 7761 as of 21-Jul-2025. (Contributed by NM, 18-Sep-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | xpexg 7768 | The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 8004. (Contributed by NM, 14-Aug-1994.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | xpexd 7769 | The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) | ||
Theorem | 3xpexg 7770 | The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
⊢ (𝑉 ∈ 𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V) | ||
Theorem | xpex 7771 | The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 × 𝐵) ∈ V | ||
Theorem | unexd 7772 | The union of two sets is a set. (Contributed by SN, 16-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | sqxpexg 7773 | The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | ||
Theorem | abnexg 7774* | Sufficient condition for a class abstraction to be a proper class. The class 𝐹 can be thought of as an expression in 𝑥 and the abstraction appearing in the statement as the class of values 𝐹 as 𝑥 varies through 𝐴. Assuming the antecedents, if that class is a set, then so is the "domain" 𝐴. The converse holds without antecedent, see abrexexg 7983. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 7776 and pwnex 7777 respectively, proved from abnex 7775, which is a consequence of abnexg 7774 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V)) | ||
Theorem | abnex 7775* | Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 7776 and pwnex 7777. See the comment of abnexg 7774. (Contributed by BJ, 2-May-2021.) |
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V) | ||
Theorem | snnex 7776* | The class of all singletons is a proper class. See also pwnex 7777. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V | ||
Theorem | pwnex 7777* | The class of all power sets is a proper class. See also snnex 7776. (Contributed by BJ, 2-May-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V | ||
Theorem | difex2 7778 | If the subtrahend of a class difference exists, then the minuend exists iff the difference exists. (Contributed by NM, 12-Nov-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ V ↔ (𝐴 ∖ 𝐵) ∈ V)) | ||
Theorem | difsnexi 7779 | If the difference of a class and a singleton is a set, the class itself is a set. (Contributed by AV, 15-Jan-2019.) |
⊢ ((𝑁 ∖ {𝐾}) ∈ V → 𝑁 ∈ V) | ||
Theorem | uniuni 7780* | Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007.) |
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | uniexr 7781 | Converse of the Axiom of Union. Note that it does not require ax-un 7753. (Contributed by NM, 11-Nov-2003.) |
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | uniexb 7782 | The Axiom of Union and its converse. A class is a set iff its union is a set. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝐴 ∈ V ↔ ∪ 𝐴 ∈ V) | ||
Theorem | pwexr 7783 | Converse of the Axiom of Power Sets. Note that it does not require ax-pow 5370. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝒫 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | pwexb 7784 | The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V) | ||
Theorem | elpwpwel 7785 | A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.) |
⊢ (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵) | ||
Theorem | eldifpw 7786 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵)) | ||
Theorem | elpwun 7787 | Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐶) ∈ 𝒫 𝐵) | ||
Theorem | pwuncl 7788 | Power classes are closed under union. (Contributed by AV, 27-Feb-2024.) |
⊢ ((𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋) → (𝐴 ∪ 𝐵) ∈ 𝒫 𝑋) | ||
Theorem | iunpw 7789* | An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of [Enderton] p. 33. (Contributed by NM, 29-Nov-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥) | ||
Theorem | fr3nr 7790 | A well-founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 10-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | epne3 7791 | A well-founded class contains no 3-cycle loops. (Contributed by NM, 19-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
⊢ (( E Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ 𝐵)) | ||
Theorem | dfwe2 7792* | Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | epweon 7793 | The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of [Mendelson] p. 244. For a shorter proof requiring ax-un 7753, see epweonALT 7794. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7753. (Revised by BTernaryTau, 30-Nov-2024.) |
⊢ E We On | ||
Theorem | epweonALT 7794 | Alternate proof of epweon 7793, shorter but requiring ax-un 7753. (Contributed by NM, 1-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ E We On | ||
Theorem | ordon 7795 | The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.) |
⊢ Ord On | ||
Theorem | onprc 7796 | No set contains all ordinal numbers. Proposition 7.13 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. This is also known as the Burali-Forti paradox (remark in [Enderton] p. 194). In 1897, Cesare Burali-Forti noticed that since the "set" of all ordinal numbers is an ordinal class (ordon 7795), it must be both an element of the set of all ordinal numbers yet greater than every such element. ZF set theory resolves this paradox by not allowing the class of all ordinal numbers to be a set (so instead it is a proper class). Here we prove the denial of its existence. (Contributed by NM, 18-May-1994.) |
⊢ ¬ On ∈ V | ||
Theorem | ssorduni 7797 | The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. Lemma 2.7 of [Schloeder] p. 4. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) | ||
Theorem | ssonuni 7798 | The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. Lemma 2.7 of [Schloeder] p. 4. (Contributed by NM, 1-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴 ∈ On)) | ||
Theorem | ssonunii 7799 | The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of [Enderton] p. 193. (Contributed by NM, 20-Sep-2003.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ⊆ On → ∪ 𝐴 ∈ On) | ||
Theorem | ordeleqon 7800 | A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of [TakeutiZaring] p. 38 and its converse. (Contributed by NM, 1-Jun-2003.) |
⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |