Home | Metamath
Proof Explorer Theorem List (p. 77 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elovmpt3imp 7601* | If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands must be sets. Remark: a function which is the result of an operation can be regared as operation with 3 operands - therefore the abbreviation "mpt3" is used in the label. (Contributed by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ 𝐵)) ⇒ ⊢ (𝐴 ∈ ((𝑋𝑂𝑌)‘𝑍) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | ||
Theorem | ovmpt3rab1 7602* | The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑀 = 𝐾) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑁 = 𝐿) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈) → (𝑋𝑂𝑌) = (𝑧 ∈ 𝐾 ↦ {𝑎 ∈ 𝐿 ∣ 𝜓})) | ||
Theorem | ovmpt3rabdm 7603* | If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands and the argument of the function must be sets. (Contributed by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑀 = 𝐾) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑁 = 𝐿) ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐾 ∈ 𝑈) ∧ 𝐿 ∈ 𝑇) → dom (𝑋𝑂𝑌) = 𝐾) | ||
Theorem | elovmpt3rab1 7604* | Implications for the value of an operation defined by the maps-to notation with a function into a class abstraction as a result having an element. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑀 = 𝐾) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝑁 = 𝐿) ⇒ ⊢ ((𝐾 ∈ 𝑈 ∧ 𝐿 ∈ 𝑇) → (𝐴 ∈ ((𝑋𝑂𝑌)‘𝑍) → ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑍 ∈ 𝐾 ∧ 𝐴 ∈ 𝐿)))) | ||
Theorem | elovmpt3rab 7605* | Implications for the value of an operation defined by the maps-to notation with a class abstraction as a result having an element. (Contributed by AV, 17-Jul-2018.) (Revised by AV, 16-May-2019.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑧 ∈ 𝑀 ↦ {𝑎 ∈ 𝑁 ∣ 𝜑})) ⇒ ⊢ ((𝑀 ∈ 𝑈 ∧ 𝑁 ∈ 𝑇) → (𝐴 ∈ ((𝑋𝑂𝑌)‘𝑍) → ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑍 ∈ 𝑀 ∧ 𝐴 ∈ 𝑁)))) | ||
Syntax | cof 7606 | Extend class notation to include mapping of an operation to a function operation. |
class ∘f 𝑅 | ||
Syntax | cofr 7607 | Extend class notation to include mapping of a binary relation to a function relation. |
class ∘r 𝑅 | ||
Definition | df-of 7608* | Define the function operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘f 𝑅 is the analogous operation on functions which corresponds to applying 𝑅 pointwise to the values of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ ∘f 𝑅 = (𝑓 ∈ V, 𝑔 ∈ V ↦ (𝑥 ∈ (dom 𝑓 ∩ dom 𝑔) ↦ ((𝑓‘𝑥)𝑅(𝑔‘𝑥)))) | ||
Definition | df-ofr 7609* | Define the function relation map. The definition is designed so that if 𝑅 is a binary relation, then ∘r 𝑅 is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ ∘r 𝑅 = {⟨𝑓, 𝑔⟩ ∣ ∀𝑥 ∈ (dom 𝑓 ∩ dom 𝑔)(𝑓‘𝑥)𝑅(𝑔‘𝑥)} | ||
Theorem | ofeqd 7610 | Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → ∘f 𝑅 = ∘f 𝑆) | ||
Theorem | ofeq 7611 | Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝑅 = 𝑆 → ∘f 𝑅 = ∘f 𝑆) | ||
Theorem | ofreq 7612 | Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝑅 = 𝑆 → ∘r 𝑅 = ∘r 𝑆) | ||
Theorem | ofexg 7613 | A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → ( ∘f 𝑅 ↾ 𝐴) ∈ V) | ||
Theorem | nfof 7614 | Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘f 𝑅 | ||
Theorem | nfofr 7615 | Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘r 𝑅 | ||
Theorem | ofrfvalg 7616* | Value of a relation applied to two functions. Originally part of ofrfval 7618, this version assumes the functions are sets rather than their domains, avoiding ax-rep 5241. (Contributed by SN, 5-Aug-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) | ||
Theorem | offval 7617* | Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) | ||
Theorem | ofrfval 7618* | Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) | ||
Theorem | ofval 7619 | Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) | ||
Theorem | ofrval 7620 | Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∘r 𝑅𝐺 ∧ 𝑋 ∈ 𝑆) → 𝐶𝑅𝐷) | ||
Theorem | offn 7621 | The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) Fn 𝑆) | ||
Theorem | offun 7622 | The function operation produces a function. (Contributed by SN, 23-Jul-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → Fun (𝐹 ∘f 𝑅𝐺)) | ||
Theorem | offval2f 7623* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofmresval 7624 | Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹( ∘f 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹 ∘f 𝑅𝐺)) | ||
Theorem | fnfvof 7625 | 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 7626* | The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) | ||
Theorem | ofres 7627 | 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 7628* | The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofrfval2 7629* | The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) | ||
Theorem | ofmpteq 7630* | 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 | ofco 7631 | The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐻:𝐷⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘f 𝑅(𝐺 ∘ 𝐻))) | ||
Theorem | offveq 7632* | 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 7633* | 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 7634 | Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘f 𝑅𝐹)‘𝑋) = (𝐵𝑅𝐶)) | ||
Theorem | ofc2 7635 | Right operation by a constant. (Contributed by NM, 7-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f 𝑅(𝐴 × {𝐵}))‘𝑋) = (𝐶𝑅𝐵)) | ||
Theorem | ofc12 7636 | Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) | ||
Theorem | caofref 7637* | Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘r 𝑅𝐹) | ||
Theorem | caofinvl 7638* | Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑁:𝑆⟶𝑆) & ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘f 𝑅𝐹) = (𝐴 × {𝐵})) | ||
Theorem | caofid0l 7639* | Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝑥) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = 𝐹) | ||
Theorem | caofid0r 7640* | Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝑥) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = 𝐹) | ||
Theorem | caofid1 7641* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = (𝐴 × {𝐶})) | ||
Theorem | caofid2 7642* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = (𝐴 × {𝐶})) | ||
Theorem | caofcom 7643* | Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐺 ∘f 𝑅𝐹)) | ||
Theorem | caofrss 7644* | Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 → 𝐹 ∘r 𝑇𝐺)) | ||
Theorem | caofass 7645* | Transfer an associative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦)𝑇𝑧) = (𝑥𝑂(𝑦𝑃𝑧))) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘f 𝑇𝐻) = (𝐹 ∘f 𝑂(𝐺 ∘f 𝑃𝐻))) | ||
Theorem | caoftrn 7646* | Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘r 𝑅𝐺 ∧ 𝐺 ∘r 𝑇𝐻) → 𝐹 ∘r 𝑈𝐻)) | ||
Theorem | caofdi 7647* | Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑇(𝑦𝑅𝑧)) = ((𝑥𝑇𝑦)𝑂(𝑥𝑇𝑧))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑇(𝐺 ∘f 𝑅𝐻)) = ((𝐹 ∘f 𝑇𝐺) ∘f 𝑂(𝐹 ∘f 𝑇𝐻))) | ||
Theorem | caofdir 7648* | Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝑅𝑦)𝑇𝑧) = ((𝑥𝑇𝑧)𝑂(𝑦𝑇𝑧))) ⇒ ⊢ (𝜑 → ((𝐺 ∘f 𝑅𝐻) ∘f 𝑇𝐹) = ((𝐺 ∘f 𝑇𝐹) ∘f 𝑂(𝐻 ∘f 𝑇𝐹))) | ||
Theorem | caonncan 7649* | Transfer nncan 11364-shaped laws to vectors of numbers. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴:𝐼⟶𝑆) & ⊢ (𝜑 → 𝐵:𝐼⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) ⇒ ⊢ (𝜑 → (𝐴 ∘f 𝑀(𝐴 ∘f 𝑀𝐵)) = 𝐵) | ||
Syntax | crpss 7650 | Extend class notation to include the reified proper subset relation. |
class [⊊] | ||
Definition | df-rpss 7651* | Define a relation which corresponds to proper subsethood df-pss 3928 on sets. This allows to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss 7656. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦} | ||
Theorem | relrpss 7652 | The proper subset relation is a relation. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ Rel [⊊] | ||
Theorem | brrpssg 7653 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | brrpss 7654 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵) | ||
Theorem | porpss 7655 | Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] Po 𝐴 | ||
Theorem | sorpss 7656* | 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 7657 | Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) | ||
Theorem | sorpssun 7658 | A chain of sets is closed under binary union. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∪ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssin 7659 | A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∩ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssuni 7660* | 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 7661* | 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 7662* | 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 7663* |
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 7665 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 7666. A version using class
notation is uniex 7669.
The union of a class df-uni 4865 should not be confused with the union of two classes df-un 3914. Their relationship is shown in unipr 4882. (Contributed by NM, 23-Dec-1993.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfun 7664* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) Use ax-un 7663 instead. (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axun2 7665* | A variant of the Axiom of Union ax-un 7663. 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 7666* | The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | vuniex 7667 | The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) (Revised by BJ, 6-Apr-2024.) |
⊢ ∪ 𝑥 ∈ V | ||
Theorem | uniexg 7668 | 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 7669 | The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3457), 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 7670 | Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ∪ 𝐴 ∈ V) | ||
Theorem | unex 7671 | 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 | tpex 7672 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} ∈ V | ||
Theorem | unexb 7673 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | unexg 7674 | A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | xpexg 7675 | The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7905. (Contributed by NM, 14-Aug-1994.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | xpexd 7676 | The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) | ||
Theorem | 3xpexg 7677 | The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
⊢ (𝑉 ∈ 𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V) | ||
Theorem | xpex 7678 | 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 7679 | The union of two sets is a set. (Contributed by SN, 16-Jul-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | sqxpexg 7680 | The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | ||
Theorem | abnexg 7681* | 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 7884. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 7683 and pwnex 7684 respectively, proved from abnex 7682, which is a consequence of abnexg 7681 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V)) | ||
Theorem | abnex 7682* | Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 7683 and pwnex 7684. See the comment of abnexg 7681. (Contributed by BJ, 2-May-2021.) |
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V) | ||
Theorem | snnex 7683* | The class of all singletons is a proper class. See also pwnex 7684. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V | ||
Theorem | pwnex 7684* | The class of all power sets is a proper class. See also snnex 7683. (Contributed by BJ, 2-May-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V | ||
Theorem | difex2 7685 | 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 7686 | 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 7687* | Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007.) |
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | uniexr 7688 | Converse of the Axiom of Union. Note that it does not require ax-un 7663. (Contributed by NM, 11-Nov-2003.) |
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | uniexb 7689 | 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 7690 | Converse of the Axiom of Power Sets. Note that it does not require ax-pow 5319. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝒫 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | pwexb 7691 | 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 7692 | 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 7693 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵)) | ||
Theorem | elpwun 7694 | Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐶) ∈ 𝒫 𝐵) | ||
Theorem | pwuncl 7695 | Power classes are closed under union. (Contributed by AV, 27-Feb-2024.) |
⊢ ((𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋) → (𝐴 ∪ 𝐵) ∈ 𝒫 𝑋) | ||
Theorem | iunpw 7696* | 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 7697 | 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 7698 | 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 7699* | 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 7700 | 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 7663, see epweonALT 7701. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7663. (Revised by BTernaryTau, 30-Nov-2024.) |
⊢ E We On |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |