![]() |
Intuitionistic Logic Explorer Theorem List (p. 70 of 135) | < 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 | isotilem 6901* | Lemma for isoti 6902. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ↔ (¬ 𝑥𝑆𝑦 ∧ ¬ 𝑦𝑆𝑥)) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))) | ||
Theorem | isoti 6902* | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) ↔ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑆𝑣 ∧ ¬ 𝑣𝑆𝑢)))) | ||
Theorem | supisolem 6903* | Lemma for supisoti 6905. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) | ||
Theorem | supisoex 6904* | Lemma for supisoti 6905. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))) | ||
Theorem | supisoti 6905* | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) & ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅))) | ||
Theorem | infeq1 6906 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1d 6907 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1i 6908 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) | ||
Theorem | infeq2 6909 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅)) | ||
Theorem | infeq3 6910 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆)) | ||
Theorem | infeq123d 6911 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfinf 6912 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅) | ||
Theorem | cnvinfex 6913* | Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
Theorem | cnvti 6914* | 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 6915* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqinftid 6916* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | infvalti 6917* | Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))) | ||
Theorem | infclti 6918* | An infimum belongs to its base class (closure law). See also inflbti 6919 and infglbti 6920. (Contributed by Jim Kingdon, 17-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | inflbti 6919* | An infimum is a lower bound. See also infclti 6918 and infglbti 6920. (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅))) | ||
Theorem | infglbti 6920* | An infimum is the greatest lower bound. See also infclti 6918 and inflbti 6919. (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infnlbti 6921* | A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | infminti 6922* | 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 6923* | Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | infeuti 6924* | An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | infsnti 6925* | The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → inf({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | inf00 6926 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ inf(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | infisoti 6927* | Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅))) | ||
Theorem | ordiso2 6928 | Generalize ordiso 6929 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ordiso 6929* | 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 6930 | Extend class notation to include disjoint union of two classes. |
class (𝐴 ⊔ 𝐵) | ||
Definition | df-dju 6931 | 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 6932 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐷)) | ||
Theorem | djueq1 6933 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐶)) | ||
Theorem | djueq2 6934 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊔ 𝐴) = (𝐶 ⊔ 𝐵)) | ||
Theorem | nfdju 6935 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ⊔ 𝐵) | ||
Theorem | djuex 6936 | The disjoint union of sets is a set. See also the more precise djuss 6963. (Contributed by AV, 28-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ∈ V) | ||
Theorem | djuexb 6937 | 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 6938 | Extend class notation to include left injection of a disjoint union. |
class inl | ||
Syntax | cinr 6939 | Extend class notation to include right injection of a disjoint union. |
class inr | ||
Definition | df-inl 6940 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
⊢ inl = (𝑥 ∈ V ↦ 〈∅, 𝑥〉) | ||
Definition | df-inr 6941 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
⊢ inr = (𝑥 ∈ V ↦ 〈1o, 𝑥〉) | ||
Theorem | djulclr 6942 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djurclr 6943 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐵 → ((inr ↾ 𝐵)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djulcl 6944 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
⊢ (𝐶 ∈ 𝐴 → (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djurcl 6945 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
⊢ (𝐶 ∈ 𝐵 → (inr‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djuf1olem 6946* | Lemma for djulf1o 6951 and djurf1o 6952. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 〈𝑋, 𝑥〉) ⇒ ⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) | ||
Theorem | djuf1olemr 6947* | Lemma for djulf1or 6949 and djurf1or 6950. For a version of this lemma with 𝐹 defined on 𝐴 and no restriction in the conclusion, see djuf1olem 6946. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ V ↦ 〈𝑋, 𝑥〉) ⇒ ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→({𝑋} × 𝐴) | ||
Theorem | djulclb 6948 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ 𝐴 ↔ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵))) | ||
Theorem | djulf1or 6949 | 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 6950 | 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 6951 | 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 6952 | 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 6953* | Lemma for inlresf1 6954 and inrresf1 6955. (Contributed by BJ, 4-Jul-2022.) |
⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) & ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴–1-1→𝐵 | ||
Theorem | inlresf1 6954 | 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 6955 | 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 6956 | 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 6986 and djufun 6997) while the simpler statement ⊢ (ran inl ∩ ran inr) = ∅ is easily recovered from it by substituting V for both 𝐴 and 𝐵 as done in casefun 6978). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
⊢ (ran (inl ↾ 𝐴) ∩ ran (inr ↾ 𝐵)) = ∅ | ||
Theorem | djuin 6957 | 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 6958 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((inl‘𝐴) = (inl‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | djuunr 6959 | 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 6960 | 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 6961* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝐶 = ((inl ↾ 𝐴)‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = ((inr ↾ 𝐵)‘𝑥))) | ||
Theorem | djur 6962* | 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 6963 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1o} × (𝐴 ∪ 𝐵)) | ||
Theorem | eldju1st 6964 | 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 6965 | 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 6966 | 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 6967 | The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inl‘𝑋)) = ∅) | ||
Theorem | 2ndinl 6968 | The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inl‘𝑋)) = 𝑋) | ||
Theorem | 1stinr 6969 | The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inr‘𝑋)) = 1o) | ||
Theorem | 2ndinr 6970 | The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.) |
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inr‘𝑋)) = 𝑋) | ||
Theorem | djune 6971 | Left and right injection never produce equal values. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (inl‘𝐴) ≠ (inr‘𝐵)) | ||
Theorem | updjudhf 6972* | 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 6973* | 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 6974* | 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 6975* | Universal property of the disjoint union. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐶) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → ∃!ℎ(ℎ:(𝐴 ⊔ 𝐵)⟶𝐶 ∧ (ℎ ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (ℎ ∘ (inr ↾ 𝐵)) = 𝐺)) | ||
Syntax | cdjucase 6976 | Syntax for the "case" construction. |
class case(𝑅, 𝑆) | ||
Definition | df-case 6977 | 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 6975. 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 6978 | The "case" construction of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun case(𝐹, 𝐺)) | ||
Theorem | casedm 6979 | 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 6980 | 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 6981 | The "case" construction of two functions is a function on the disjoint union of their domains. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝑋) & ⊢ (𝜑 → 𝐺:𝐵⟶𝑋) ⇒ ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)⟶𝑋) | ||
Theorem | caseinj 6982 | The "case" construction of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun ◡𝑅) & ⊢ (𝜑 → Fun ◡𝑆) & ⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅) ⇒ ⊢ (𝜑 → Fun ◡case(𝑅, 𝑆)) | ||
Theorem | casef1 6983 | The "case" construction of two injective functions with disjoint ranges is an injective function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴–1-1→𝑋) & ⊢ (𝜑 → 𝐺:𝐵–1-1→𝑋) & ⊢ (𝜑 → (ran 𝐹 ∩ ran 𝐺) = ∅) ⇒ ⊢ (𝜑 → case(𝐹, 𝐺):(𝐴 ⊔ 𝐵)–1-1→𝑋) | ||
Theorem | caseinl 6984 | Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.) |
⊢ (𝜑 → 𝐹 Fn 𝐵) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (case(𝐹, 𝐺)‘(inl‘𝐴)) = (𝐹‘𝐴)) | ||
Theorem | caseinr 6985 | Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (case(𝐹, 𝐺)‘(inr‘𝐴)) = (𝐺‘𝐴)) | ||
Theorem | djudom 6986 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → (𝐴 ⊔ 𝐶) ≼ (𝐵 ⊔ 𝐷)) | ||
Theorem | omp1eomlem 6987* | Lemma for omp1eom 6988. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ 𝐹 = (𝑥 ∈ ω ↦ if(𝑥 = ∅, (inr‘𝑥), (inl‘∪ 𝑥))) & ⊢ 𝑆 = (𝑥 ∈ ω ↦ suc 𝑥) & ⊢ 𝐺 = case(𝑆, ( I ↾ 1o)) ⇒ ⊢ 𝐹:ω–1-1-onto→(ω ⊔ 1o) | ||
Theorem | omp1eom 6988 | Adding one to ω. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊢ (ω ⊔ 1o) ≈ ω | ||
Theorem | endjusym 6989 | Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ≈ (𝐵 ⊔ 𝐴)) | ||
Theorem | eninl 6990 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (inl “ 𝐴) ≈ 𝐴) | ||
Theorem | eninr 6991 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ (𝐴 ∈ 𝑉 → (inr “ 𝐴) ≈ 𝐴) | ||
Theorem | difinfsnlem 6992* | Lemma for difinfsn 6993. The case where we need to swap 𝐵 and (inr‘∅) in building the mapping 𝐺. (Contributed by Jim Kingdon, 9-Aug-2023.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(ω ⊔ 1o)–1-1→𝐴) & ⊢ (𝜑 → (𝐹‘(inr‘∅)) ≠ 𝐵) & ⊢ 𝐺 = (𝑛 ∈ ω ↦ if((𝐹‘(inl‘𝑛)) = 𝐵, (𝐹‘(inr‘∅)), (𝐹‘(inl‘𝑛)))) ⇒ ⊢ (𝜑 → 𝐺:ω–1-1→(𝐴 ∖ {𝐵})) | ||
Theorem | difinfsn 6993* | An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴 ∧ 𝐵 ∈ 𝐴) → ω ≼ (𝐴 ∖ {𝐵})) | ||
Theorem | difinfinf 6994* | An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ∈ Fin)) → ω ≼ (𝐴 ∖ 𝐵)) | ||
Syntax | cdjud 6995 | Syntax for the domain-disjoint-union of two relations. |
class (𝑅 ⊔d 𝑆) | ||
Definition | df-djud 6996 |
The "domain-disjoint-union" of two relations: if 𝑅 ⊆ (𝐴 × 𝑋) and
𝑆
⊆ (𝐵 × 𝑋) are two binary
relations, then (𝑅 ⊔d 𝑆) is the
binary relation from (𝐴 ⊔ 𝐵) to 𝑋 having the universal
property of disjoint unions (see updjud 6975 in the case of functions).
Remark: the restrictions to dom 𝑅 (resp. dom 𝑆) are not necessary since extra stuff would be thrown away in the post-composition with 𝑅 (resp. 𝑆), as in df-case 6977, but they are explicitly written for clarity. (Contributed by MC and BJ, 10-Jul-2022.) |
⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆))) | ||
Theorem | djufun 6997 | The "domain-disjoint-union" of two functions is a function. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → Fun 𝐺) ⇒ ⊢ (𝜑 → Fun (𝐹 ⊔d 𝐺)) | ||
Theorem | djudm 6998 | The domain of the "domain-disjoint-union" is the disjoint union of the domains. Remark: its range is the (standard) union of the ranges. (Contributed by BJ, 10-Jul-2022.) |
⊢ dom (𝐹 ⊔d 𝐺) = (dom 𝐹 ⊔ dom 𝐺) | ||
Theorem | djuinj 6999 | The "domain-disjoint-union" of two injective relations with disjoint ranges is an injective relation. (Contributed by BJ, 10-Jul-2022.) |
⊢ (𝜑 → Fun ◡𝑅) & ⊢ (𝜑 → Fun ◡𝑆) & ⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅) ⇒ ⊢ (𝜑 → Fun ◡(𝑅 ⊔d 𝑆)) | ||
Theorem | 0ct 7000 | The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊢ ∃𝑓 𝑓:ω–onto→(∅ ⊔ 1o) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |