Home | Metamath
Proof Explorer Theorem List (p. 84 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ressuppfi 8301 | 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 8302 | 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 8303 | The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍) | ||
Theorem | frnfsuppbi 8304 | Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.) |
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 finSupp 𝑍 ↔ (◡𝐹 “ (𝑆 ∖ {𝑍})) ∈ Fin))) | ||
Theorem | fsuppmptif 8305* | 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 | fsuppcolem 8306 | Lemma for fsuppco 8307. 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 8307 | 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 8308 | 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 8309 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 8309 | 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 8310* | Lemma 1 for mapfien 8313. (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊) | ||
Theorem | mapfienlem2 8311* | Lemma 2 for mapfien 8313. (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) finSupp 𝑍) | ||
Theorem | mapfienlem3 8312* | Lemma 3 for mapfien 8313. (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆) | ||
Theorem | mapfien 8313* | 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.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇) | ||
Theorem | mapfien2 8314* | Equinumerousity relation for sets of finitely supported functions. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑𝑚 𝐴) ∣ 𝑥 finSupp 0 } & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑𝑚 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ (𝜑 → 𝐴 ≈ 𝐶) & ⊢ (𝜑 → 𝐵 ≈ 𝐷) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Theorem | sniffsupp 8315* | A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 0 ∈ 𝑊) & ⊢ 𝐹 = (𝑥 ∈ 𝐼 ↦ if(𝑥 = 𝑋, 𝐴, 0 )) ⇒ ⊢ (𝜑 → 𝐹 finSupp 0 ) | ||
Syntax | cfi 8316 | Extend class notation with the function whose value is the class of all the finite intersections of the elements of a given set. |
class fi | ||
Definition | df-fi 8317* | Function whose value is the class of all the finite intersections of the elements of 𝑥. (Contributed by FL, 27-Apr-2008.) |
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) | ||
Theorem | fival 8318* | 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 8319* | Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) | ||
Theorem | elfi2 8320* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥)) | ||
Theorem | elfir 8321 | Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵)) | ||
Theorem | intrnfi 8322 | 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 8323* | 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 8324 | The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∩ 𝐵) ∈ (fi‘𝑋)) | ||
Theorem | ssfii 8325 | 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 8326 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘∅) = ∅ | ||
Theorem | fieq0 8327 | If 𝐴 is not empty, the class of all the finite intersections of 𝐴 is not empty either. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ∅ ↔ (fi‘𝐴) = ∅)) | ||
Theorem | fiin 8328 | The elements of (fi‘𝐶) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐴 ∩ 𝐵) ∈ (fi‘𝐶)) | ||
Theorem | dffi2 8329* | 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 8330 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵)) | ||
Theorem | inficl 8331* | 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 8332 | 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 8333 | A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (fi‘{𝐴}) = {𝐴} | ||
Theorem | fiuni 8334 | 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 8335 | 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 8336* | 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 8337* | 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 8338* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) | ||
Theorem | marypha1lem 8339* | Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))) | ||
Theorem | marypha1 8340* | (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 8341* | Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 ⊆ (𝐴 × ∪ ran 𝐹) | ||
Theorem | marypha2lem2 8342* | Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} | ||
Theorem | marypha2lem3 8343* | Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐺 ⊆ 𝑇 ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹‘𝑥))) | ||
Theorem | marypha2lem4 8344* | Lemma for marypha2 8345. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → (𝑇 “ 𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | marypha2 8345* | Version of marypha1 8340 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 8346 | 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 8347 | 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 8348* | 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 13977. See dfsup2 8350 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.) |
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} | ||
Definition | df-inf 8349 | 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 8350 | Quantifier free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ sup(𝐵, 𝐴, 𝑅) = ∪ (𝐴 ∖ ((◡𝑅 “ 𝐵) ∪ (𝑅 “ (𝐴 ∖ (◡𝑅 “ 𝐵))))) | ||
Theorem | supeq1 8351 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1d 8352 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1i 8353 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) | ||
Theorem | supeq2 8354 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅)) | ||
Theorem | supeq3 8355 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆)) | ||
Theorem | supeq123d 8356 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfsup 8357 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅) | ||
Theorem | supmo 8358* | 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 8359 | A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | supeu 8360* | 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 8361* | Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))) | ||
Theorem | eqsup 8362* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqsupd 8363* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | supcl 8364* | A supremum belongs to its base class (closure law). See also supub 8365 and suplub 8366. (Contributed by NM, 12-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supub 8365* |
A supremum is an upper bound. See also supcl 8364 and suplub 8366.
This proof demonstrates how to expand an iota-based definition (df-iota 5851) using riotacl2 6624. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | suplub 8366* | A supremum is the least upper bound. See also supcl 8364 and supub 8365. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | suplub2 8367* | Bidirectional form of suplub 8366. (Contributed by Mario Carneiro, 6-Sep-2014.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | supnub 8368* | An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅))) | ||
Theorem | supex 8369 | A supremum is a set. (Contributed by NM, 22-May-1999.) |
⊢ 𝑅 Or 𝐴 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V | ||
Theorem | sup00 8370 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ sup(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | sup0riota 8371* | The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
⊢ (𝑅 Or 𝐴 → sup(∅, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)) | ||
Theorem | sup0 8372* | The supremum of an empty set under a base set which has a unique smallest element is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑋) ∧ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) → sup(∅, 𝐴, 𝑅) = 𝑋) | ||
Theorem | supmax 8373* | The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jeff Hoffman, 17-Jun-2008.) (Proof shortened by OpenAI, 30-Mar-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | fisup2g 8374* | A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | fisupcl 8375 | A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵) | ||
Theorem | supgtoreq 8376 | The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 = sup(𝐵, 𝐴, 𝑅)) ⇒ ⊢ (𝜑 → (𝐶𝑅𝑆 ∨ 𝐶 = 𝑆)) | ||
Theorem | suppr 8377 | The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → sup({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐶𝑅𝐵, 𝐵, 𝐶)) | ||
Theorem | supsn 8378 | The supremum of a singleton. (Contributed by NM, 2-Oct-2007.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | supisolem 8379* | Lemma for supiso 8381. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) | ||
Theorem | supisoex 8380* | Lemma for supiso 8381. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))) | ||
Theorem | supiso 8381* | Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅))) | ||
Theorem | infeq1 8382 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1d 8383 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1i 8384 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) | ||
Theorem | infeq2 8385 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅)) | ||
Theorem | infeq3 8386 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆)) | ||
Theorem | infeq123d 8387 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfinf 8388 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅) | ||
Theorem | infexd 8389 | An infimum is a set. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | eqinf 8390* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqinfd 8391* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | infval 8392* | Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))) | ||
Theorem | infcllem 8393* | Lemma for infcl 8394, inflb 8395, infglb 8396, etc. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
Theorem | infcl 8394* | An infimum belongs to its base class (closure law). See also inflb 8395 and infglb 8396. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | inflb 8395* | An infimum is a lower bound. See also infcl 8394 and infglb 8396. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅))) | ||
Theorem | infglb 8396* | An infimum is the greatest lower bound. See also infcl 8394 and inflb 8395. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infglbb 8397* | Bidirectional form of infglb 8396. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infnlb 8398* | A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | infex 8399 | An infimum is a set. (Contributed by AV, 3-Sep-2020.) |
⊢ 𝑅 Or 𝐴 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V | ||
Theorem | infmin 8400* | The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |