![]() |
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 | ||
Theorem | elfi2 7001* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥)) | ||
Theorem | elfir 7002 | Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵)) | ||
Theorem | ssfii 7003 | Any element of a set 𝐴 is the intersection of a finite subset of 𝐴. (Contributed by FL, 27-Apr-2008.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (fi‘𝐴)) | ||
Theorem | fi0 7004 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘∅) = ∅ | ||
Theorem | fieq0 7005 | A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = ∅ ↔ (fi‘𝐴) = ∅)) | ||
Theorem | fiss 7006 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵)) | ||
Theorem | fiuni 7007 | The union of the finite intersections of a set is simply the union of the set itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 = ∪ (fi‘𝐴)) | ||
Theorem | fipwssg 7008 | If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ 𝒫 𝑋) → (fi‘𝐴) ⊆ 𝒫 𝑋) | ||
Theorem | fifo 7009* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) | ||
Theorem | dcfi 7010* | Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∀𝑥 ∈ 𝐴 𝜑) | ||
Syntax | csup 7011 | 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 7012 | 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 7013* | 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 7014 | 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 7015 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1d 7016 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1i 7017 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) | ||
Theorem | supeq2 7018 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅)) | ||
Theorem | supeq3 7019 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆)) | ||
Theorem | supeq123d 7020 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfsup 7021 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅) | ||
Theorem | supmoti 7022* | Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 8067) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | supeuti 7023* | 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 7024* | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))) | ||
Theorem | eqsupti 7025* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqsuptid 7026* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | supclti 7027* | A supremum belongs to its base class (closure law). See also supubti 7028 and suplubti 7029. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supubti 7028* |
A supremum is an upper bound. See also supclti 7027 and suplubti 7029.
This proof demonstrates how to expand an iota-based definition (df-iota 5196) using riotacl2 5865. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | suplubti 7029* | A supremum is the least upper bound. See also supclti 7027 and supubti 7028. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | suplub2ti 7030* | Bidirectional form of suplubti 7029. (Contributed by Jim Kingdon, 17-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | supelti 7031* | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐶 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐶) | ||
Theorem | sup00 7032 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ sup(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | supmaxti 7033* | 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 7034* | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | isotilem 7035* | Lemma for isoti 7036. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ↔ (¬ 𝑥𝑆𝑦 ∧ ¬ 𝑦𝑆𝑥)) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))) | ||
Theorem | isoti 7036* | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) ↔ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑆𝑣 ∧ ¬ 𝑣𝑆𝑢)))) | ||
Theorem | supisolem 7037* | Lemma for supisoti 7039. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) | ||
Theorem | supisoex 7038* | Lemma for supisoti 7039. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))) | ||
Theorem | supisoti 7039* | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) & ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅))) | ||
Theorem | infeq1 7040 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1d 7041 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1i 7042 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) | ||
Theorem | infeq2 7043 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅)) | ||
Theorem | infeq3 7044 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆)) | ||
Theorem | infeq123d 7045 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfinf 7046 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅) | ||
Theorem | cnvinfex 7047* | Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
Theorem | cnvti 7048* | 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 7049* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqinftid 7050* | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | infvalti 7051* | Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))) | ||
Theorem | infclti 7052* | An infimum belongs to its base class (closure law). See also inflbti 7053 and infglbti 7054. (Contributed by Jim Kingdon, 17-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | inflbti 7053* | An infimum is a lower bound. See also infclti 7052 and infglbti 7054. (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅))) | ||
Theorem | infglbti 7054* | An infimum is the greatest lower bound. See also infclti 7052 and inflbti 7053. (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infnlbti 7055* | A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | infminti 7056* | 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 7057* | Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by Jim Kingdon, 18-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | infeuti 7058* | An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | infsnti 7059* | The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → inf({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | inf00 7060 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ inf(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | infisoti 7061* | Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅))) | ||
Theorem | supex2g 7062 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐴 ∈ 𝐶 → sup(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | infex2g 7063 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
⊢ (𝐴 ∈ 𝐶 → inf(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | ordiso2 7064 | Generalize ordiso 7065 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ordiso 7065* | 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 7066 | Extend class notation to include disjoint union of two classes. |
class (𝐴 ⊔ 𝐵) | ||
Definition | df-dju 7067 | 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 7068 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐷)) | ||
Theorem | djueq1 7069 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐴 = 𝐵 → (𝐴 ⊔ 𝐶) = (𝐵 ⊔ 𝐶)) | ||
Theorem | djueq2 7070 | Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐴 = 𝐵 → (𝐶 ⊔ 𝐴) = (𝐶 ⊔ 𝐵)) | ||
Theorem | nfdju 7071 | Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 ⊔ 𝐵) | ||
Theorem | djuex 7072 | The disjoint union of sets is a set. See also the more precise djuss 7099. (Contributed by AV, 28-Jun-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ∈ V) | ||
Theorem | djuexb 7073 | 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 7074 | Extend class notation to include left injection of a disjoint union. |
class inl | ||
Syntax | cinr 7075 | Extend class notation to include right injection of a disjoint union. |
class inr | ||
Definition | df-inl 7076 | Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
⊢ inl = (𝑥 ∈ V ↦ 〈∅, 𝑥〉) | ||
Definition | df-inr 7077 | Right injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022.) |
⊢ inr = (𝑥 ∈ V ↦ 〈1o, 𝑥〉) | ||
Theorem | djulclr 7078 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djurclr 7079 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) (Revised by BJ, 6-Jul-2022.) |
⊢ (𝐶 ∈ 𝐵 → ((inr ↾ 𝐵)‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djulcl 7080 | Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
⊢ (𝐶 ∈ 𝐴 → (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djurcl 7081 | Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.) |
⊢ (𝐶 ∈ 𝐵 → (inr‘𝐶) ∈ (𝐴 ⊔ 𝐵)) | ||
Theorem | djuf1olem 7082* | Lemma for djulf1o 7087 and djurf1o 7088. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 〈𝑋, 𝑥〉) ⇒ ⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) | ||
Theorem | djuf1olemr 7083* | Lemma for djulf1or 7085 and djurf1or 7086. For a version of this lemma with 𝐹 defined on 𝐴 and no restriction in the conclusion, see djuf1olem 7082. (Contributed by BJ and Jim Kingdon, 4-Jul-2022.) |
⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ V ↦ 〈𝑋, 𝑥〉) ⇒ ⊢ (𝐹 ↾ 𝐴):𝐴–1-1-onto→({𝑋} × 𝐴) | ||
Theorem | djulclb 7084 | Left biconditional closure of disjoint union. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ 𝐴 ↔ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵))) | ||
Theorem | djulf1or 7085 | 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 7086 | 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 7087 | 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 7088 | 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 7089* | Lemma for inlresf1 7090 and inrresf1 7091. (Contributed by BJ, 4-Jul-2022.) |
⊢ 𝐹:𝐴–1-1-onto→({𝑋} × 𝐴) & ⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵) ⇒ ⊢ 𝐹:𝐴–1-1→𝐵 | ||
Theorem | inlresf1 7090 | 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 7091 | 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 7092 | 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 7122 and djufun 7133) while the simpler statement ⊢ (ran inl ∩ ran inr) = ∅ is easily recovered from it by substituting V for both 𝐴 and 𝐵 as done in casefun 7114). (Contributed by BJ and Jim Kingdon, 21-Jun-2022.) |
⊢ (ran (inl ↾ 𝐴) ∩ ran (inr ↾ 𝐵)) = ∅ | ||
Theorem | djuin 7093 | 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 7094 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((inl‘𝐴) = (inl‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | djuunr 7095 | 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 7096 | 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 7097* | Element of a disjoint union. (Contributed by BJ and Jim Kingdon, 23-Jun-2022.) |
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑥 ∈ 𝐴 𝐶 = ((inl ↾ 𝐴)‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = ((inr ↾ 𝐵)‘𝑥))) | ||
Theorem | djur 7098* | 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 7099 | A disjoint union is a subset of a Cartesian product. (Contributed by AV, 25-Jun-2022.) |
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1o} × (𝐴 ∪ 𝐵)) | ||
Theorem | eldju1st 7100 | The first component of an element of a disjoint union is either ∅ or 1o. (Contributed by AV, 26-Jun-2022.) |
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) → ((1st ‘𝑋) = ∅ ∨ (1st ‘𝑋) = 1o)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |