![]() |
Intuitionistic Logic Explorer Theorem List (p. 71 of 153) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | csup 7001 | 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 7002 | 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 7003* | Define the supremum of class π΄. It is meaningful when π is a relation that strictly orders π΅ and when the supremum exists. (Contributed by NM, 22-May-1999.) |
β’ sup(π΄, π΅, π ) = βͺ {π₯ β π΅ β£ (βπ¦ β π΄ Β¬ π₯π π¦ β§ βπ¦ β π΅ (π¦π π₯ β βπ§ β π΄ π¦π π§))} | ||
Definition | df-inf 7004 | 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 | supeq1 7005 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
β’ (π΅ = πΆ β sup(π΅, π΄, π ) = sup(πΆ, π΄, π )) | ||
Theorem | supeq1d 7006 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ (π β π΅ = πΆ) β β’ (π β sup(π΅, π΄, π ) = sup(πΆ, π΄, π )) | ||
Theorem | supeq1i 7007 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ π΅ = πΆ β β’ sup(π΅, π΄, π ) = sup(πΆ, π΄, π ) | ||
Theorem | supeq2 7008 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΅ = πΆ β sup(π΄, π΅, π ) = sup(π΄, πΆ, π )) | ||
Theorem | supeq3 7009 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β sup(π΄, π΅, π ) = sup(π΄, π΅, π)) | ||
Theorem | supeq123d 7010 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β sup(π΄, π΅, πΆ) = sup(π·, πΈ, πΉ)) | ||
Theorem | nfsup 7011 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯sup(π΄, π΅, π ) | ||
Theorem | supmoti 7012* | Any class π΅ has at most one supremum in π΄ (where π is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 8057) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β β*π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) | ||
Theorem | supeuti 7013* | A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by Jim Kingdon, 23-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β β!π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) | ||
Theorem | supval2ti 7014* | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β sup(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§)))) | ||
Theorem | eqsupti 7015* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ πΆπ π¦ β§ βπ¦ β π΄ (π¦π πΆ β βπ§ β π΅ π¦π π§)) β sup(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqsuptid 7016* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ πΆπ π¦) & β’ ((π β§ (π¦ β π΄ β§ π¦π πΆ)) β βπ§ β π΅ π¦π π§) β β’ (π β sup(π΅, π΄, π ) = πΆ) | ||
Theorem | supclti 7017* | A supremum belongs to its base class (closure law). See also supubti 7018 and suplubti 7019. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β sup(π΅, π΄, π ) β π΄) | ||
Theorem | supubti 7018* |
A supremum is an upper bound. See also supclti 7017 and suplubti 7019.
This proof demonstrates how to expand an iota-based definition (df-iota 5193) using riotacl2 5861. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β (πΆ β π΅ β Β¬ sup(π΅, π΄, π )π πΆ)) | ||
Theorem | suplubti 7019* | A supremum is the least upper bound. See also supclti 7017 and supubti 7018. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β ((πΆ β π΄ β§ πΆπ sup(π΅, π΄, π )) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | suplub2ti 7020* | Bidirectional form of suplubti 7019. (Contributed by Jim Kingdon, 17-Jan-2022.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) & β’ (π β π Or π΄) & β’ (π β π΅ β π΄) β β’ ((π β§ πΆ β π΄) β (πΆπ sup(π΅, π΄, π ) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | supelti 7021* | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β πΆ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) & β’ (π β πΆ β π΄) β β’ (π β sup(π΅, π΄, π ) β πΆ) | ||
Theorem | sup00 7022 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
β’ sup(π΅, β , π ) = β | ||
Theorem | supmaxti 7023* | 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 Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β πΆ β π΄) & β’ (π β πΆ β π΅) & β’ ((π β§ π¦ β π΅) β Β¬ πΆπ π¦) β β’ (π β sup(π΅, π΄, π ) = πΆ) | ||
Theorem | supsnti 7024* | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β π΅ β π΄) β β’ (π β sup({π΅}, π΄, π ) = π΅) | ||
Theorem | isotilem 7025* | Lemma for isoti 7026. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ (πΉ Isom π , π (π΄, π΅) β (βπ₯ β π΅ βπ¦ β π΅ (π₯ = π¦ β (Β¬ π₯ππ¦ β§ Β¬ π¦ππ₯)) β βπ’ β π΄ βπ£ β π΄ (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’)))) | ||
Theorem | isoti 7026* | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ (πΉ Isom π , π (π΄, π΅) β (βπ’ β π΄ βπ£ β π΄ (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’)) β βπ’ β π΅ βπ£ β π΅ (π’ = π£ β (Β¬ π’ππ£ β§ Β¬ π£ππ’)))) | ||
Theorem | supisolem 7027* | Lemma for supisoti 7029. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) β β’ ((π β§ π· β π΄) β ((βπ¦ β πΆ Β¬ π·π π¦ β§ βπ¦ β π΄ (π¦π π· β βπ§ β πΆ π¦π π§)) β (βπ€ β (πΉ β πΆ) Β¬ (πΉβπ·)ππ€ β§ βπ€ β π΅ (π€π(πΉβπ·) β βπ£ β (πΉ β πΆ)π€ππ£)))) | ||
Theorem | supisoex 7028* | Lemma for supisoti 7029. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) β β’ (π β βπ’ β π΅ (βπ€ β (πΉ β πΆ) Β¬ π’ππ€ β§ βπ€ β π΅ (π€ππ’ β βπ£ β (πΉ β πΆ)π€ππ£))) | ||
Theorem | supisoti 7029* | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) & β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β sup((πΉ β πΆ), π΅, π) = (πΉβsup(πΆ, π΄, π ))) | ||
Theorem | infeq1 7030 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1d 7031 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1i 7032 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ π΅ = πΆ β β’ inf(π΅, π΄, π ) = inf(πΆ, π΄, π ) | ||
Theorem | infeq2 7033 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΄, π΅, π ) = inf(π΄, πΆ, π )) | ||
Theorem | infeq3 7034 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π = π β inf(π΄, π΅, π ) = inf(π΄, π΅, π)) | ||
Theorem | infeq123d 7035 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β inf(π΄, π΅, πΆ) = inf(π·, πΈ, πΉ)) | ||
Theorem | nfinf 7036 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯inf(π΄, π΅, π ) | ||
Theorem | cnvinfex 7037* | Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.) |
β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΄ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§))) | ||
Theorem | cnvti 7038* | If a relation satisfies a condition corresponding to tightness of an apartness generated by an order, so does its converse. (Contributed by Jim Kingdon, 17-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’β‘π π£ β§ Β¬ π£β‘π π’))) | ||
Theorem | eqinfti 7039* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ π¦π πΆ β§ βπ¦ β π΄ (πΆπ π¦ β βπ§ β π΅ π§π π¦)) β inf(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqinftid 7040* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ π¦π πΆ) & β’ ((π β§ (π¦ β π΄ β§ πΆπ π¦)) β βπ§ β π΅ π§π π¦) β β’ (π β inf(π΅, π΄, π ) = πΆ) | ||
Theorem | infvalti 7041* | Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β inf(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦)))) | ||
Theorem | infclti 7042* | An infimum belongs to its base class (closure law). See also inflbti 7043 and infglbti 7044. (Contributed by Jim Kingdon, 17-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β inf(π΅, π΄, π ) β π΄) | ||
Theorem | inflbti 7043* | An infimum is a lower bound. See also infclti 7042 and infglbti 7044. (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β (πΆ β π΅ β Β¬ πΆπ inf(π΅, π΄, π ))) | ||
Theorem | infglbti 7044* | An infimum is the greatest lower bound. See also infclti 7042 and inflbti 7043. (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ inf(π΅, π΄, π )π πΆ) β βπ§ β π΅ π§π πΆ)) | ||
Theorem | infnlbti 7045* | A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ βπ§ β π΅ Β¬ π§π πΆ) β Β¬ inf(π΅, π΄, π )π πΆ)) | ||
Theorem | infminti 7046* | 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 Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β πΆ β π΄) & β’ (π β πΆ β π΅) & β’ ((π β§ π¦ β π΅) β Β¬ π¦π πΆ) β β’ (π β inf(π΅, π΄, π ) = πΆ) | ||
Theorem | infmoti 7047* | Any class π΅ has at most one infimum in π΄ (where π is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β β*π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | infeuti 7048* | An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β β!π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | infsnti 7049* | The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β π΅ β π΄) β β’ (π β inf({π΅}, π΄, π ) = π΅) | ||
Theorem | inf00 7050 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
β’ inf(π΅, β , π ) = β | ||
Theorem | infisoti 7051* | Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β πΆ π§π π¦))) & β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β inf((πΉ β πΆ), π΅, π) = (πΉβinf(πΆ, π΄, π ))) | ||
Theorem | supex2g 7052 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β πΆ β sup(π΅, π΄, π ) β V) | ||
Theorem | infex2g 7053 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
β’ (π΄ β πΆ β inf(π΅, π΄, π ) β V) | ||
Theorem | ordiso2 7054 | Generalize ordiso 7055 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄ β§ Ord π΅) β π΄ = π΅) | ||
Theorem | ordiso 7055* | Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.) (Proof shortened by Mario Carneiro, 24-Jun-2015.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ = π΅ β βπ π Isom E , E (π΄, π΅))) | ||
Syntax | cdju 7056 | Extend class notation to include disjoint union of two classes. |
class (π΄ β π΅) | ||
Definition | df-dju 7057 | Disjoint union of two classes. This is a way of creating a class which contains elements corresponding to each element of π΄ or π΅, tagging each one with whether it came from π΄ or π΅. (Contributed by Jim Kingdon, 20-Jun-2022.) |
β’ (π΄ β π΅) = (({β } Γ π΄) βͺ ({1o} Γ π΅)) | ||
Theorem | djueq12 7058 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ ((π΄ = π΅ β§ πΆ = π·) β (π΄ β πΆ) = (π΅ β π·)) | ||
Theorem | djueq1 7059 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ (π΄ = π΅ β (π΄ β πΆ) = (π΅ β πΆ)) | ||
Theorem | djueq2 7060 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ (π΄ = π΅ β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | nfdju 7061 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯(π΄ β π΅) | ||
Theorem | djuex 7062 | The disjoint union of sets is a set. See also the more precise djuss 7089. (Contributed by AV, 28-Jun-2022.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ β π΅) β V) | ||
Theorem | djuexb 7063 | The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.) |
β’ ((π΄ β V β§ π΅ β V) β (π΄ β π΅) β V) | ||
In this section, we define the left and right injections of a disjoint union and prove their main properties. These injections are restrictions of the "template" functions inl and inr, which appear in most applications in the form (inl βΎ π΄) and (inr βΎ π΅). | ||
Syntax | cinl 7064 | Extend class notation to include left injection of a disjoint union. |
class inl | ||
Syntax | cinr 7065 | Extend class notation to include right injection of a disjoint union. |
class inr | ||
Definition | df-inl 7066 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
β’ inl = (π₯ β V β¦ β¨β , π₯β©) | ||
Definition | df-inr 7067 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
β’ inr = (π₯ β V β¦ β¨1o, π₯β©) | ||
Theorem | djulclr 7068 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
β’ (πΆ β π΄ β ((inl βΎ π΄)βπΆ) β (π΄ β π΅)) | ||
Theorem | djurclr 7069 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
β’ (πΆ β π΅ β ((inr βΎ π΅)βπΆ) β (π΄ β π΅)) | ||
Theorem | djulcl 7070 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
β’ (πΆ β π΄ β (inlβπΆ) β (π΄ β π΅)) | ||
Theorem | djurcl 7071 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
β’ (πΆ β π΅ β (inrβπΆ) β (π΄ β π΅)) | ||
Theorem | djuf1olem 7072* | Lemma for djulf1o 7077 and djurf1o 7078. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
β’ π β V & β’ πΉ = (π₯ β π΄ β¦ β¨π, π₯β©) β β’ πΉ:π΄β1-1-ontoβ({π} Γ π΄) | ||
Theorem | djuf1olemr 7073* | Lemma for djulf1or 7075 and djurf1or 7076. For a version of this lemma with πΉ defined on π΄ and no restriction in the conclusion, see djuf1olem 7072. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
β’ π β V & β’ πΉ = (π₯ β V β¦ β¨π, π₯β©) β β’ (πΉ βΎ π΄):π΄β1-1-ontoβ({π} Γ π΄) | ||
Theorem | djulclb 7074 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
β’ (πΆ β π β (πΆ β π΄ β (inlβπΆ) β (π΄ β π΅))) | ||
Theorem | djulf1or 7075 | The left injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
β’ (inl βΎ π΄):π΄β1-1-ontoβ({β } Γ π΄) | ||
Theorem | djurf1or 7076 | The right injection function on all sets is one to one and onto. (Contributed by BJ and Jim Kingdon, 22-Jun-2022.) |
β’ (inr βΎ π΄):π΄β1-1-ontoβ({1o} Γ π΄) | ||
Theorem | djulf1o 7077 | The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
β’ inl:Vβ1-1-ontoβ({β } Γ V) | ||
Theorem | djurf1o 7078 | The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.) |
β’ inr:Vβ1-1-ontoβ({1o} Γ V) | ||
Theorem | inresflem 7079* | Lemma for inlresf1 7080 and inrresf1 7081. (Contributed by BJ, 4-Jul-2022.) |
β’ πΉ:π΄β1-1-ontoβ({π} Γ π΄) & β’ (π₯ β π΄ β (πΉβπ₯) β π΅) β β’ πΉ:π΄β1-1βπ΅ | ||
Theorem | inlresf1 7080 | The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
β’ (inl βΎ π΄):π΄β1-1β(π΄ β π΅) | ||
Theorem | inrresf1 7081 | The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.) |
β’ (inr βΎ π΅):π΅β1-1β(π΄ β π΅) | ||
Theorem | djuinr 7082 | The ranges of any left and right injections are disjoint. Remark: the extra generality offered by the two restrictions makes the theorem more readily usable (e.g., by djudom 7112 and djufun 7123) while the simpler statement β’ (ran inl β© ran inr) = β is easily recovered from it by substituting V for both π΄ and π΅ as done in casefun 7104). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
β’ (ran (inl βΎ π΄) β© ran (inr βΎ π΅)) = β | ||
Theorem | djuin 7083 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
β’ ((inl β π΄) β© (inr β π΅)) = β | ||
Theorem | inl11 7084 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
β’ ((π΄ β π β§ π΅ β π) β ((inlβπ΄) = (inlβπ΅) β π΄ = π΅)) | ||
Theorem | djuunr 7085 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 6-Jul-2022.) |
β’ (ran (inl βΎ π΄) βͺ ran (inr βΎ π΅)) = (π΄ β π΅) | ||
Theorem | djuun 7086 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
β’ ((inl β π΄) βͺ (inr β π΅)) = (π΄ β π΅) | ||
Theorem | eldju 7087* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
β’ (πΆ β (π΄ β π΅) β (βπ₯ β π΄ πΆ = ((inl βΎ π΄)βπ₯) β¨ βπ₯ β π΅ πΆ = ((inr βΎ π΅)βπ₯))) | ||
Theorem | djur 7088* | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.) |
β’ (πΆ β (π΄ β π΅) β (βπ₯ β π΄ πΆ = (inlβπ₯) β¨ βπ₯ β π΅ πΆ = (inrβπ₯))) | ||
Theorem | djuss 7089 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
β’ (π΄ β π΅) β ({β , 1o} Γ (π΄ βͺ π΅)) | ||
Theorem | eldju1st 7090 | The first component of an element of a disjoint union is either β or 1o. (Contributed by AV, 26-Jun-2022.) |
β’ (π β (π΄ β π΅) β ((1st βπ) = β β¨ (1st βπ) = 1o)) | ||
Theorem | eldju2ndl 7091 | The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.) |
β’ ((π β (π΄ β π΅) β§ (1st βπ) = β ) β (2nd βπ) β π΄) | ||
Theorem | eldju2ndr 7092 | The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.) |
β’ ((π β (π΄ β π΅) β§ (1st βπ) β β ) β (2nd βπ) β π΅) | ||
Theorem | 1stinl 7093 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (1st β(inlβπ)) = β ) | ||
Theorem | 2ndinl 7094 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (2nd β(inlβπ)) = π) | ||
Theorem | 1stinr 7095 | The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (1st β(inrβπ)) = 1o) | ||
Theorem | 2ndinr 7096 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (2nd β(inrβπ)) = π) | ||
Theorem | djune 7097 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
β’ ((π΄ β π β§ π΅ β π) β (inlβπ΄) β (inrβπ΅)) | ||
Theorem | updjudhf 7098* | The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ π» = (π₯ β (π΄ β π΅) β¦ if((1st βπ₯) = β , (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯)))) β β’ (π β π»:(π΄ β π΅)βΆπΆ) | ||
Theorem | updjudhcoinlf 7099* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ π» = (π₯ β (π΄ β π΅) β¦ if((1st βπ₯) = β , (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯)))) β β’ (π β (π» β (inl βΎ π΄)) = πΉ) | ||
Theorem | updjudhcoinrg 7100* | The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ π» = (π₯ β (π΄ β π΅) β¦ if((1st βπ₯) = β , (πΉβ(2nd βπ₯)), (πΊβ(2nd βπ₯)))) β β’ (π β (π» β (inr βΎ π΅)) = πΊ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |