![]() |
Metamath
Proof Explorer Theorem List (p. 82 of 482) | < 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-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | curry1 8101* | Composition with β‘(2nd βΎ ({πΆ} Γ V)) turns any binary operation πΉ with a constant first operand into a function πΊ of the second operand only. This transformation is called "currying". (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Dec-2014.) |
β’ πΊ = (πΉ β β‘(2nd βΎ ({πΆ} Γ V))) β β’ ((πΉ Fn (π΄ Γ π΅) β§ πΆ β π΄) β πΊ = (π₯ β π΅ β¦ (πΆπΉπ₯))) | ||
Theorem | curry1val 8102 | The value of a curried function with a constant first argument. (Contributed by NM, 28-Mar-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
β’ πΊ = (πΉ β β‘(2nd βΎ ({πΆ} Γ V))) β β’ ((πΉ Fn (π΄ Γ π΅) β§ πΆ β π΄) β (πΊβπ·) = (πΆπΉπ·)) | ||
Theorem | curry1f 8103 | Functionality of a curried function with a constant first argument. (Contributed by NM, 29-Mar-2008.) |
β’ πΊ = (πΉ β β‘(2nd βΎ ({πΆ} Γ V))) β β’ ((πΉ:(π΄ Γ π΅)βΆπ· β§ πΆ β π΄) β πΊ:π΅βΆπ·) | ||
Theorem | curry2 8104* | Composition with β‘(1st βΎ (V Γ {πΆ})) turns any binary operation πΉ with a constant second operand into a function πΊ of the first operand only. This transformation is called "currying". (If this becomes frequently used, we can introduce a new notation for the hypothesis.) (Contributed by NM, 16-Dec-2008.) |
β’ πΊ = (πΉ β β‘(1st βΎ (V Γ {πΆ}))) β β’ ((πΉ Fn (π΄ Γ π΅) β§ πΆ β π΅) β πΊ = (π₯ β π΄ β¦ (π₯πΉπΆ))) | ||
Theorem | curry2f 8105 | Functionality of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
β’ πΊ = (πΉ β β‘(1st βΎ (V Γ {πΆ}))) β β’ ((πΉ:(π΄ Γ π΅)βΆπ· β§ πΆ β π΅) β πΊ:π΄βΆπ·) | ||
Theorem | curry2val 8106 | The value of a curried function with a constant second argument. (Contributed by NM, 16-Dec-2008.) |
β’ πΊ = (πΉ β β‘(1st βΎ (V Γ {πΆ}))) β β’ ((πΉ Fn (π΄ Γ π΅) β§ πΆ β π΅) β (πΊβπ·) = (π·πΉπΆ)) | ||
Theorem | cnvf1olem 8107 | Lemma for cnvf1o 8108. (Contributed by Mario Carneiro, 27-Apr-2014.) |
β’ ((Rel π΄ β§ (π΅ β π΄ β§ πΆ = βͺ β‘{π΅})) β (πΆ β β‘π΄ β§ π΅ = βͺ β‘{πΆ})) | ||
Theorem | cnvf1o 8108* | Describe a function that maps the elements of a set to its converse bijectively. (Contributed by Mario Carneiro, 27-Apr-2014.) |
β’ (Rel π΄ β (π₯ β π΄ β¦ βͺ β‘{π₯}):π΄β1-1-ontoββ‘π΄) | ||
Theorem | fparlem1 8109 | Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (β‘(1st βΎ (V Γ V)) β {π₯}) = ({π₯} Γ V) | ||
Theorem | fparlem2 8110 | Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (β‘(2nd βΎ (V Γ V)) β {π¦}) = (V Γ {π¦}) | ||
Theorem | fparlem3 8111* | Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΉ Fn π΄ β (β‘(1st βΎ (V Γ V)) β (πΉ β (1st βΎ (V Γ V)))) = βͺ π₯ β π΄ (({π₯} Γ V) Γ ({(πΉβπ₯)} Γ V))) | ||
Theorem | fparlem4 8112* | Lemma for fpar 8113. (Contributed by NM, 22-Dec-2008.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΊ Fn π΅ β (β‘(2nd βΎ (V Γ V)) β (πΊ β (2nd βΎ (V Γ V)))) = βͺ π¦ β π΅ ((V Γ {π¦}) Γ (V Γ {(πΊβπ¦)}))) | ||
Theorem | fpar 8113* | Merge two functions in parallel. Use as the second argument of a composition with a binary operation to build compound functions such as (π₯ β (0[,)+β), π¦ β β β¦ ((ββπ₯) + (sinβπ¦))), see also ex-fpar 30246. (Contributed by NM, 17-Sep-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) |
β’ π» = ((β‘(1st βΎ (V Γ V)) β (πΉ β (1st βΎ (V Γ V)))) β© (β‘(2nd βΎ (V Γ V)) β (πΊ β (2nd βΎ (V Γ V))))) β β’ ((πΉ Fn π΄ β§ πΊ Fn π΅) β π» = (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©)) | ||
Theorem | fsplit 8114 | A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar 8113 in order to build compound functions such as (π₯ β (0[,)+β) β¦ ((ββπ₯) + (sinβπ₯))). (Contributed by NM, 17-Sep-2007.) Replace use of dfid2 5572 with df-id 5570. (Revised by BJ, 31-Dec-2023.) |
β’ β‘(1st βΎ I ) = (π₯ β V β¦ β¨π₯, π₯β©) | ||
Theorem | fsplitfpar 8115* | Merge two functions with a common argument in parallel. Combination of fsplit 8114 and fpar 8113. (Contributed by AV, 3-Jan-2024.) |
β’ π» = ((β‘(1st βΎ (V Γ V)) β (πΉ β (1st βΎ (V Γ V)))) β© (β‘(2nd βΎ (V Γ V)) β (πΊ β (2nd βΎ (V Γ V))))) & β’ π = (β‘(1st βΎ I ) βΎ π΄) β β’ ((πΉ Fn π΄ β§ πΊ Fn π΄) β (π» β π) = (π₯ β π΄ β¦ β¨(πΉβπ₯), (πΊβπ₯)β©)) | ||
Theorem | offsplitfpar 8116 | Express the function operation map βf by the functions defined in fsplit 8114 and fpar 8113. (Contributed by AV, 4-Jan-2024.) |
β’ π» = ((β‘(1st βΎ (V Γ V)) β (πΉ β (1st βΎ (V Γ V)))) β© (β‘(2nd βΎ (V Γ V)) β (πΊ β (2nd βΎ (V Γ V))))) & β’ π = (β‘(1st βΎ I ) βΎ π΄) β β’ (((πΉ Fn π΄ β§ πΊ Fn π΄) β§ (πΉ β π β§ πΊ β π) β§ ( + Fn πΆ β§ (ran πΉ Γ ran πΊ) β πΆ)) β ( + β (π» β π)) = (πΉ βf + πΊ)) | ||
Theorem | f2ndf 8117 | The 2nd (second component of an ordered pair) function restricted to a function πΉ is a function from πΉ into the codomain of πΉ. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆπ΅) | ||
Theorem | fo2ndf 8118 | The 2nd (second component of an ordered pair) function restricted to a function πΉ is a function from πΉ onto the range of πΉ. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβontoβran πΉ) | ||
Theorem | f1o2ndf1 8119 | The 2nd (second component of an ordered pair) function restricted to a one-to-one function πΉ is a one-to-one function from πΉ onto the range of πΉ. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
β’ (πΉ:π΄β1-1βπ΅ β (2nd βΎ πΉ):πΉβ1-1-ontoβran πΉ) | ||
Theorem | opco1 8120 | Value of an operation precomposed with the projection on the first component. (Contributed by Mario Carneiro, 28-May-2014.) Generalize to closed form. (Revised by BJ, 27-Oct-2024.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(πΉ β 1st )π΅) = (πΉβπ΄)) | ||
Theorem | opco2 8121 | Value of an operation precomposed with the projection on the second component. (Contributed by BJ, 27-Oct-2024.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (π΄(πΉ β 2nd )π΅) = (πΉβπ΅)) | ||
Theorem | opco1i 8122 | Inference form of opco1 8120. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π΅ β V & β’ πΆ β V β β’ (π΅(πΉ β 1st )πΆ) = (πΉβπ΅) | ||
Theorem | frxp 8123* | A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅)) β§ ((1st βπ₯)π (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯)π(2nd βπ¦))))} β β’ ((π Fr π΄ β§ π Fr π΅) β π Fr (π΄ Γ π΅)) | ||
Theorem | xporderlem 8124* | Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅)) β§ ((1st βπ₯)π (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯)π(2nd βπ¦))))} β β’ (β¨π, πβ©πβ¨π, πβ© β (((π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π΅)) β§ (ππ π β¨ (π = π β§ πππ)))) | ||
Theorem | poxp 8125* | A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅)) β§ ((1st βπ₯)π (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯)π(2nd βπ¦))))} β β’ ((π Po π΄ β§ π Po π΅) β π Po (π΄ Γ π΅)) | ||
Theorem | soxp 8126* | A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅)) β§ ((1st βπ₯)π (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯)π(2nd βπ¦))))} β β’ ((π Or π΄ β§ π Or π΅) β π Or (π΄ Γ π΅)) | ||
Theorem | wexp 8127* | A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅)) β§ ((1st βπ₯)π (1st βπ¦) β¨ ((1st βπ₯) = (1st βπ¦) β§ (2nd βπ₯)π(2nd βπ¦))))} β β’ ((π We π΄ β§ π We π΅) β π We (π΄ Γ π΅)) | ||
Theorem | fnwelem 8128* | Lemma for fnwe 8129. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))} & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π We π΅) & β’ (π β π We π΄) & β’ (π β (πΉ β π€) β V) & β’ π = {β¨π’, π£β© β£ ((π’ β (π΅ Γ π΄) β§ π£ β (π΅ Γ π΄)) β§ ((1st βπ’)π (1st βπ£) β¨ ((1st βπ’) = (1st βπ£) β§ (2nd βπ’)π(2nd βπ£))))} & β’ πΊ = (π§ β π΄ β¦ β¨(πΉβπ§), π§β©) β β’ (π β π We π΄) | ||
Theorem | fnwe 8129* | A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))} & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π We π΅) & β’ (π β π We π΄) & β’ (π β (πΉ β π€) β V) β β’ (π β π We π΄) | ||
Theorem | fnse 8130* | Condition for the well-order in fnwe 8129 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.) |
β’ π = {β¨π₯, π¦β© β£ ((π₯ β π΄ β§ π¦ β π΄) β§ ((πΉβπ₯)π (πΉβπ¦) β¨ ((πΉβπ₯) = (πΉβπ¦) β§ π₯ππ¦)))} & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π Se π΅) & β’ (π β (β‘πΉ β π€) β V) β β’ (π β π Se π΄) | ||
Theorem | fvproj 8131* | Value of a function on ordered pairs with values expressed as ordered pairs. Note that πΉ and πΊ are the projections of π» to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
β’ π» = (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) & β’ (π β π β π΄) & β’ (π β π β π΅) β β’ (π β (π»ββ¨π, πβ©) = β¨(πΉβπ), (πΊβπ)β©) | ||
Theorem | fimaproj 8132* | Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that πΉ and πΊ are the projections of π» to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
β’ π» = (π₯ β π΄, π¦ β π΅ β¦ β¨(πΉβπ₯), (πΊβπ¦)β©) & β’ (π β πΉ Fn π΄) & β’ (π β πΊ Fn π΅) & β’ (π β π β π΄) & β’ (π β π β π΅) β β’ (π β (π» β (π Γ π)) = ((πΉ β π) Γ (πΊ β π))) | ||
Theorem | ralxpes 8133* | A version of ralxp 5838 with explicit substitution. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ (βπ₯ β (π΄ Γ π΅)[(1st βπ₯) / π¦][(2nd βπ₯) / π§]π β βπ¦ β π΄ βπ§ β π΅ π) | ||
Theorem | ralxp3f 8134* | Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ β²π¦π & β’ β²π§π & β’ β²π€π & β’ β²π₯π & β’ (π₯ = β¨π¦, π§, π€β© β (π β π)) β β’ (βπ₯ β ((π΄ Γ π΅) Γ πΆ)π β βπ¦ β π΄ βπ§ β π΅ βπ€ β πΆ π) | ||
Theorem | ralxp3 8135* | Restricted for all over a triple Cartesian product. (Contributed by Scott Fenton, 2-Feb-2025.) |
β’ (π₯ = β¨π¦, π§, π€β© β (π β π)) β β’ (βπ₯ β ((π΄ Γ π΅) Γ πΆ)π β βπ¦ β π΄ βπ§ β π΅ βπ€ β πΆ π) | ||
Theorem | ralxp3es 8136* | Restricted for-all over a triple Cartesian product with explicit substitution. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ (βπ₯ β ((π΄ Γ π΅) Γ πΆ)[(1st β(1st βπ₯)) / π¦][(2nd β(1st βπ₯)) / π§][(2nd βπ₯) / π€]π β βπ¦ β π΄ βπ§ β π΅ βπ€ β πΆ π) | ||
Theorem | frpoins3xpg 8137* | Special case of founded partial induction over a Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ ((π₯ β π΄ β§ π¦ β π΅) β (βπ§βπ€(β¨π§, π€β© β Pred(π , (π΄ Γ π΅), β¨π₯, π¦β©) β π) β π)) & β’ (π₯ = π§ β (π β π)) & β’ (π¦ = π€ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π¦ = π β (π β π)) β β’ (((π Fr (π΄ Γ π΅) β§ π Po (π΄ Γ π΅) β§ π Se (π΄ Γ π΅)) β§ (π β π΄ β§ π β π΅)) β π) | ||
Theorem | frpoins3xp3g 8138* | Special case of founded partial recursion over a triple Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ ((π₯ β π΄ β§ π¦ β π΅ β§ π§ β πΆ) β (βπ€βπ‘βπ’(β¨π€, π‘, π’β© β Pred(π , ((π΄ Γ π΅) Γ πΆ), β¨π₯, π¦, π§β©) β π) β π)) & β’ (π₯ = π€ β (π β π)) & β’ (π¦ = π‘ β (π β π)) & β’ (π§ = π’ β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π¦ = π β (π β π)) & β’ (π§ = π β (π β π)) β β’ (((π Fr ((π΄ Γ π΅) Γ πΆ) β§ π Po ((π΄ Γ π΅) Γ πΆ) β§ π Se ((π΄ Γ π΅) Γ πΆ)) β§ (π β π΄ β§ π β π΅ β§ π β πΆ)) β π) | ||
Theorem | xpord2lem 8139* | Lemma for Cartesian product ordering. Calculate the value of the Cartesian product relation. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ (β¨π, πβ©πβ¨π, πβ© β ((π β π΄ β§ π β π΅) β§ (π β π΄ β§ π β π΅) β§ ((ππ π β¨ π = π) β§ (πππ β¨ π = π) β§ (π β π β¨ π β π)))) | ||
Theorem | poxp2 8140* | Another way of partially ordering a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ (π β π Po π΄) & β’ (π β π Po π΅) β β’ (π β π Po (π΄ Γ π΅)) | ||
Theorem | frxp2 8141* | Another way of giving a well-founded order to a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ (π β π Fr π΄) & β’ (π β π Fr π΅) β β’ (π β π Fr (π΄ Γ π΅)) | ||
Theorem | xpord2pred 8142* | Calculate the predecessor class in frxp2 8141. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ ((π β π΄ β§ π β π΅) β Pred(π, (π΄ Γ π΅), β¨π, πβ©) = (((Pred(π , π΄, π) βͺ {π}) Γ (Pred(π, π΅, π) βͺ {π})) β {β¨π, πβ©})) | ||
Theorem | sexp2 8143* | Condition for the relation in frxp2 8141 to be set-like. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ (π β π Se π΄) & β’ (π β π Se π΅) β β’ (π β π Se (π΄ Γ π΅)) | ||
Theorem | xpord2indlem 8144* | Induction over the Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄ Γ π΅) β§ π¦ β (π΄ Γ π΅) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} & β’ π Fr π΄ & β’ π Po π΄ & β’ π Se π΄ & β’ π Fr π΅ & β’ π Po π΅ & β’ π Se π΅ & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β π΄ β§ π β π΅) β ((βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)π β§ βπ β Pred (π , π΄, π)π β§ βπ β Pred (π, π΅, π)π) β π)) β β’ ((π β π΄ β§ π β π΅) β π) | ||
Theorem | xpord2ind 8145* | Induction over the Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ π Fr π΄ & β’ π Po π΄ & β’ π Se π΄ & β’ π Fr π΅ & β’ π Po π΅ & β’ π Se π΅ & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β π΄ β§ π β π΅) β ((βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)π β§ βπ β Pred (π , π΄, π)π β§ βπ β Pred (π, π΅, π)π) β π)) β β’ ((π β π΄ β§ π β π΅) β π) | ||
Theorem | xpord3lem 8146* | Lemma for triple ordering. Calculate the value of the relation. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} β β’ (β¨π, π, πβ©πβ¨π, π, πβ© β ((π β π΄ β§ π β π΅ β§ π β πΆ) β§ (π β π΄ β§ π β π΅ β§ π β πΆ) β§ (((ππ π β¨ π = π) β§ (πππ β¨ π = π) β§ (πππ β¨ π = π)) β§ (π β π β¨ π β π β¨ π β π)))) | ||
Theorem | poxp3 8147* | Triple Cartesian product partial ordering. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ (π β π Po π΄) & β’ (π β π Po π΅) & β’ (π β π Po πΆ) β β’ (π β π Po ((π΄ Γ π΅) Γ πΆ)) | ||
Theorem | frxp3 8148* | Give well-foundedness over a triple Cartesian product. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ (π β π Fr π΄) & β’ (π β π Fr π΅) & β’ (π β π Fr πΆ) β β’ (π β π Fr ((π΄ Γ π΅) Γ πΆ)) | ||
Theorem | xpord3pred 8149* | Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} β β’ ((π β π΄ β§ π β π΅ β§ π β πΆ) β Pred(π, ((π΄ Γ π΅) Γ πΆ), β¨π, π, πβ©) = ((((Pred(π , π΄, π) βͺ {π}) Γ (Pred(π, π΅, π) βͺ {π})) Γ (Pred(π, πΆ, π) βͺ {π})) β {β¨π, π, πβ©})) | ||
Theorem | sexp3 8150* | Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ (π β π Se π΄) & β’ (π β π Se π΅) & β’ (π β π Se πΆ) β β’ (π β π Se ((π΄ Γ π΅) Γ πΆ)) | ||
Theorem | xpord3inddlem 8151* | Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025.) |
β’ π = {β¨π₯, π¦β© β£ (π₯ β ((π΄ Γ π΅) Γ πΆ) β§ π¦ β ((π΄ Γ π΅) Γ πΆ) β§ ((((1st β(1st βπ₯))π (1st β(1st βπ¦)) β¨ (1st β(1st βπ₯)) = (1st β(1st βπ¦))) β§ ((2nd β(1st βπ₯))π(2nd β(1st βπ¦)) β¨ (2nd β(1st βπ₯)) = (2nd β(1st βπ¦))) β§ ((2nd βπ₯)π(2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦))) β§ π₯ β π¦))} & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ (π β π β πΆ) & β’ (π β π Fr π΄) & β’ (π β π Po π΄) & β’ (π β π Se π΄) & β’ (π β π Fr π΅) & β’ (π β π Po π΅) & β’ (π β π Se π΅) & β’ (π β π Fr πΆ) & β’ (π β π Po πΆ) & β’ (π β π Se πΆ) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β§ (π β π΄ β§ π β π΅ β§ π β πΆ)) β (((βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, πΆ, π)π) β§ (βπ β Pred (π , π΄, π)π β§ βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π, π΅, π)π) β§ βπ β Pred (π, πΆ, π)π) β π)) β β’ (π β π) | ||
Theorem | xpord3indd 8152* | Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025.) |
β’ (π β π β π΄) & β’ (π β π β π΅) & β’ (π β π β πΆ) & β’ (π β π Fr π΄) & β’ (π β π Po π΄) & β’ (π β π Se π΄) & β’ (π β π Fr π΅) & β’ (π β π Po π΅) & β’ (π β π Se π΅) & β’ (π β π Fr πΆ) & β’ (π β π Po πΆ) & β’ (π β π Se πΆ) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β§ (π β π΄ β§ π β π΅ β§ π β πΆ)) β (((βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, πΆ, π)π) β§ (βπ β Pred (π , π΄, π)π β§ βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π, π΅, π)π) β§ βπ β Pred (π, πΆ, π)π) β π)) β β’ (π β π) | ||
Theorem | xpord3ind 8153* | Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024.) |
β’ π Fr π΄ & β’ π Po π΄ & β’ π Se π΄ & β’ π Fr π΅ & β’ π Po π΅ & β’ π Se π΅ & β’ π Fr πΆ & β’ π Po πΆ & β’ π Se πΆ & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β π΄ β§ π β π΅ β§ π β πΆ) β (((βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, π΅, π)π β§ βπ β Pred (π , π΄, π)βπ β Pred (π, πΆ, π)π) β§ (βπ β Pred (π , π΄, π)π β§ βπ β Pred (π, π΅, π)βπ β Pred (π, πΆ, π)π β§ βπ β Pred (π, π΅, π)π) β§ βπ β Pred (π, πΆ, π)π) β π)) β β’ ((π β π΄ β§ π β π΅ β§ π β πΆ) β π) | ||
Theorem | orderseqlem 8154* | Lemma for poseq 8155 and soseq 8156. The function value of a sequence is either in π΄ or null. (Contributed by Scott Fenton, 8-Jun-2011.) |
β’ πΉ = {π β£ βπ₯ β On π:π₯βΆπ΄} β β’ (πΊ β πΉ β (πΊβπ) β (π΄ βͺ {β })) | ||
Theorem | poseq 8155* | A partial ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011.) |
β’ π Po (π΄ βͺ {β }) & β’ πΉ = {π β£ βπ₯ β On π:π₯βΆπ΄} & β’ π = {β¨π, πβ© β£ ((π β πΉ β§ π β πΉ) β§ βπ₯ β On (βπ¦ β π₯ (πβπ¦) = (πβπ¦) β§ (πβπ₯)π (πβπ₯)))} β β’ π Po πΉ | ||
Theorem | soseq 8156* | A linear ordering of ordinal sequences. (Contributed by Scott Fenton, 8-Jun-2011.) |
β’ π Or (π΄ βͺ {β }) & β’ πΉ = {π β£ βπ₯ β On π:π₯βΆπ΄} & β’ π = {β¨π, πβ© β£ ((π β πΉ β§ π β πΉ) β§ βπ₯ β On (βπ¦ β π₯ (πβπ¦) = (πβπ¦) β§ (πβπ₯)π (πβπ₯)))} & β’ Β¬ β β π΄ β β’ π Or πΉ | ||
In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 8159) are based on the Axiom of Union (usage of dmexg 7901), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (β‘π β (V β {π})) (see suppimacnv 8170). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now). | ||
Syntax | csupp 8157 | Extend class definition to include the support of functions. |
class supp | ||
Definition | df-supp 8158* | Define the support of a function against a "zero" value. According to Wikipedia ("Support (mathematics)", 31-Mar-2019, https://en.wikipedia.org/wiki/Support_(mathematics)) "In mathematics, the support of a real-valued function f is the subset of the domain containing those elements which are not mapped to zero." and "The notion of support also extends in a natural way to functions taking values in more general sets than R [the real numbers] and to other objects." The following definition allows for such extensions, being applicable for any sets (which usually are functions) and any element (even not necessarily from the range of the function) regarded as "zero". (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
β’ supp = (π₯ β V, π§ β V β¦ {π β dom π₯ β£ (π₯ β {π}) β {π§}}) | ||
Theorem | suppval 8159* | The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
β’ ((π β π β§ π β π) β (π supp π) = {π β dom π β£ (π β {π}) β {π}}) | ||
Theorem | supp0prc 8160 | The support of a class is empty if either the class or the "zero" is a proper class. (Contributed by AV, 28-May-2019.) |
β’ (Β¬ (π β V β§ π β V) β (π supp π) = β ) | ||
Theorem | suppvalbr 8161* | The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
β’ ((π β π β§ π β π) β (π supp π) = {π₯ β£ (βπ¦ π₯π π¦ β§ βπ¦(π₯π π¦ β π¦ β π))}) | ||
Theorem | supp0 8162 | The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.) |
β’ (π β π β (β supp π) = β ) | ||
Theorem | suppval1 8163* | The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019.) |
β’ ((Fun π β§ π β π β§ π β π) β (π supp π) = {π β dom π β£ (πβπ) β π}) | ||
Theorem | suppvalfng 8164* | The value of the operation constructing the support of a function with a given domain. This version of suppvalfn 8165 assumes πΉ is a set rather than its domain π, avoiding ax-rep 5279. (Contributed by SN, 5-Aug-2024.) |
β’ ((πΉ Fn π β§ πΉ β π β§ π β π) β (πΉ supp π) = {π β π β£ (πΉβπ) β π}) | ||
Theorem | suppvalfn 8165* | The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by AV, 22-Apr-2019.) |
β’ ((πΉ Fn π β§ π β π β§ π β π) β (πΉ supp π) = {π β π β£ (πΉβπ) β π}) | ||
Theorem | elsuppfng 8166 | An element of the support of a function with a given domain. This version of elsuppfn 8167 assumes πΉ is a set rather than its domain π, avoiding ax-rep 5279. (Contributed by SN, 5-Aug-2024.) |
β’ ((πΉ Fn π β§ πΉ β π β§ π β π) β (π β (πΉ supp π) β (π β π β§ (πΉβπ) β π))) | ||
Theorem | elsuppfn 8167 | An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019.) |
β’ ((πΉ Fn π β§ π β π β§ π β π) β (π β (πΉ supp π) β (π β π β§ (πΉβπ) β π))) | ||
Theorem | cnvimadfsn 8168* | The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
β’ (β‘π β (V β {π})) = {π₯ β£ βπ¦(π₯π π¦ β§ π¦ β π)} | ||
Theorem | suppimacnvss 8169 | The support of functions "defined" by inverse images is a subset of the support defined by df-supp 8158. (Contributed by AV, 7-Apr-2019.) |
β’ ((π β π β§ π β π) β (β‘π β (V β {π})) β (π supp π)) | ||
Theorem | suppimacnv 8170 | Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.) |
β’ ((π β π β§ π β π) β (π supp π) = (β‘π β (V β {π}))) | ||
Theorem | fsuppeq 8171 | Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.) |
β’ ((πΌ β π β§ π β π) β (πΉ:πΌβΆπ β (πΉ supp π) = (β‘πΉ β (π β {π})))) | ||
Theorem | fsuppeqg 8172 | Version of fsuppeq 8171 avoiding ax-rep 5279 by assuming πΉ is a set rather than its domain πΌ. (Contributed by SN, 30-Jul-2024.) |
β’ ((πΉ β π β§ π β π) β (πΉ:πΌβΆπ β (πΉ supp π) = (β‘πΉ β (π β {π})))) | ||
Theorem | suppssdm 8173 | The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.) |
β’ (πΉ supp π) β dom πΉ | ||
Theorem | suppsnop 8174 | The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019.) |
β’ πΉ = {β¨π, πβ©} β β’ ((π β π β§ π β π β§ π β π) β (πΉ supp π) = if(π = π, β , {π})) | ||
Theorem | snopsuppss 8175 | The support of a singleton containing an ordered pair is a subset of the singleton containing the first element of the ordered pair, i.e. it is empty or the singleton itself. (Contributed by AV, 19-Jul-2019.) |
β’ ({β¨π, πβ©} supp π) β {π} | ||
Theorem | fvn0elsupp 8176 | If the function value for a given argument is not empty, the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 2-Jul-2019.) (Revised by AV, 4-Apr-2020.) |
β’ (((π΅ β π β§ π β π΅) β§ (πΊ Fn π΅ β§ (πΊβπ) β β )) β π β (πΊ supp β )) | ||
Theorem | fvn0elsuppb 8177 | The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020.) |
β’ ((π΅ β π β§ π β π΅ β§ πΊ Fn π΅) β ((πΊβπ) β β β π β (πΊ supp β ))) | ||
Theorem | rexsupp 8178* | Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by AV, 27-May-2019.) |
β’ ((πΉ Fn π β§ π β π β§ π β π) β (βπ₯ β (πΉ supp π)π β βπ₯ β π ((πΉβπ₯) β π β§ π))) | ||
Theorem | ressuppss 8179 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
β’ ((πΉ β π β§ π β π) β ((πΉ βΎ π΅) supp π) β (πΉ supp π)) | ||
Theorem | suppun 8180 | The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019.) |
β’ (π β πΊ β π) β β’ (π β (πΉ supp π) β ((πΉ βͺ πΊ) supp π)) | ||
Theorem | ressuppssdif 8181 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
β’ ((πΉ β π β§ π β π) β (πΉ supp π) β (((πΉ βΎ π΅) supp π) βͺ (dom πΉ β π΅))) | ||
Theorem | mptsuppdifd 8182* | The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β π΄ β π) & β’ (π β π β π) β β’ (π β (πΉ supp π) = {π₯ β π΄ β£ π΅ β (V β {π})}) | ||
Theorem | mptsuppd 8183* | The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019.) (Revised by AV, 28-May-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ ((π β§ π₯ β π΄) β π΅ β π) β β’ (π β (πΉ supp π) = {π₯ β π΄ β£ π΅ β π}) | ||
Theorem | extmptsuppeq 8184* | The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 30-Jun-2019.) |
β’ (π β π΅ β π) & β’ (π β π΄ β π΅) & β’ ((π β§ π β (π΅ β π΄)) β π = π) β β’ (π β ((π β π΄ β¦ π) supp π) = ((π β π΅ β¦ π) supp π)) | ||
Theorem | suppfnss 8185* | The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 6-Jun-2022.) |
β’ (((πΉ Fn π΄ β§ πΊ Fn π΅) β§ (π΄ β π΅ β§ π΅ β π β§ π β π)) β (βπ₯ β π΄ ((πΊβπ₯) = π β (πΉβπ₯) = π) β (πΉ supp π) β (πΊ supp π))) | ||
Theorem | funsssuppss 8186 | The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019.) |
β’ ((Fun πΊ β§ πΉ β πΊ β§ πΊ β π) β (πΉ supp π) β (πΊ supp π)) | ||
Theorem | fnsuppres 8187 | Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 28-May-2019.) |
β’ ((πΉ Fn (π΄ βͺ π΅) β§ (πΉ β π β§ π β π) β§ (π΄ β© π΅) = β ) β ((πΉ supp π) β π΄ β (πΉ βΎ π΅) = (π΅ Γ {π}))) | ||
Theorem | fnsuppeq0 8188 | The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
β’ ((πΉ Fn π΄ β§ π΄ β π β§ π β π) β ((πΉ supp π) = β β πΉ = (π΄ Γ {π}))) | ||
Theorem | fczsupp0 8189 | The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019.) |
β’ ((π΅ Γ {π}) supp π) = β | ||
Theorem | suppss 8190* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) (Proof shortened by SN, 5-Aug-2024.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ ((π β§ π β (π΄ β π)) β (πΉβπ) = π) β β’ (π β (πΉ supp π) β π) | ||
Theorem | suppssOLD 8191* | Obsolete version of suppss 8190 as of 5-Aug-2024. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ ((π β§ π β (π΄ β π)) β (πΉβπ) = π) β β’ (π β (πΉ supp π) β π) | ||
Theorem | suppssr 8192 | A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ (π β (πΉ supp π) β π) & β’ (π β π΄ β π) & β’ (π β π β π) β β’ ((π β§ π β (π΄ β π)) β (πΉβπ) = π) | ||
Theorem | suppssrg 8193 | A function is zero outside its support. Version of suppssr 8192 avoiding ax-rep 5279 by assuming πΉ is a set rather than its domain π΄. (Contributed by SN, 5-May-2024.) |
β’ (π β πΉ:π΄βΆπ΅) & β’ (π β (πΉ supp π) β π) & β’ (π β πΉ β π) & β’ (π β π β π) β β’ ((π β§ π β (π΄ β π)) β (πΉβπ) = π) | ||
Theorem | suppssov1 8194* | Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) (Proof shortened by SN, 11-Apr-2025.) |
β’ (π β ((π₯ β π· β¦ π΄) supp π) β πΏ) & β’ ((π β§ π£ β π ) β (πππ£) = π) & β’ ((π β§ π₯ β π·) β π΄ β π) & β’ ((π β§ π₯ β π·) β π΅ β π ) & β’ (π β π β π) β β’ (π β ((π₯ β π· β¦ (π΄ππ΅)) supp π) β πΏ) | ||
Theorem | suppssov2 8195* | Formula building theorem for support restrictions: operator with right annihilator. (Contributed by SN, 11-Apr-2025.) |
β’ (π β ((π₯ β π· β¦ π΅) supp π) β πΏ) & β’ ((π β§ π£ β π ) β (π£ππ) = π) & β’ ((π β§ π₯ β π·) β π΄ β π ) & β’ ((π β§ π₯ β π·) β π΅ β π) & β’ (π β π β π) β β’ (π β ((π₯ β π· β¦ (π΄ππ΅)) supp π) β πΏ) | ||
Theorem | suppssof1 8196* | Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
β’ (π β (π΄ supp π) β πΏ) & β’ ((π β§ π£ β π ) β (πππ£) = π) & β’ (π β π΄:π·βΆπ) & β’ (π β π΅:π·βΆπ ) & β’ (π β π· β π) & β’ (π β π β π) β β’ (π β ((π΄ βf ππ΅) supp π) β πΏ) | ||
Theorem | suppss2 8197* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
β’ ((π β§ π β (π΄ β π)) β π΅ = π) & β’ (π β π΄ β π) β β’ (π β ((π β π΄ β¦ π΅) supp π) β π) | ||
Theorem | suppsssn 8198* | Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019.) |
β’ ((π β§ π β π΄ β§ π β π) β π΅ = π) & β’ (π β π΄ β π) β β’ (π β ((π β π΄ β¦ π΅) supp π) β {π}) | ||
Theorem | suppssfv 8199* | Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
β’ (π β ((π₯ β π· β¦ π΄) supp π) β πΏ) & β’ (π β (πΉβπ) = π) & β’ ((π β§ π₯ β π·) β π΄ β π) & β’ (π β π β π) β β’ (π β ((π₯ β π· β¦ (πΉβπ΄)) supp π) β πΏ) | ||
Theorem | suppofssd 8200 | Condition for the support of a function operation to be a subset of the union of the supports of the left and right function terms. (Contributed by Steven Nguyen, 28-Aug-2023.) |
β’ (π β π΄ β π) & β’ (π β π β π΅) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΊ:π΄βΆπ΅) & β’ (π β (πππ) = π) β β’ (π β ((πΉ βf ππΊ) supp π) β ((πΉ supp π) βͺ (πΊ supp π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |