![]() |
Metamath
Proof Explorer Theorem List (p. 95 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 | relprcnfsupp 9401 | A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍) | ||
Theorem | isfsupp 9402 | The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin))) | ||
Theorem | isfsuppd 9403 | Deduction form of isfsupp 9402. (Contributed by SN, 29-Jul-2024.) |
⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → Fun 𝑅) & ⊢ (𝜑 → (𝑅 supp 𝑍) ∈ Fin) ⇒ ⊢ (𝜑 → 𝑅 finSupp 𝑍) | ||
Theorem | funisfsupp 9404 | The property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin)) | ||
Theorem | fsuppimp 9405 | Implications of a class being a finitely supported function (in relation to a given zero). (Contributed by AV, 26-May-2019.) |
⊢ (𝑅 finSupp 𝑍 → (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)) | ||
Theorem | fsuppimpd 9406 | A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) | ||
Theorem | fsuppfund 9407 | A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | fisuppfi 9408 | A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin) | ||
Theorem | fidmfisupp 9409 | A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | finnzfsuppd 9410* | If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑥 ∈ 𝐴 ∨ (𝐹‘𝑥) = 𝑍)) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | fdmfisuppfi 9411 | The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.) |
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) | ||
Theorem | fdmfifsupp 9412 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | fsuppmptdm 9413* | A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | fndmfisuppfi 9414 | The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.) |
⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) | ||
Theorem | fndmfifsupp 9415 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | suppeqfsuppbi 9416 | If two functions have the same support, one function is finitely supported iff the other one is finitely supported. (Contributed by AV, 30-Jun-2019.) |
⊢ (((𝐹 ∈ 𝑈 ∧ Fun 𝐹) ∧ (𝐺 ∈ 𝑉 ∧ Fun 𝐺)) → ((𝐹 supp 𝑍) = (𝐺 supp 𝑍) → (𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍))) | ||
Theorem | suppssfifsupp 9417 | If the support of a function is a subset of a finite set, the function is finitely supported. (Contributed by AV, 15-Jul-2019.) |
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ∧ (𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹)) → 𝐺 finSupp 𝑍) | ||
Theorem | fsuppsssupp 9418 | If the support of a function is a subset of the support of a finitely supported function, the function is finitely supported. (Contributed by AV, 2-Jul-2019.) (Proof shortened by AV, 15-Jul-2019.) |
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐹 finSupp 𝑍 ∧ (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑍))) → 𝐺 finSupp 𝑍) | ||
Theorem | fsuppsssuppgd 9419 | If the support of a function is a subset of a finite support, it is finite. Deduction associated with fsuppsssupp 9418. (Contributed by SN, 6-Mar-2025.) |
⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐹 finSupp 𝑂) & ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑂)) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
Theorem | fsuppss 9420 | A subset of a finitely supported function is a finitely supported function. (Contributed by SN, 8-Mar-2025.) |
⊢ (𝜑 → 𝐹 ⊆ 𝐺) & ⊢ (𝜑 → 𝐺 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | fsuppssov1 9421* | Formula building theorem for finite support: operator with left annihilator. Finite support version of suppssov1 8220. (Contributed by SN, 26-Apr-2025.) |
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ 𝐴) finSupp 𝑌) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) finSupp 𝑍) | ||
Theorem | fsuppxpfi 9422 | The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.) |
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 supp 𝑍) × (𝐺 supp 𝑍)) ∈ Fin) | ||
Theorem | fczfsuppd 9423 | A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐵 × {𝑍}) finSupp 𝑍) | ||
Theorem | fsuppun 9424 | The union of two finitely supported functions is finitely supported (but not necessarily a function!). (Contributed by AV, 3-Jun-2019.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → 𝐺 finSupp 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∪ 𝐺) supp 𝑍) ∈ Fin) | ||
Theorem | fsuppunfi 9425 | The union of the support of two finitely supported functions is finite. (Contributed by AV, 1-Jul-2019.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → 𝐺 finSupp 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍)) ∈ Fin) | ||
Theorem | fsuppunbi 9426 | If the union of two classes/functions is a function, this union is finitely supported iff the two functions are finitely supported. (Contributed by AV, 18-Jun-2019.) |
⊢ (𝜑 → Fun (𝐹 ∪ 𝐺)) ⇒ ⊢ (𝜑 → ((𝐹 ∪ 𝐺) finSupp 𝑍 ↔ (𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍))) | ||
Theorem | 0fsupp 9427 | The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
⊢ (𝑍 ∈ 𝑉 → ∅ finSupp 𝑍) | ||
Theorem | snopfsupp 9428 | A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉} finSupp 𝑍) | ||
Theorem | funsnfsupp 9429 | Finite support for a function extended by a singleton. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by AV, 19-Jul-2019.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) ∧ (Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹)) → ((𝐹 ∪ {〈𝑋, 𝑌〉}) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍)) | ||
Theorem | fsuppres 9430 | The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍) | ||
Theorem | fmptssfisupp 9431* | The restriction of a mapping function has finite support if that function has finite support. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) finSupp 𝑍) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐵) finSupp 𝑍) | ||
Theorem | ressuppfi 9432 | If the support of the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finite, the support of the function itself is finite. (Contributed by AV, 22-Apr-2019.) |
⊢ (𝜑 → (dom 𝐹 ∖ 𝐵) ∈ Fin) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ (𝜑 → 𝐺 = (𝐹 ↾ 𝐵)) & ⊢ (𝜑 → (𝐺 supp 𝑍) ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) | ||
Theorem | resfsupp 9433 | If the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finitely supported, the function itself is finitely supported. (Contributed by AV, 27-May-2019.) |
⊢ (𝜑 → (dom 𝐹 ∖ 𝐵) ∈ Fin) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝐺 = (𝐹 ↾ 𝐵)) & ⊢ (𝜑 → 𝐺 finSupp 𝑍) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | resfifsupp 9434 | The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍) | ||
Theorem | ffsuppbi 9435 | Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.) |
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 finSupp 𝑍 ↔ (◡𝐹 “ (𝑆 ∖ {𝑍})) ∈ Fin))) | ||
Theorem | fsuppmptif 9436* | A function mapping an argument to either a value of a finitely supported function or zero is finitely supported. (Contributed by AV, 6-Jun-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 𝑍)) finSupp 𝑍) | ||
Theorem | sniffsupp 9437* | A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 0 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑋, 𝐴, 0 )) ⇒ ⊢ (𝜑 → 𝐹 finSupp 0 ) | ||
Theorem | fsuppcolem 9438 | Lemma for fsuppco 9439. Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ (𝜑 → (◡𝐹 “ (V ∖ {𝑍})) ∈ Fin) & ⊢ (𝜑 → 𝐺:𝑋–1-1→𝑌) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) ∈ Fin) | ||
Theorem | fsuppco 9439 | The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → 𝐺:𝑋–1-1→𝑌) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) finSupp 𝑍) | ||
Theorem | fsuppco2 9440 | The composition of a function which maps the zero to zero with a finitely supported function is finitely supported. This is not only a special case of fsuppcor 9441 because it does not require that the "zero" is an element of the range of the finitely supported function. (Contributed by AV, 6-Jun-2019.) |
⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → (𝐺‘𝑍) = 𝑍) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) finSupp 𝑍) | ||
Theorem | fsuppcor 9441 | The composition of a function which maps the zero of the range of a finitely supported function to the zero of its range with this finitely supported function is finitely supported. (Contributed by AV, 6-Jun-2019.) |
⊢ (𝜑 → 0 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐷) & ⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → (𝐺‘𝑍) = 0 ) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) finSupp 0 ) | ||
Theorem | mapfienlem1 9442* | Lemma 1 for mapfien 9445. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊) | ||
Theorem | mapfienlem2 9443* | Lemma 2 for mapfien 9445. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) finSupp 𝑍) | ||
Theorem | mapfienlem3 9444* | Lemma 3 for mapfien 9445. (Contributed by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆) | ||
Theorem | mapfien 9445* | A bijection of the base sets induces a bijection on the set of finitely supported functions. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.) (Revised by AV, 28-Jul-2024.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇) | ||
Theorem | mapfien2 9446* | Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 0 } & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ (𝜑 → 𝐴 ≈ 𝐶) & ⊢ (𝜑 → 𝐵 ≈ 𝐷) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Syntax | cfi 9447 | Extend class notation with the function whose value is the class of finite intersections of the elements of a given set. |
class fi | ||
Definition | df-fi 9448* | Function whose value is the class of finite intersections of the elements of the argument. Note that the empty intersection being the universal class, hence a proper class, it cannot be an element of that class. Therefore, the function value is the class of nonempty finite intersections of elements of the argument (see elfi2 9451). (Contributed by FL, 27-Apr-2008.) |
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) | ||
Theorem | fival 9449* | The set of all the finite intersections of the elements of 𝐴. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) | ||
Theorem | elfi 9450* | Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) | ||
Theorem | elfi2 9451* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥)) | ||
Theorem | elfir 9452 | Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵)) | ||
Theorem | intrnfi 9453 | Sufficient condition for the intersection of the range of a function to be in the set of finite intersections. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ ran 𝐹 ∈ (fi‘𝐵)) | ||
Theorem | iinfi 9454* | An indexed intersection of elements of 𝐶 is an element of the finite intersections of 𝐶. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ (fi‘𝐶)) | ||
Theorem | inelfi 9455 | The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∩ 𝐵) ∈ (fi‘𝑋)) | ||
Theorem | ssfii 9456 | Any element of a set 𝐴 is the intersection of a finite subset of 𝐴. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴)) | ||
Theorem | fi0 9457 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘∅) = ∅ | ||
Theorem | fieq0 9458 | A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ∅ ↔ (fi‘𝐴) = ∅)) | ||
Theorem | fiin 9459 | The elements of (fi‘𝐶) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐴 ∩ 𝐵) ∈ (fi‘𝐶)) | ||
Theorem | dffi2 9460* | The set of finite intersections is the smallest set that contains 𝐴 and is closed under pairwise intersection. (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}) | ||
Theorem | fiss 9461 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵)) | ||
Theorem | inficl 9462* | A set which is closed under pairwise intersection is closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴)) | ||
Theorem | fipwuni 9463 | The set of finite intersections of a set is contained in the powerset of the union of the elements of 𝐴. (Contributed by Mario Carneiro, 24-Nov-2013.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ (fi‘𝐴) ⊆ 𝒫 ∪ 𝐴 | ||
Theorem | fisn 9464 | A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (fi‘{𝐴}) = {𝐴} | ||
Theorem | fiuni 9465 | The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 = ∪ (fi‘𝐴)) | ||
Theorem | fipwss 9466 | If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐴 ⊆ 𝒫 𝑋 → (fi‘𝐴) ⊆ 𝒫 𝑋) | ||
Theorem | elfiun 9467* | A finite intersection of elements taken from a union of collections. (Contributed by Jeff Hankins, 15-Nov-2009.) (Proof shortened by Mario Carneiro, 26-Nov-2013.) |
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐾) → (𝐴 ∈ (fi‘(𝐵 ∪ 𝐶)) ↔ (𝐴 ∈ (fi‘𝐵) ∨ 𝐴 ∈ (fi‘𝐶) ∨ ∃𝑥 ∈ (fi‘𝐵)∃𝑦 ∈ (fi‘𝐶)𝐴 = (𝑥 ∩ 𝑦)))) | ||
Theorem | dffi3 9468* | The set of finite intersections can be "constructed" inductively by iterating binary intersection ω-many times. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑅 = (𝑢 ∈ V ↦ ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧))) ⇒ ⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∪ (rec(𝑅, 𝐴) “ ω)) | ||
Theorem | fifo 9469* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) | ||
Theorem | marypha1lem 9470* | Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))) | ||
Theorem | marypha1 9471* | (Philip) Hall's marriage theorem, sufficiency: a finite relation contains an injection if there is no subset of its domain which would be forced to violate the pigeonhole principle. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ⊆ (𝐴 × 𝐵)) & ⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ (𝐶 “ 𝑑)) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ 𝒫 𝐶𝑓:𝐴–1-1→𝐵) | ||
Theorem | marypha2lem1 9472* | Lemma for marypha2 9476. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 ⊆ (𝐴 × ∪ ran 𝐹) | ||
Theorem | marypha2lem2 9473* | Lemma for marypha2 9476. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} | ||
Theorem | marypha2lem3 9474* | Lemma for marypha2 9476. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐺 ⊆ 𝑇 ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹‘𝑥))) | ||
Theorem | marypha2lem4 9475* | Lemma for marypha2 9476. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → (𝑇 “ 𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | marypha2 9476* | Version of marypha1 9471 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶Fin) & ⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ ∪ (𝐹 “ 𝑑)) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) | ||
Syntax | csup 9477 | Extend class notation to include supremum of class 𝐴. Here 𝑅 is ordinarily a relation that strictly orders class 𝐵. For example, 𝑅 could be 'less than' and 𝐵 could be the set of real numbers. |
class sup(𝐴, 𝐵, 𝑅) | ||
Syntax | cinf 9478 | Extend class notation to include infimum of class 𝐴. Here 𝑅 is ordinarily a relation that strictly orders class 𝐵. For example, 𝑅 could be 'less than' and 𝐵 could be the set of real numbers. |
class inf(𝐴, 𝐵, 𝑅) | ||
Definition | df-sup 9479* | Define the supremum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the supremum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrtval 15272. See dfsup2 9481 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.) |
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} | ||
Definition | df-inf 9480 | Define the infimum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the infimum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals; in this case the infimum is 0. The infimum is defined as the supremum using the converse ordering relation. In the given example, 0 is the supremum of all reals (greatest real number) for which all positive reals are greater. (Contributed by AV, 2-Sep-2020.) |
⊢ inf(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, ◡𝑅) | ||
Theorem | dfsup2 9481 | Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ sup(𝐵, 𝐴, 𝑅) = ∪ (𝐴 ∖ ((◡𝑅 “ 𝐵) ∪ (𝑅 “ (𝐴 ∖ (◡𝑅 “ 𝐵))))) | ||
Theorem | supeq1 9482 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1d 9483 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1i 9484 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) | ||
Theorem | supeq2 9485 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅)) | ||
Theorem | supeq3 9486 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆)) | ||
Theorem | supeq123d 9487 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfsup 9488 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅) | ||
Theorem | supmo 9489* | Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by NM, 5-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | supexd 9490 | A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | supeu 9491* | A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by NM, 12-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | supval2 9492* | Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))) | ||
Theorem | eqsup 9493* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqsupd 9494* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | supcl 9495* | A supremum belongs to its base class (closure law). See also supub 9496 and suplub 9497. (Contributed by NM, 12-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supub 9496* |
A supremum is an upper bound. See also supcl 9495 and suplub 9497.
This proof demonstrates how to expand an iota-based definition (df-iota 6515) using riotacl2 7403. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | suplub 9497* | A supremum is the least upper bound. See also supcl 9495 and supub 9496. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | suplub2 9498* | Bidirectional form of suplub 9497. (Contributed by Mario Carneiro, 6-Sep-2014.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | supnub 9499* | An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅))) | ||
Theorem | supex 9500 | A supremum is a set. (Contributed by NM, 22-May-1999.) |
⊢ 𝑅 Or 𝐴 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |