![]() |
Metamath
Proof Explorer Theorem List (p. 302 of 445) | < 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-28391) |
![]() (28392-29914) |
![]() (29915-44437) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | acunirnmpt2f 30101* | Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ Ⅎ𝑗𝐶 & ⊢ Ⅎ𝑗𝐷 & ⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵 & ⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) | ||
Theorem | aciunf1lem 30102* | Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) & ⊢ Ⅎ𝑗𝐴 & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑥)) = 𝑥)) | ||
Theorem | aciunf1 30103* | Choice in an index union. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑘)) = 𝑘)) | ||
Theorem | ofoprabco 30104* | Function operation as a composition with an operation. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ Ⅎ𝑎𝑀 & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 = (𝑎 ∈ 𝐴 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)) & ⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑁 ∘ 𝑀)) | ||
Theorem | ofpreima 30105* | Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
Theorem | ofpreima2 30106* | Express the preimage of a function operation as a union of preimages. This version of ofpreima 30105 iterates the union over a smaller set. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) ⇒ ⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ∪ 𝑝 ∈ ((◡𝑅 “ 𝐷) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) | ||
Theorem | funcnvmpt 30107* | Condition for a function in maps-to notation to be single-rooted. (Contributed by Thierry Arnoux, 28-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) | ||
Theorem | funcnv5mpt 30108* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 1-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) & ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥 = 𝑧 ∨ 𝐵 ≠ 𝐶))) | ||
Theorem | funcnv4mpt 30109* | Two ways to say that a function in maps-to notation is single-rooted. (Contributed by Thierry Arnoux, 2-Mar-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑖 ∈ 𝐴 ∀𝑗 ∈ 𝐴 (𝑖 = 𝑗 ∨ ⦋𝑖 / 𝑥⦌𝐵 ≠ ⦋𝑗 / 𝑥⦌𝐵))) | ||
Theorem | preimane 30110 | Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐹) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐹) ⇒ ⊢ (𝜑 → (◡𝐹 “ {𝑋}) ≠ (◡𝐹 “ {𝑌})) | ||
Theorem | fnpreimac 30111* | Choose a set 𝑥 containing a preimage of each element of a given set 𝐵. (Contributed by Thierry Arnoux, 7-May-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) | ||
Theorem | fgreu 30112* | Exactly one point of a function's graph has a given first element. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∃!𝑝 ∈ 𝐹 𝑋 = (1st ‘𝑝)) | ||
Theorem | fcnvgreu 30113* | If the converse of a relation 𝐴 is a function, exactly one point of its graph has a given second element (that is, function value). (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ (((Rel 𝐴 ∧ Fun ◡𝐴) ∧ 𝑌 ∈ ran 𝐴) → ∃!𝑝 ∈ 𝐴 𝑌 = (2nd ‘𝑝)) | ||
Theorem | rnmposs 30114* | The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 → ran 𝐹 ⊆ 𝐷) | ||
Theorem | mptssALT 30115* | Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss 5796. (Contributed by Thierry Arnoux, 30-May-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) ⊆ (𝑥 ∈ 𝐵 ↦ 𝐶)) | ||
Theorem | partfun 30116 | Rewrite a function defined by parts, using a mapping and an if construct, into a union of functions on disjoint domains. (Contributed by Thierry Arnoux, 30-Mar-2017.) |
⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 ∈ 𝐵, 𝐶, 𝐷)) = ((𝑥 ∈ (𝐴 ∩ 𝐵) ↦ 𝐶) ∪ (𝑥 ∈ (𝐴 ∖ 𝐵) ↦ 𝐷)) | ||
Theorem | dfcnv2 30117* | Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018.) |
⊢ (ran 𝑅 ⊆ 𝐴 → ◡𝑅 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (◡𝑅 “ {𝑥}))) | ||
Theorem | fnimatp 30118 | The image of a triplet under a function. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝐴 ∈ 𝐷) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 “ {𝐴, 𝐵, 𝐶}) = {(𝐹‘𝐴), (𝐹‘𝐵), (𝐹‘𝐶)}) | ||
Theorem | fnunres2 30119 | Restriction of a disjoint union to the domain of the second function. (Contributed by Thierry Arnoux, 12-Oct-2023.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺) | ||
Theorem | mpomptxf 30120* | Express a two-argument function as a one-argument function, or vice-versa. In this version 𝐵(𝑥) is not assumed to be constant w.r.t 𝑥. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Thierry Arnoux, 31-Mar-2018.) |
⊢ Ⅎ𝑥𝐶 & ⊢ Ⅎ𝑦𝐶 & ⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝐶 = 𝐷) ⇒ ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) | ||
Theorem | suppovss 30121* | A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑦 ∈ 𝐵 ↦ 𝐶)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑍 ∈ 𝐷) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐷) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐺 supp (𝐵 × {𝑍})) × ∪ 𝑘 ∈ (𝐺 supp (𝐵 × {𝑍}))((𝐺‘𝑘) supp 𝑍))) | ||
Theorem | brsnop 30122 | Binary relation for an ordered pair singleton. (Contributed by Thierry Arnoux, 23-Sep-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑋{〈𝐴, 𝐵〉}𝑌 ↔ (𝑋 = 𝐴 ∧ 𝑌 = 𝐵))) | ||
Theorem | cosnopne 30123 | Composition of two ordered pair singletons with non-matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → ({〈𝐴, 𝐵〉} ∘ {〈𝐶, 𝐷〉}) = ∅) | ||
Theorem | cosnop 30124 | Composition of two ordered pair singletons with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → ({〈𝐴, 𝐵〉} ∘ {〈𝐶, 𝐴〉}) = {〈𝐶, 𝐵〉}) | ||
Theorem | cnvprop 30125 | Converse of a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {〈𝐵, 𝐴〉, 〈𝐷, 𝐶〉}) | ||
Theorem | brprop 30126 | Binary relation for a pair of ordered pairs. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}𝑌 ↔ ((𝑋 = 𝐴 ∧ 𝑌 = 𝐵) ∨ (𝑋 = 𝐶 ∧ 𝑌 = 𝐷)))) | ||
Theorem | mptprop 30127* | Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷))) | ||
Theorem | coprprop 30128 | Composition of two pairs of ordered pairs with matching domain and range. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ≠ 𝐹) ⇒ ⊢ (𝜑 → ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∘ {〈𝐸, 𝐴〉, 〈𝐹, 𝐶〉}) = {〈𝐸, 𝐵〉, 〈𝐹, 𝐷〉}) | ||
Theorem | gtiso 30129 | Two ways to write a strictly decreasing function on the reals. (Contributed by Thierry Arnoux, 6-Apr-2017.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐵 ⊆ ℝ*) → (𝐹 Isom < , ◡ < (𝐴, 𝐵) ↔ 𝐹 Isom ≤ , ◡ ≤ (𝐴, 𝐵))) | ||
Theorem | isoun 30130* | Infer an isomorphism from a union of two isomorphisms. (Contributed by Thierry Arnoux, 30-Mar-2017.) |
⊢ (𝜑 → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) → 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷) → 𝑧𝑆𝑤) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑥𝑅𝑦) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐵) → ¬ 𝑧𝑆𝑤) & ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) & ⊢ (𝜑 → (𝐵 ∩ 𝐷) = ∅) ⇒ ⊢ (𝜑 → (𝐻 ∪ 𝐺) Isom 𝑅, 𝑆 ((𝐴 ∪ 𝐶), (𝐵 ∪ 𝐷))) | ||
Theorem | disjdsct 30131* | A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv 6298) (Contributed by Thierry Arnoux, 28-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝐴 & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ (𝑉 ∖ {∅})) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) ⇒ ⊢ (𝜑 → Fun ◡(𝑥 ∈ 𝐴 ↦ 𝐵)) | ||
Theorem | df1stres 30132* | Definition for a restriction of the 1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (1st ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑥) | ||
Theorem | df2ndres 30133* | Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑦) | ||
Theorem | 1stpreimas 30134 | The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
⊢ ((Rel 𝐴 ∧ 𝑋 ∈ 𝑉) → (◡(1st ↾ 𝐴) “ {𝑋}) = ({𝑋} × (𝐴 “ {𝑋}))) | ||
Theorem | 1stpreima 30135 | The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
⊢ (𝐴 ⊆ 𝐵 → (◡(1st ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐴 × 𝐶)) | ||
Theorem | 2ndpreima 30136 | The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
⊢ (𝐴 ⊆ 𝐶 → (◡(2nd ↾ (𝐵 × 𝐶)) “ 𝐴) = (𝐵 × 𝐴)) | ||
Theorem | curry2ima 30137* | The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
⊢ 𝐺 = (𝐹 ∘ ◡(1st ↾ (V × {𝐶}))) ⇒ ⊢ ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴) → (𝐺 “ 𝐷) = {𝑦 ∣ ∃𝑥 ∈ 𝐷 𝑦 = (𝑥𝐹𝐶)}) | ||
Theorem | supssd 30138* | Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ¬ sup(𝐶, 𝐴, 𝑅)𝑅sup(𝐵, 𝐴, 𝑅)) | ||
Theorem | infssd 30139* | Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ¬ inf(𝐶, 𝐴, 𝑅)𝑅inf(𝐵, 𝐴, 𝑅)) | ||
Theorem | imafi2 30140 | The image by a finite set is finite. See also imafi 8668. (Contributed by Thierry Arnoux, 25-Apr-2020.) |
⊢ (𝐴 ∈ Fin → (𝐴 “ 𝐵) ∈ Fin) | ||
Theorem | unifi3 30141 | If a union is finite, then all its elements are finite. See unifi 8664. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
⊢ (∪ 𝐴 ∈ Fin → 𝐴 ⊆ Fin) | ||
Theorem | snct 30142 | A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≼ ω) | ||
Theorem | prct 30143 | An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ≼ ω) | ||
Theorem | mpocti 30144* | An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 ⇒ ⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
Theorem | abrexct 30145* | An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | ||
Theorem | mptctf 30146 | A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≼ ω → (𝑥 ∈ 𝐴 ↦ 𝐵) ≼ ω) | ||
Theorem | abrexctf 30147* | An image set of a countable set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω) | ||
Theorem | padct 30148* | Index a countable set with integers and pad with 𝑍. (Contributed by Thierry Arnoux, 1-Jun-2020.) |
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) | ||
Theorem | cnvoprabOLD 30149* | The converse of a class abstraction of nested ordered pairs. Obsolete version of cnvoprab 7619 as of 16-Oct-2022, which has nonfreeness hypotheses instead of disjoint variable conditions. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑎 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜑)) & ⊢ (𝜓 → 𝑎 ∈ (V × V)) ⇒ ⊢ ◡{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} = {〈𝑧, 𝑎〉 ∣ 𝜓} | ||
Theorem | f1od2 30150* | Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by Thierry Arnoux, 17-Aug-2017.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐷) → (𝐼 ∈ 𝑋 ∧ 𝐽 ∈ 𝑌)) & ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ (𝑧 ∈ 𝐷 ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)))) ⇒ ⊢ (𝜑 → 𝐹:(𝐴 × 𝐵)–1-1-onto→𝐷) | ||
Theorem | fcobij 30151* | Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017.) |
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑓 ∈ (𝑆 ↑𝑚 𝑅) ↦ (𝐺 ∘ 𝑓)):(𝑆 ↑𝑚 𝑅)–1-1-onto→(𝑇 ↑𝑚 𝑅)) | ||
Theorem | fcobijfs 30152* | Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 8722. (Contributed by Thierry Arnoux, 25-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ (𝜑 → 𝐺:𝑆–1-1-onto→𝑇) & ⊢ (𝜑 → 𝑅 ∈ 𝑈) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ 𝑊) & ⊢ (𝜑 → 𝑂 ∈ 𝑆) & ⊢ 𝑄 = (𝐺‘𝑂) & ⊢ 𝑋 = {𝑔 ∈ (𝑆 ↑𝑚 𝑅) ∣ 𝑔 finSupp 𝑂} & ⊢ 𝑌 = {ℎ ∈ (𝑇 ↑𝑚 𝑅) ∣ ℎ finSupp 𝑄} ⇒ ⊢ (𝜑 → (𝑓 ∈ 𝑋 ↦ (𝐺 ∘ 𝑓)):𝑋–1-1-onto→𝑌) | ||
Theorem | suppss3 30153* | Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑍) → 𝐵 = 𝑍) ⇒ ⊢ (𝜑 → (𝐺 supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | fsuppcurry1 30154* | Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
⊢ 𝐺 = (𝑥 ∈ 𝐵 ↦ (𝐶𝐹𝑥)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
Theorem | fsuppcurry2 30155* | Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝑥𝐹𝐶)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 Fn (𝐴 × 𝐵)) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → 𝐺 finSupp 𝑍) | ||
Theorem | offinsupp1 30156* | Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝑇) & ⊢ (𝜑 → 𝐹 finSupp 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑇) → (𝑌𝑅𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) finSupp 𝑍) | ||
Theorem | ffs2 30157 | Rewrite a function's support based with its range rather than the universal class. See also frnsuppeq 7698. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐶 = (𝐵 ∖ {𝑍}) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 supp 𝑍) = (◡𝐹 “ 𝐶)) | ||
Theorem | ffsrn 30158 | The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ Fin) | ||
Theorem | resf1o 30159* | Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
⊢ 𝑋 = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶} & ⊢ 𝐹 = (𝑓 ∈ 𝑋 ↦ (𝑓 ↾ 𝐶)) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝐹:𝑋–1-1-onto→(𝐵 ↑𝑚 𝐶)) | ||
Theorem | maprnin 30160* | Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ∩ 𝐶) ↑𝑚 𝐴) = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ ran 𝑓 ⊆ 𝐶} | ||
Theorem | fpwrelmapffslem 30161* | Lemma for fpwrelmapffs 30163. For this theorem, the sets 𝐴 and 𝐵 could be infinite, but the relation 𝑅 itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝜑 → 𝐹:𝐴⟶𝒫 𝐵) & ⊢ (𝜑 → 𝑅 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}) ⇒ ⊢ (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin))) | ||
Theorem | fpwrelmap 30162* | Define a canonical mapping between functions from 𝐴 into subsets of 𝐵 and the relations with domain 𝐴 and range within 𝐵. Note that the same relation is used in axdc2lem 9721 and marypha2lem1 8750. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) ⇒ ⊢ 𝑀:(𝒫 𝐵 ↑𝑚 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵) | ||
Theorem | fpwrelmapffs 30163* | Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝐴) ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))}) & ⊢ 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑𝑚 𝐴) ∣ (𝑓 supp ∅) ∈ Fin} ⇒ ⊢ (𝑀 ↾ 𝑆):𝑆–1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin) | ||
Theorem | creq0 30164 | The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 11484. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ (𝐴 + (i · 𝐵)) = 0)) | ||
Theorem | 1nei 30165 | The imaginary unit i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
⊢ 1 ≠ i | ||
Theorem | 1neg1t1neg1 30166 | An integer unit times itself. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
⊢ (𝑁 ∈ {-1, 1} → (𝑁 · 𝑁) = 1) | ||
Theorem | nnmulge 30167 | Multiplying by a positive integer 𝑀 yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (𝑀 · 𝑁)) | ||
Theorem | lt2addrd 30168* | If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ (𝐴 = (𝑏 + 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) | ||
Theorem | xrlelttric 30169 | Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) | ||
Theorem | xaddeq0 30170 | Two extended reals which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴 +𝑒 𝐵) = 0 ↔ 𝐴 = -𝑒𝐵)) | ||
Theorem | xrinfm 30171 | The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
⊢ inf(ℝ*, ℝ*, < ) = -∞ | ||
Theorem | le2halvesd 30172 | A sum is less than the whole if each term is less than half. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ (𝐶 / 2)) & ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 2)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≤ 𝐶) | ||
Theorem | xraddge02 30173 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ 𝐵 → 𝐴 ≤ (𝐴 +𝑒 𝐵))) | ||
Theorem | xrge0addge 30174 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ (0[,]+∞)) → 𝐴 ≤ (𝐴 +𝑒 𝐵)) | ||
Theorem | xlt2addrd 30175* | If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ≠ -∞) & ⊢ (𝜑 → 𝐶 ≠ -∞) & ⊢ (𝜑 → 𝐴 < (𝐵 +𝑒 𝐶)) ⇒ ⊢ (𝜑 → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ* (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶)) | ||
Theorem | xrsupssd 30176 | Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝜑 → 𝐶 ⊆ ℝ*) ⇒ ⊢ (𝜑 → sup(𝐵, ℝ*, < ) ≤ sup(𝐶, ℝ*, < )) | ||
Theorem | xrge0infss 30177* | Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝐴 ⊆ (0[,]+∞) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | xrge0infssd 30178 | Inequality deduction for infimum of a nonnegative extended real subset. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ (0[,]+∞)) ⇒ ⊢ (𝜑 → inf(𝐵, (0[,]+∞), < ) ≤ inf(𝐶, (0[,]+∞), < )) | ||
Theorem | xrge0addcld 30179 | Nonnegative extended reals are closed under addition. (Contributed by Thierry Arnoux, 16-Sep-2019.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞)) | ||
Theorem | xrge0subcld 30180 | Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020.) |
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐴 +𝑒 -𝑒𝐵) ∈ (0[,]+∞)) | ||
Theorem | infxrge0lb 30181 | A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → inf(𝐴, (0[,]+∞), < ) ≤ 𝐵) | ||
Theorem | infxrge0glb 30182* | The infimum of a set of nonnegative extended reals is the greatest lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (inf(𝐴, (0[,]+∞), < ) < 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵)) | ||
Theorem | infxrge0gelb 30183* | The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞)) ⇒ ⊢ (𝜑 → (𝐵 ≤ inf(𝐴, (0[,]+∞), < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥)) | ||
Theorem | dfrp2 30184 | Alternate definition of the positive real numbers. (Contributed by Thierry Arnoux, 4-May-2020.) |
⊢ ℝ+ = (0(,)+∞) | ||
Theorem | xrofsup 30185 | The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017.) |
⊢ (𝜑 → 𝑋 ⊆ ℝ*) & ⊢ (𝜑 → 𝑌 ⊆ ℝ*) & ⊢ (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞) & ⊢ (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞) & ⊢ (𝜑 → 𝑍 = ( +𝑒 “ (𝑋 × 𝑌))) ⇒ ⊢ (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < ))) | ||
Theorem | supxrnemnf 30186 | The supremum of a nonempty set of extended reals which does not contain minus infinity is not minus infinity. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) ≠ -∞) | ||
Theorem | xnn0gt0 30187 | Non-zero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ ((𝑁 ∈ ℕ0* ∧ 𝑁 ≠ 0) → 0 < 𝑁) | ||
Theorem | xnn01gt 30188 | An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than 1. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
⊢ (𝑁 ∈ ℕ0* → (¬ 𝑁 ∈ {0, 1} ↔ 1 < 𝑁)) | ||
Theorem | nn0xmulclb 30189 | Finite multiplication in the extended nonnegative integers. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ (((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 ·e 𝐵) ∈ ℕ0 ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0))) | ||
Theorem | joiniooico 30190 | Disjoint joining an open interval with a closed-below, open-above interval to form a closed-below, open-above interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶)) → (((𝐴(,)𝐵) ∩ (𝐵[,)𝐶)) = ∅ ∧ ((𝐴(,)𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶))) | ||
Theorem | ubico 30191 | A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → ¬ 𝐵 ∈ (𝐴[,)𝐵)) | ||
Theorem | xeqlelt 30192 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵))) | ||
Theorem | eliccelico 30193 | Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵))) | ||
Theorem | elicoelioo 30194 | Relate elementhood to a closed-below, open-above interval with elementhood to the same open interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵)))) | ||
Theorem | iocinioc2 30195 | Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → ((𝐴(,]𝐶) ∩ (𝐵(,]𝐶)) = (𝐵(,]𝐶)) | ||
Theorem | xrdifh 30196 | Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.) |
⊢ 𝐴 ∈ ℝ* ⇒ ⊢ (ℝ* ∖ (𝐴[,]+∞)) = (-∞[,)𝐴) | ||
Theorem | iocinif 30197 | Relate intersection of two open-below, closed-above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴(,]𝐶) ∩ (𝐵(,]𝐶)) = if(𝐴 < 𝐵, (𝐵(,]𝐶), (𝐴(,]𝐶))) | ||
Theorem | difioo 30198 | The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐶) ∖ (𝐴(,)𝐵)) = (𝐵[,)𝐶)) | ||
Theorem | difico 30199 | The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,)𝐶) ∖ (𝐵[,)𝐶)) = (𝐴[,)𝐵)) | ||
Theorem | uzssico 30200 | Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ (𝑀[,)+∞)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |