Home | Metamath
Proof Explorer Theorem List (p. 89 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 | iunfi 8801* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 8802. Note that 𝐵 depends on 𝑥, i.e. can be thought of as 𝐵(𝑥). (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin) | ||
Theorem | unifi 8802 | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. (Contributed by NM, 22-Aug-2008.) (Revised by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴 ∈ Fin) | ||
Theorem | unifi2 8803* | The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 8802 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 8770). (Contributed by NM, 11-Mar-2006.) |
⊢ ((𝐴 ≺ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ ω) → ∪ 𝐴 ≺ ω) | ||
Theorem | infssuni 8804* | If an infinite set 𝐴 is included in the underlying set of a finite cover 𝐵, then there exists a set of the cover that contains an infinite number of element of 𝐴. (Contributed by FL, 2-Aug-2009.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝐵) → ∃𝑥 ∈ 𝐵 ¬ (𝐴 ∩ 𝑥) ∈ Fin) | ||
Theorem | unirnffid 8805 | The union of the range of a function from a finite set into the class of finite sets is finite. Deduction form. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐹:𝑇⟶Fin) & ⊢ (𝜑 → 𝑇 ∈ Fin) ⇒ ⊢ (𝜑 → ∪ ran 𝐹 ∈ Fin) | ||
Theorem | imafi 8806 | Images of finite sets are finite. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((Fun 𝐹 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin) | ||
Theorem | pwfilem 8807* | Lemma for pwfi 8808. (Contributed by NM, 26-Mar-2007.) |
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥})) ⇒ ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin) | ||
Theorem | pwfi 8808 | The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105. (Contributed by NM, 26-Mar-2007.) |
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin) | ||
Theorem | mapfi 8809 | Set exponentiation of finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ↑m 𝐵) ∈ Fin) | ||
Theorem | ixpfi 8810* | A Cartesian product of finitely many finite sets is finite. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) → X𝑥 ∈ 𝐴 𝐵 ∈ Fin) | ||
Theorem | ixpfi2 8811* | A Cartesian product of finite sets such that all but finitely many are singletons is finite. (Note that 𝐵(𝑥) and 𝐷(𝑥) are both possibly dependent on 𝑥.) (Contributed by Mario Carneiro, 25-Jan-2015.) |
⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐶)) → 𝐵 ⊆ {𝐷}) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 ∈ Fin) | ||
Theorem | mptfi 8812* | A finite mapping set is finite. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin) | ||
Theorem | abrexfi 8813* | An image set from a finite set is finite. (Contributed by Mario Carneiro, 13-Feb-2014.) |
⊢ (𝐴 ∈ Fin → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ Fin) | ||
Theorem | cnvimamptfin 8814* | A preimage of a mapping with a finite domain under any class is finite. In contrast to fisuppfi 8830, the range of the mapping needs not to be known. (Contributed by AV, 21-Dec-2018.) |
⊢ (𝜑 → 𝑁 ∈ Fin) ⇒ ⊢ (𝜑 → (◡(𝑝 ∈ 𝑁 ↦ 𝑋) “ 𝑌) ∈ Fin) | ||
Theorem | elfpw 8815 | Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐴 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ∈ Fin)) | ||
Theorem | unifpw 8816 | A set is the union of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ∪ (𝒫 𝐴 ∩ Fin) = 𝐴 | ||
Theorem | f1opwfi 8817* | A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015.) |
⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin)) | ||
Theorem | fissuni 8818* | A finite subset of a union is covered by finitely many elements. (Contributed by Stefan O'Rear, 2-Apr-2015.) |
⊢ ((𝐴 ⊆ ∪ 𝐵 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)𝐴 ⊆ ∪ 𝑐) | ||
Theorem | fipreima 8819* | Given a finite subset 𝐴 of the range of a function, there exists a finite subset of the domain whose image is 𝐴. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ (𝒫 𝐵 ∩ Fin)(𝐹 “ 𝑐) = 𝐴) | ||
Theorem | finsschain 8820* | A finite subset of the union of a superset chain is a subset of some element of the chain. A useful preliminary result for alexsub 22583 and others. (Contributed by Jeff Hankins, 25-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Feb-2015.) (Revised by Mario Carneiro, 18-May-2015.) |
⊢ (((𝐴 ≠ ∅ ∧ [⊊] Or 𝐴) ∧ (𝐵 ∈ Fin ∧ 𝐵 ⊆ ∪ 𝐴)) → ∃𝑧 ∈ 𝐴 𝐵 ⊆ 𝑧) | ||
Theorem | indexfi 8821* | If for every element of a finite indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a finite subset of 𝐵 consisting only of those elements which are indexed by 𝐴. Proven without the Axiom of Choice, unlike indexdom 34892. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) | ||
Syntax | cfsupp 8822 | Extend class definition to include the predicate to be a finitely supported function. |
class finSupp | ||
Definition | df-fsupp 8823* | Define the property of a function to be finitely supported (in relation to a given zero). (Contributed by AV, 23-May-2019.) |
⊢ finSupp = {〈𝑟, 𝑧〉 ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)} | ||
Theorem | relfsupp 8824 | The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019.) |
⊢ Rel finSupp | ||
Theorem | relprcnfsupp 8825 | A proper class is never finitely supported. (Contributed by AV, 7-Jun-2019.) |
⊢ (¬ 𝐴 ∈ V → ¬ 𝐴 finSupp 𝑍) | ||
Theorem | isfsupp 8826 | 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 | funisfsupp 8827 | 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 8828 | 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 8829 | A finitely supported function is a function with a finite support. (Contributed by AV, 6-Jun-2019.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) | ||
Theorem | fisuppfi 8830 | A function on a finite set is finitely supported. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin) | ||
Theorem | fdmfisuppfi 8831 | The support of a function with a finite domain is always finite. (Contributed by AV, 27-Apr-2019.) |
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) | ||
Theorem | fdmfifsupp 8832 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | fsuppmptdm 8833* | A mapping with a finite domain is finitely supported. (Contributed by AV, 7-Jun-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝑌) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | fndmfisuppfi 8834 | The support of a function with a finite domain is always finite. (Contributed by AV, 25-May-2019.) |
⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin) | ||
Theorem | fndmfifsupp 8835 | A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.) |
⊢ (𝜑 → 𝐹 Fn 𝐷) & ⊢ (𝜑 → 𝐷 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹 finSupp 𝑍) | ||
Theorem | suppeqfsuppbi 8836 | 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 8837 | 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 8838 | 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 | fsuppxpfi 8839 | The cartesian product of two finitely supported functions is finite. (Contributed by AV, 17-Jul-2019.) |
⊢ ((𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍) → ((𝐹 supp 𝑍) × (𝐺 supp 𝑍)) ∈ Fin) | ||
Theorem | fczfsuppd 8840 | A constant function with value zero is finitely supported. (Contributed by AV, 30-Jun-2019.) |
⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐵 × {𝑍}) finSupp 𝑍) | ||
Theorem | fsuppun 8841 | 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 8842 | 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 8843 | 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 8844 | The empty set is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
⊢ (𝑍 ∈ 𝑉 → ∅ finSupp 𝑍) | ||
Theorem | snopfsupp 8845 | A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → {〈𝑋, 𝑌〉} finSupp 𝑍) | ||
Theorem | funsnfsupp 8846 | 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 8847 | The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019.) |
⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍) | ||
Theorem | ressuppfi 8848 | 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 8849 | 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 8850 | The restriction of a function to a finite set is finitely supported. (Contributed by AV, 12-Dec-2019.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝑋) finSupp 𝑍) | ||
Theorem | frnfsuppbi 8851 | Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019.) |
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 finSupp 𝑍 ↔ (◡𝐹 “ (𝑆 ∖ {𝑍})) ∈ Fin))) | ||
Theorem | fsuppmptif 8852* | 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 8853 | Lemma for fsuppco 8854. 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 8854 | 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 8855 | 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 8856 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 8856 | 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 8857* | Lemma 1 for mapfien 8860. (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → (𝐺 ∘ (𝑓 ∘ 𝐹)) finSupp 𝑊) | ||
Theorem | mapfienlem2 8858* | Lemma 2 for mapfien 8860. (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) finSupp 𝑍) | ||
Theorem | mapfienlem3 8859* | Lemma 3 for mapfien 8860. (Contributed by AV, 3-Jul-2019.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑇) → ((◡𝐺 ∘ 𝑔) ∘ ◡𝐹) ∈ 𝑆) | ||
Theorem | mapfien 8860* | 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.) |
⊢ 𝑆 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍} & ⊢ 𝑇 = {𝑥 ∈ (𝐷 ↑m 𝐶) ∣ 𝑥 finSupp 𝑊} & ⊢ 𝑊 = (𝐺‘𝑍) & ⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) & ⊢ (𝜑 → 𝐺:𝐵–1-1-onto→𝐷) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ V) & ⊢ (𝜑 → 𝐷 ∈ V) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ (𝐺 ∘ (𝑓 ∘ 𝐹))):𝑆–1-1-onto→𝑇) | ||
Theorem | mapfien2 8861* | 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 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐷) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
Theorem | sniffsupp 8862* | 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 8863 | 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 8864* | 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 8867). (Contributed by FL, 27-Apr-2008.) |
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) | ||
Theorem | fival 8865* | 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 8866* | Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) | ||
Theorem | elfi2 8867* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥)) | ||
Theorem | elfir 8868 | Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵)) | ||
Theorem | intrnfi 8869 | 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 8870* | 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 8871 | The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ∩ 𝐵) ∈ (fi‘𝑋)) | ||
Theorem | ssfii 8872 | 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 8873 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘∅) = ∅ | ||
Theorem | fieq0 8874 | 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 8875 | The elements of (fi‘𝐶) are closed under finite intersection. (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ (fi‘𝐶) ∧ 𝐵 ∈ (fi‘𝐶)) → (𝐴 ∩ 𝐵) ∈ (fi‘𝐶)) | ||
Theorem | dffi2 8876* | 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 8877 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵)) | ||
Theorem | inficl 8878* | 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 8879 | 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 8880 | A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (fi‘{𝐴}) = {𝐴} | ||
Theorem | fiuni 8881 | 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 8882 | 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 8883* | 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 8884* | 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 8885* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) | ||
Theorem | marypha1lem 8886* | Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))) | ||
Theorem | marypha1 8887* | (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 8888* | Lemma for marypha2 8892. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 ⊆ (𝐴 × ∪ ran 𝐹) | ||
Theorem | marypha2lem2 8889* | Lemma for marypha2 8892. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} | ||
Theorem | marypha2lem3 8890* | Lemma for marypha2 8892. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐺 ⊆ 𝑇 ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹‘𝑥))) | ||
Theorem | marypha2lem4 8891* | Lemma for marypha2 8892. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → (𝑇 “ 𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | marypha2 8892* | Version of marypha1 8887 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 8893 | 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 8894 | 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 8895* | 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 14586. See dfsup2 8897 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.) |
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} | ||
Definition | df-inf 8896 | 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 8897 | Quantifier free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ sup(𝐵, 𝐴, 𝑅) = ∪ (𝐴 ∖ ((◡𝑅 “ 𝐵) ∪ (𝑅 “ (𝐴 ∖ (◡𝑅 “ 𝐵))))) | ||
Theorem | supeq1 8898 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1d 8899 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1i 8900 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |