![]() |
Intuitionistic Logic Explorer Theorem List (p. 71 of 152) | < 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 | ||
Theorem | supeq2 7001 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΅ = πΆ β sup(π΄, π΅, π ) = sup(π΄, πΆ, π )) | ||
Theorem | supeq3 7002 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
β’ (π = π β sup(π΄, π΅, π ) = sup(π΄, π΅, π)) | ||
Theorem | supeq123d 7003 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β sup(π΄, π΅, πΆ) = sup(π·, πΈ, πΉ)) | ||
Theorem | nfsup 7004 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯sup(π΄, π΅, π ) | ||
Theorem | supmoti 7005* | Any class π΅ has at most one supremum in π΄ (where π is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 8050) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β β*π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) | ||
Theorem | supeuti 7006* | 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 7007* | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β sup(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§)))) | ||
Theorem | eqsupti 7008* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ πΆπ π¦ β§ βπ¦ β π΄ (π¦π πΆ β βπ§ β π΅ π¦π π§)) β sup(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqsuptid 7009* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ πΆπ π¦) & β’ ((π β§ (π¦ β π΄ β§ π¦π πΆ)) β βπ§ β π΅ π¦π π§) β β’ (π β sup(π΅, π΄, π ) = πΆ) | ||
Theorem | supclti 7010* | A supremum belongs to its base class (closure law). See also supubti 7011 and suplubti 7012. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β sup(π΅, π΄, π ) β π΄) | ||
Theorem | supubti 7011* |
A supremum is an upper bound. See also supclti 7010 and suplubti 7012.
This proof demonstrates how to expand an iota-based definition (df-iota 5190) using riotacl2 5857. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β (πΆ β π΅ β Β¬ sup(π΅, π΄, π )π πΆ)) | ||
Theorem | suplubti 7012* | A supremum is the least upper bound. See also supclti 7010 and supubti 7011. (Contributed by Jim Kingdon, 24-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) β β’ (π β ((πΆ β π΄ β§ πΆπ sup(π΅, π΄, π )) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | suplub2ti 7013* | Bidirectional form of suplubti 7012. (Contributed by Jim Kingdon, 17-Jan-2022.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) & β’ (π β π Or π΄) & β’ (π β π΅ β π΄) β β’ ((π β§ πΆ β π΄) β (πΆπ sup(π΅, π΄, π ) β βπ§ β π΅ πΆπ π§)) | ||
Theorem | supelti 7014* | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β πΆ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) & β’ (π β πΆ β π΄) β β’ (π β sup(π΅, π΄, π ) β πΆ) | ||
Theorem | sup00 7015 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
β’ sup(π΅, β , π ) = β | ||
Theorem | supmaxti 7016* | 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 7017* | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β π΅ β π΄) β β’ (π β sup({π΅}, π΄, π ) = π΅) | ||
Theorem | isotilem 7018* | Lemma for isoti 7019. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ (πΉ Isom π , π (π΄, π΅) β (βπ₯ β π΅ βπ¦ β π΅ (π₯ = π¦ β (Β¬ π₯ππ¦ β§ Β¬ π¦ππ₯)) β βπ’ β π΄ βπ£ β π΄ (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’)))) | ||
Theorem | isoti 7019* | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ (πΉ Isom π , π (π΄, π΅) β (βπ’ β π΄ βπ£ β π΄ (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’)) β βπ’ β π΅ βπ£ β π΅ (π’ = π£ β (Β¬ π’ππ£ β§ Β¬ π£ππ’)))) | ||
Theorem | supisolem 7020* | Lemma for supisoti 7022. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) β β’ ((π β§ π· β π΄) β ((βπ¦ β πΆ Β¬ π·π π¦ β§ βπ¦ β π΄ (π¦π π· β βπ§ β πΆ π¦π π§)) β (βπ€ β (πΉ β πΆ) Β¬ (πΉβπ·)ππ€ β§ βπ€ β π΅ (π€π(πΉβπ·) β βπ£ β (πΉ β πΆ)π€ππ£)))) | ||
Theorem | supisoex 7021* | Lemma for supisoti 7022. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) β β’ (π β βπ’ β π΅ (βπ€ β (πΉ β πΆ) Β¬ π’ππ€ β§ βπ€ β π΅ (π€ππ’ β βπ£ β (πΉ β πΆ)π€ππ£))) | ||
Theorem | supisoti 7022* | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) & β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β sup((πΉ β πΆ), π΅, π) = (πΉβsup(πΆ, π΄, π ))) | ||
Theorem | infeq1 7023 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1d 7024 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β inf(π΅, π΄, π ) = inf(πΆ, π΄, π )) | ||
Theorem | infeq1i 7025 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ π΅ = πΆ β β’ inf(π΅, π΄, π ) = inf(πΆ, π΄, π ) | ||
Theorem | infeq2 7026 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π΅ = πΆ β inf(π΄, π΅, π ) = inf(π΄, πΆ, π )) | ||
Theorem | infeq3 7027 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π = π β inf(π΄, π΅, π ) = inf(π΄, π΅, π)) | ||
Theorem | infeq123d 7028 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ (π β π΄ = π·) & β’ (π β π΅ = πΈ) & β’ (π β πΆ = πΉ) β β’ (π β inf(π΄, π΅, πΆ) = inf(π·, πΈ, πΉ)) | ||
Theorem | nfinf 7029 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
β’ β²π₯π΄ & β’ β²π₯π΅ & β’ β²π₯π β β’ β²π₯inf(π΄, π΅, π ) | ||
Theorem | cnvinfex 7030* | Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.) |
β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯β‘π π¦ β§ βπ¦ β π΄ (π¦β‘π π₯ β βπ§ β π΅ π¦β‘π π§))) | ||
Theorem | cnvti 7031* | 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 7032* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β ((πΆ β π΄ β§ βπ¦ β π΅ Β¬ π¦π πΆ β§ βπ¦ β π΄ (πΆπ π¦ β βπ§ β π΅ π§π π¦)) β inf(π΅, π΄, π ) = πΆ)) | ||
Theorem | eqinftid 7033* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β πΆ β π΄) & β’ ((π β§ π¦ β π΅) β Β¬ π¦π πΆ) & β’ ((π β§ (π¦ β π΄ β§ πΆπ π¦)) β βπ§ β π΅ π§π π¦) β β’ (π β inf(π΅, π΄, π ) = πΆ) | ||
Theorem | infvalti 7034* | Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β inf(π΅, π΄, π ) = (β©π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦)))) | ||
Theorem | infclti 7035* | An infimum belongs to its base class (closure law). See also inflbti 7036 and infglbti 7037. (Contributed by Jim Kingdon, 17-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β inf(π΅, π΄, π ) β π΄) | ||
Theorem | inflbti 7036* | An infimum is a lower bound. See also infclti 7035 and infglbti 7037. (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β (πΆ β π΅ β Β¬ πΆπ inf(π΅, π΄, π ))) | ||
Theorem | infglbti 7037* | An infimum is the greatest lower bound. See also infclti 7035 and inflbti 7036. (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ inf(π΅, π΄, π )π πΆ) β βπ§ β π΅ π§π πΆ)) | ||
Theorem | infnlbti 7038* | A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β ((πΆ β π΄ β§ βπ§ β π΅ Β¬ π§π πΆ) β Β¬ inf(π΅, π΄, π )π πΆ)) | ||
Theorem | infminti 7039* | 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 7040* | Any class π΅ has at most one infimum in π΄ (where π is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β β*π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | infeuti 7041* | An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β β!π₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) | ||
Theorem | infsnti 7042* | The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.) |
β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) & β’ (π β π΅ β π΄) β β’ (π β inf({π΅}, π΄, π ) = π΅) | ||
Theorem | inf00 7043 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
β’ inf(π΅, β , π ) = β | ||
Theorem | infisoti 7044* | Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.) |
β’ (π β πΉ Isom π , π (π΄, π΅)) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β πΆ π§π π¦))) & β’ ((π β§ (π’ β π΄ β§ π£ β π΄)) β (π’ = π£ β (Β¬ π’π π£ β§ Β¬ π£π π’))) β β’ (π β inf((πΉ β πΆ), π΅, π) = (πΉβinf(πΆ, π΄, π ))) | ||
Theorem | supex2g 7045 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β πΆ β sup(π΅, π΄, π ) β V) | ||
Theorem | infex2g 7046 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
β’ (π΄ β πΆ β inf(π΅, π΄, π ) β V) | ||
Theorem | ordiso2 7047 | Generalize ordiso 7048 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
β’ ((πΉ Isom E , E (π΄, π΅) β§ Ord π΄ β§ Ord π΅) β π΄ = π΅) | ||
Theorem | ordiso 7048* | 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 7049 | Extend class notation to include disjoint union of two classes. |
class (π΄ β π΅) | ||
Definition | df-dju 7050 | 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 7051 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ ((π΄ = π΅ β§ πΆ = π·) β (π΄ β πΆ) = (π΅ β π·)) | ||
Theorem | djueq1 7052 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ (π΄ = π΅ β (π΄ β πΆ) = (π΅ β πΆ)) | ||
Theorem | djueq2 7053 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ (π΄ = π΅ β (πΆ β π΄) = (πΆ β π΅)) | ||
Theorem | nfdju 7054 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯(π΄ β π΅) | ||
Theorem | djuex 7055 | The disjoint union of sets is a set. See also the more precise djuss 7082. (Contributed by AV, 28-Jun-2022.) |
β’ ((π΄ β π β§ π΅ β π) β (π΄ β π΅) β V) | ||
Theorem | djuexb 7056 | 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 7057 | Extend class notation to include left injection of a disjoint union. |
class inl | ||
Syntax | cinr 7058 | Extend class notation to include right injection of a disjoint union. |
class inr | ||
Definition | df-inl 7059 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
β’ inl = (π₯ β V β¦ β¨β , π₯β©) | ||
Definition | df-inr 7060 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
β’ inr = (π₯ β V β¦ β¨1o, π₯β©) | ||
Theorem | djulclr 7061 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
β’ (πΆ β π΄ β ((inl βΎ π΄)βπΆ) β (π΄ β π΅)) | ||
Theorem | djurclr 7062 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
β’ (πΆ β π΅ β ((inr βΎ π΅)βπΆ) β (π΄ β π΅)) | ||
Theorem | djulcl 7063 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
β’ (πΆ β π΄ β (inlβπΆ) β (π΄ β π΅)) | ||
Theorem | djurcl 7064 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
β’ (πΆ β π΅ β (inrβπΆ) β (π΄ β π΅)) | ||
Theorem | djuf1olem 7065* | Lemma for djulf1o 7070 and djurf1o 7071. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
β’ π β V & β’ πΉ = (π₯ β π΄ β¦ β¨π, π₯β©) β β’ πΉ:π΄β1-1-ontoβ({π} Γ π΄) | ||
Theorem | djuf1olemr 7066* | Lemma for djulf1or 7068 and djurf1or 7069. For a version of this lemma with πΉ defined on π΄ and no restriction in the conclusion, see djuf1olem 7065. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
β’ π β V & β’ πΉ = (π₯ β V β¦ β¨π, π₯β©) β β’ (πΉ βΎ π΄):π΄β1-1-ontoβ({π} Γ π΄) | ||
Theorem | djulclb 7067 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
β’ (πΆ β π β (πΆ β π΄ β (inlβπΆ) β (π΄ β π΅))) | ||
Theorem | djulf1or 7068 | 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 7069 | 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 7070 | 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 7071 | 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 7072* | Lemma for inlresf1 7073 and inrresf1 7074. (Contributed by BJ, 4-Jul-2022.) |
β’ πΉ:π΄β1-1-ontoβ({π} Γ π΄) & β’ (π₯ β π΄ β (πΉβπ₯) β π΅) β β’ πΉ:π΄β1-1βπ΅ | ||
Theorem | inlresf1 7073 | 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 7074 | 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 7075 | 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 7105 and djufun 7116) while the simpler statement β’ (ran inl β© ran inr) = β is easily recovered from it by substituting V for both π΄ and π΅ as done in casefun 7097). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
β’ (ran (inl βΎ π΄) β© ran (inr βΎ π΅)) = β | ||
Theorem | djuin 7076 | 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 7077 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
β’ ((π΄ β π β§ π΅ β π) β ((inlβπ΄) = (inlβπ΅) β π΄ = π΅)) | ||
Theorem | djuunr 7078 | 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 7079 | 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 7080* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
β’ (πΆ β (π΄ β π΅) β (βπ₯ β π΄ πΆ = ((inl βΎ π΄)βπ₯) β¨ βπ₯ β π΅ πΆ = ((inr βΎ π΅)βπ₯))) | ||
Theorem | djur 7081* | 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 7082 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
β’ (π΄ β π΅) β ({β , 1o} Γ (π΄ βͺ π΅)) | ||
Theorem | eldju1st 7083 | 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 7084 | 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 7085 | 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 7086 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (1st β(inlβπ)) = β ) | ||
Theorem | 2ndinl 7087 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (2nd β(inlβπ)) = π) | ||
Theorem | 1stinr 7088 | The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (1st β(inrβπ)) = 1o) | ||
Theorem | 2ndinr 7089 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
β’ (π β π β (2nd β(inrβπ)) = π) | ||
Theorem | djune 7090 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
β’ ((π΄ β π β§ π΅ β π) β (inlβπ΄) β (inrβπ΅)) | ||
Theorem | updjudhf 7091* | 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 7092* | 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 7093* | 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 βΎ π΅)) = πΊ) | ||
Theorem | updjud 7094* | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
β’ (π β πΉ:π΄βΆπΆ) & β’ (π β πΊ:π΅βΆπΆ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β β!β(β:(π΄ β π΅)βΆπΆ β§ (β β (inl βΎ π΄)) = πΉ β§ (β β (inr βΎ π΅)) = πΊ)) | ||
Syntax | cdjucase 7095 | Syntax for the "case" construction. |
class case(π , π) | ||
Definition | df-case 7096 | The "case" construction: if πΉ:π΄βΆπ and πΊ:π΅βΆπ are functions, then case(πΉ, πΊ):(π΄ β π΅)βΆπ is the natural function obtained by a definition by cases, hence the name. It is the unique function whose existence is asserted by the universal property of disjoint unions updjud 7094. The definition is adapted to make sense also for binary relations (where the universal property also holds). (Contributed by MC and BJ, 10-Jul-2022.) |
β’ case(π , π) = ((π β β‘inl) βͺ (π β β‘inr)) | ||
Theorem | casefun 7097 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
β’ (π β Fun πΉ) & β’ (π β Fun πΊ) β β’ (π β Fun case(πΉ, πΊ)) | ||
Theorem | casedm 7098 | The domain of the "case" construction is the disjoint union of the domains. TODO (although less important): β’ ran case(πΉ, πΊ) = (ran πΉ βͺ ran πΊ). (Contributed by BJ, 10-Jul-2022.) |
β’ dom case(πΉ, πΊ) = (dom πΉ β dom πΊ) | ||
Theorem | caserel 7099 | The "case" construction of two relations is a relation, with bounds on its domain and codomain. Typically, the "case" construction is used when both relations have a common codomain. (Contributed by BJ, 10-Jul-2022.) |
β’ case(π , π) β ((dom π β dom π) Γ (ran π βͺ ran π)) | ||
Theorem | casef 7100 | The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.) |
β’ (π β πΉ:π΄βΆπ) & β’ (π β πΊ:π΅βΆπ) β β’ (π β case(πΉ, πΊ):(π΄ β π΅)βΆπ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |