Home | Metamath
Proof Explorer Theorem List (p. 75 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ofreq 7401 | Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝑅 = 𝑆 → ∘r 𝑅 = ∘r 𝑆) | ||
Theorem | ofexg 7402 | A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → ( ∘f 𝑅 ↾ 𝐴) ∈ V) | ||
Theorem | nfof 7403 | Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘f 𝑅 | ||
Theorem | nfofr 7404 | Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥 ∘r 𝑅 | ||
Theorem | offval 7405* | Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ (𝐶𝑅𝐷))) | ||
Theorem | ofrfval 7406* | Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = 𝐷) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝑆 𝐶𝑅𝐷)) | ||
Theorem | ofval 7407 | Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) | ||
Theorem | ofrval 7408 | Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∘r 𝑅𝐺 ∧ 𝑋 ∈ 𝑆) → 𝐶𝑅𝐷) | ||
Theorem | offn 7409 | The function operation produces a function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝑆 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) Fn 𝑆) | ||
Theorem | offval2f 7410* | The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofmresval 7411 | Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.) |
⊢ (𝜑 → 𝐹 ∈ 𝐴) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹( ∘f 𝑅 ↾ (𝐴 × 𝐵))𝐺) = (𝐹 ∘f 𝑅𝐺)) | ||
Theorem | fnfvof 7412 | 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 7413* | The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) | ||
Theorem | ofres 7414 | 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 7415* | The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴 ↦ (𝐵𝑅𝐶))) | ||
Theorem | ofrfval2 7416* | The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)) & ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐶)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 ↔ ∀𝑥 ∈ 𝐴 𝐵𝑅𝐶)) | ||
Theorem | ofmpteq 7417* | 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 7418 | The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐻:𝐷⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝐴 ∩ 𝐵) = 𝐶 ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘ 𝐻) = ((𝐹 ∘ 𝐻) ∘f 𝑅(𝐺 ∘ 𝐻))) | ||
Theorem | offveq 7419* | 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 7420* | 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 7421 | Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (((𝐴 × {𝐵}) ∘f 𝑅𝐹)‘𝑋) = (𝐵𝑅𝐶)) | ||
Theorem | ofc2 7422 | Right operation by a constant. (Contributed by NM, 7-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘f 𝑅(𝐴 × {𝐵}))‘𝑋) = (𝐶𝑅𝐵)) | ||
Theorem | ofc12 7423 | Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅(𝐴 × {𝐶})) = (𝐴 × {(𝐵𝑅𝐶)})) | ||
Theorem | caofref 7424* | Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥𝑅𝑥) ⇒ ⊢ (𝜑 → 𝐹 ∘r 𝑅𝐹) | ||
Theorem | caofinvl 7425* | Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑁:𝑆⟶𝑆) & ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐴 ↦ (𝑁‘(𝐹‘𝑣)))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑁‘𝑥)𝑅𝑥) = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∘f 𝑅𝐹) = (𝐴 × {𝐵})) | ||
Theorem | caofid0l 7426* | Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝑥) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = 𝐹) | ||
Theorem | caofid0r 7427* | Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝑥) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = 𝐹) | ||
Theorem | caofid1 7428* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥𝑅𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅(𝐴 × {𝐵})) = (𝐴 × {𝐶})) | ||
Theorem | caofid2 7429* | Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐵𝑅𝑥) = 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f 𝑅𝐹) = (𝐴 × {𝐶})) | ||
Theorem | caofcom 7430* | Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦) = (𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝐺 ∘f 𝑅𝐹)) | ||
Theorem | caofrss 7431* | Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑅𝑦 → 𝑥𝑇𝑦)) ⇒ ⊢ (𝜑 → (𝐹 ∘r 𝑅𝐺 → 𝐹 ∘r 𝑇𝐺)) | ||
Theorem | caofass 7432* | Transfer an associative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦)𝑇𝑧) = (𝑥𝑂(𝑦𝑃𝑧))) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺) ∘f 𝑇𝐻) = (𝐹 ∘f 𝑂(𝐺 ∘f 𝑃𝐻))) | ||
Theorem | caoftrn 7433* | Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑇𝑧) → 𝑥𝑈𝑧)) ⇒ ⊢ (𝜑 → ((𝐹 ∘r 𝑅𝐺 ∧ 𝐺 ∘r 𝑇𝐻) → 𝐹 ∘r 𝑈𝐻)) | ||
Theorem | caofdi 7434* | Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑇(𝑦𝑅𝑧)) = ((𝑥𝑇𝑦)𝑂(𝑥𝑇𝑧))) ⇒ ⊢ (𝜑 → (𝐹 ∘f 𝑇(𝐺 ∘f 𝑅𝐻)) = ((𝐹 ∘f 𝑇𝐺) ∘f 𝑂(𝐹 ∘f 𝑇𝐻))) | ||
Theorem | caofdir 7435* | Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐾) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝐾)) → ((𝑥𝑅𝑦)𝑇𝑧) = ((𝑥𝑇𝑧)𝑂(𝑦𝑇𝑧))) ⇒ ⊢ (𝜑 → ((𝐺 ∘f 𝑅𝐻) ∘f 𝑇𝐹) = ((𝐺 ∘f 𝑇𝐹) ∘f 𝑂(𝐻 ∘f 𝑇𝐹))) | ||
Theorem | caonncan 7436* | Transfer nncan 10904-shaped laws to vectors of numbers. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴:𝐼⟶𝑆) & ⊢ (𝜑 → 𝐵:𝐼⟶𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) ⇒ ⊢ (𝜑 → (𝐴 ∘f 𝑀(𝐴 ∘f 𝑀𝐵)) = 𝐵) | ||
Syntax | crpss 7437 | Extend class notation to include the reified proper subset relation. |
class [⊊] | ||
Definition | df-rpss 7438* | Define a relation which corresponds to proper subsethood df-pss 3953 on sets. This allows us to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss 7443. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] = {〈𝑥, 𝑦〉 ∣ 𝑥 ⊊ 𝑦} | ||
Theorem | relrpss 7439 | The proper subset relation is a relation. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ Rel [⊊] | ||
Theorem | brrpssg 7440 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵)) | ||
Theorem | brrpss 7441 | The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵) | ||
Theorem | porpss 7442 | Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ [⊊] Po 𝐴 | ||
Theorem | sorpss 7443* | 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 7444 | Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) | ||
Theorem | sorpssun 7445 | A chain of sets is closed under binary union. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∪ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssin 7446 | A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015.) |
⊢ (( [⊊] Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ∩ 𝐶) ∈ 𝐴) | ||
Theorem | sorpssuni 7447* | 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 7448* | 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 7449* | 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 7450* |
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 7452 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 7453. A version using class
notation is uniex 7454.
The union of a class df-uni 4833 should not be confused with the union of two classes df-un 3940. Their relationship is shown in unipr 4845. (Contributed by NM, 23-Dec-1993.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfun 7451* | Axiom of Union expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axun2 7452* | A variant of the Axiom of Union ax-un 7450. 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 7453* | The Axiom of Union using the standard abbreviation for union. Given any set 𝑥, its union 𝑦 exists. (Contributed by NM, 4-Jun-2006.) |
⊢ ∃𝑦 𝑦 = ∪ 𝑥 | ||
Theorem | uniex 7454 | The Axiom of Union in class notation. This says that if 𝐴 is a set i.e. 𝐴 ∈ V (see isset 3507), 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 | vuniex 7455 | The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) |
⊢ ∪ 𝑥 ∈ V | ||
Theorem | uniexg 7456 | 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 | unex 7457 | 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 7458 | An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.) |
⊢ {𝐴, 𝐵, 𝐶} ∈ V | ||
Theorem | unexb 7459 | Existence of union is equivalent to existence of its components. (Contributed by NM, 11-Jun-1998.) |
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | unexg 7460 | A union of two sets is a set. Corollary 5.8 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Sep-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
Theorem | xpexg 7461 | The Cartesian product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. See also xpexgALT 7673. (Contributed by NM, 14-Aug-1994.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) | ||
Theorem | xpexd 7462 | The Cartesian product of two sets is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) | ||
Theorem | 3xpexg 7463 | The Cartesian product of three sets is a set. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
⊢ (𝑉 ∈ 𝑊 → ((𝑉 × 𝑉) × 𝑉) ∈ V) | ||
Theorem | xpex 7464 | 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 | sqxpexg 7465 | The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V) | ||
Theorem | abnexg 7466* | 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 7653. Note that the second antecedent ∀𝑥 ∈ 𝐴𝑥 ∈ 𝐹 cannot be translated to 𝐴 ⊆ 𝐹 since 𝐹 may depend on 𝑥. In applications, one may take 𝐹 = {𝑥} or 𝐹 = 𝒫 𝑥 (see snnex 7468 and pwnex 7469 respectively, proved from abnex 7467, which is a consequence of abnexg 7466 with 𝐴 = V). (Contributed by BJ, 2-Dec-2021.) |
⊢ (∀𝑥 ∈ 𝐴 (𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐹} ∈ 𝑊 → 𝐴 ∈ V)) | ||
Theorem | abnex 7467* | Sufficient condition for a class abstraction to be a proper class. Lemma for snnex 7468 and pwnex 7469. See the comment of abnexg 7466. (Contributed by BJ, 2-May-2021.) |
⊢ (∀𝑥(𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹) → ¬ {𝑦 ∣ ∃𝑥 𝑦 = 𝐹} ∈ V) | ||
Theorem | snnex 7468* | The class of all singletons is a proper class. See also pwnex 7469. (Contributed by NM, 10-Oct-2008.) (Proof shortened by Eric Schmidt, 7-Dec-2008.) (Proof shortened by BJ, 5-Dec-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V | ||
Theorem | pwnex 7469* | The class of all power sets is a proper class. See also snnex 7468. (Contributed by BJ, 2-May-2021.) |
⊢ {𝑥 ∣ ∃𝑦 𝑥 = 𝒫 𝑦} ∉ V | ||
Theorem | difex2 7470 | 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 7471 | 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 7472* | Expression for double union that moves union into a class builder. (Contributed by FL, 28-May-2007.) |
⊢ ∪ ∪ 𝐴 = ∪ {𝑥 ∣ ∃𝑦(𝑥 = ∪ 𝑦 ∧ 𝑦 ∈ 𝐴)} | ||
Theorem | uniexr 7473 | Converse of the Axiom of Union. Note that it does not require ax-un 7450. (Contributed by NM, 11-Nov-2003.) |
⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | uniexb 7474 | 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 7475 | Converse of the Axiom of Power Sets. Note that it does not require ax-pow 5258. (Contributed by NM, 11-Nov-2003.) |
⊢ (𝒫 𝐴 ∈ 𝑉 → 𝐴 ∈ V) | ||
Theorem | pwexb 7476 | 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 7477 | 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 7478 | Membership in a power class difference. (Contributed by NM, 25-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵) → (𝐴 ∪ 𝐶) ∈ (𝒫 (𝐵 ∪ 𝐶) ∖ 𝒫 𝐵)) | ||
Theorem | elpwun 7479 | Membership in the power class of a union. (Contributed by NM, 26-Mar-2007.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ∈ 𝒫 (𝐵 ∪ 𝐶) ↔ (𝐴 ∖ 𝐶) ∈ 𝒫 𝐵) | ||
Theorem | pwuncl 7480 | Power classes are closed under union. (Contributed by AV, 27-Feb-2024.) |
⊢ ((𝐴 ∈ 𝒫 𝑋 ∧ 𝐵 ∈ 𝒫 𝑋) → (𝐴 ∪ 𝐵) ∈ 𝒫 𝑋) | ||
Theorem | iunpw 7481* | 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 7482 | 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 7483 | 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 7484* | 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 7485 | 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. (Contributed by NM, 1-Nov-2003.) |
⊢ E We On | ||
Theorem | ordon 7486 | 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 7487 | 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 7486), 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 7488 | The union of a class of ordinal numbers is ordinal. Proposition 7.19 of [TakeutiZaring] p. 40. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) | ||
Theorem | ssonuni 7489 | The union of a set of ordinal numbers is an ordinal number. Theorem 9 of [Suppes] p. 132. (Contributed by NM, 1-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊆ On → ∪ 𝐴 ∈ On)) | ||
Theorem | ssonunii 7490 | 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 7491 | 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)) | ||
Theorem | ordsson 7492 | Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
⊢ (Ord 𝐴 → 𝐴 ⊆ On) | ||
Theorem | onss 7493 | An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | ||
Theorem | predon 7494 | The predecessor of an ordinal under E and On is itself. (Contributed by Scott Fenton, 27-Mar-2011.) |
⊢ (𝐴 ∈ On → Pred( E , On, 𝐴) = 𝐴) | ||
Theorem | ssonprc 7495 | Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013.) |
⊢ (𝐴 ⊆ On → (𝐴 ∉ V ↔ ∪ 𝐴 = On)) | ||
Theorem | onuni 7496 | The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On) | ||
Theorem | orduni 7497 | The union of an ordinal class is ordinal. (Contributed by NM, 12-Sep-2003.) |
⊢ (Ord 𝐴 → Ord ∪ 𝐴) | ||
Theorem | onint 7498 | The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ 𝐴) | ||
Theorem | onint0 7499 | The intersection of a class of ordinal numbers is zero iff the class contains zero. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ⊆ On → (∩ 𝐴 = ∅ ↔ ∅ ∈ 𝐴)) | ||
Theorem | onssmin 7500* | A nonempty class of ordinal numbers has the smallest member. Exercise 9 of [TakeutiZaring] p. 40. (Contributed by NM, 3-Oct-2003.) |
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |