![]() |
Metamath
Proof Explorer Theorem List (p. 87 of 435) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28331) |
![]() (28332-29856) |
![]() (29857-43448) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | inficl 8601* | A set which is closed under pairwise intersection is closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 ↔ (fi‘𝐴) = 𝐴)) | ||
Theorem | fipwuni 8602 | The set of finite intersections of a set is contained in the powerset of the union of the elements of 𝐴. (Contributed by Mario Carneiro, 24-Nov-2013.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ (fi‘𝐴) ⊆ 𝒫 ∪ 𝐴 | ||
Theorem | fisn 8603 | A singleton is closed under finite intersections. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (fi‘{𝐴}) = {𝐴} | ||
Theorem | fiuni 8604 | 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 | fipwss 8605 | 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 | elfiun 8606* | A finite intersection of elements taken from a union of collections. (Contributed by Jeff Hankins, 15-Nov-2009.) (Proof shortened by Mario Carneiro, 26-Nov-2013.) |
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐾) → (𝐴 ∈ (fi‘(𝐵 ∪ 𝐶)) ↔ (𝐴 ∈ (fi‘𝐵) ∨ 𝐴 ∈ (fi‘𝐶) ∨ ∃𝑥 ∈ (fi‘𝐵)∃𝑦 ∈ (fi‘𝐶)𝐴 = (𝑥 ∩ 𝑦)))) | ||
Theorem | dffi3 8607* | The set of finite intersections can be "constructed" inductively by iterating binary intersection ω-many times. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑅 = (𝑢 ∈ V ↦ ran (𝑦 ∈ 𝑢, 𝑧 ∈ 𝑢 ↦ (𝑦 ∩ 𝑧))) ⇒ ⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∪ (rec(𝑅, 𝐴) “ ω)) | ||
Theorem | fifo 8608* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) | ||
Theorem | marypha1lem 8609* | Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))) | ||
Theorem | marypha1 8610* | (Philip) Hall's marriage theorem, sufficiency: a finite relation contains an injection if there is no subset of its domain which would be forced to violate the pigeonhole principle. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ⊆ (𝐴 × 𝐵)) & ⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ (𝐶 “ 𝑑)) ⇒ ⊢ (𝜑 → ∃𝑓 ∈ 𝒫 𝐶𝑓:𝐴–1-1→𝐵) | ||
Theorem | marypha2lem1 8611* | Lemma for marypha2 8615. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 ⊆ (𝐴 × ∪ ran 𝐹) | ||
Theorem | marypha2lem2 8612* | Lemma for marypha2 8615. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} | ||
Theorem | marypha2lem3 8613* | Lemma for marypha2 8615. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐺 ⊆ 𝑇 ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹‘𝑥))) | ||
Theorem | marypha2lem4 8614* | Lemma for marypha2 8615. Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ⊆ 𝐴) → (𝑇 “ 𝑋) = ∪ (𝐹 “ 𝑋)) | ||
Theorem | marypha2 8615* | Version of marypha1 8610 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶Fin) & ⊢ ((𝜑 ∧ 𝑑 ⊆ 𝐴) → 𝑑 ≼ ∪ (𝐹 “ 𝑑)) ⇒ ⊢ (𝜑 → ∃𝑔(𝑔:𝐴–1-1→V ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))) | ||
Syntax | csup 8616 | 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 8617 | 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 8618* | Define the supremum of class 𝐴. It is meaningful when 𝑅 is a relation that strictly orders 𝐵 and when the supremum exists. For example, 𝑅 could be 'less than', 𝐵 could be the set of real numbers, and 𝐴 could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrtval 14355. See dfsup2 8620 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999.) |
⊢ sup(𝐴, 𝐵, 𝑅) = ∪ {𝑥 ∈ 𝐵 ∣ (∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦𝑅𝑧))} | ||
Definition | df-inf 8619 | 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 | dfsup2 8620 | Quantifier free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013.) |
⊢ sup(𝐵, 𝐴, 𝑅) = ∪ (𝐴 ∖ ((◡𝑅 “ 𝐵) ∪ (𝑅 “ (𝐴 ∖ (◡𝑅 “ 𝐵))))) | ||
Theorem | supeq1 8621 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1d 8622 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1i 8623 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) | ||
Theorem | supeq2 8624 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅)) | ||
Theorem | supeq3 8625 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆)) | ||
Theorem | supeq123d 8626 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfsup 8627 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅) | ||
Theorem | supmo 8628* | Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by NM, 5-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | supexd 8629 | A supremum is a set. (Contributed by NM, 22-May-1999.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | supeu 8630* | A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by NM, 12-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | supval2 8631* | Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Thierry Arnoux, 24-Sep-2017.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))) | ||
Theorem | eqsup 8632* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqsupd 8633* | Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | supcl 8634* | A supremum belongs to its base class (closure law). See also supub 8635 and suplub 8636. (Contributed by NM, 12-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supub 8635* |
A supremum is an upper bound. See also supcl 8634 and suplub 8636.
This proof demonstrates how to expand an iota-based definition (df-iota 6087) using riotacl2 6880. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | suplub 8636* | A supremum is the least upper bound. See also supcl 8634 and supub 8635. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | suplub2 8637* | Bidirectional form of suplub 8636. (Contributed by Mario Carneiro, 6-Sep-2014.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | supnub 8638* | An upper bound is not less than the supremum. (Contributed by NM, 13-Oct-2004.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝐶𝑅𝑧) → ¬ 𝐶𝑅sup(𝐵, 𝐴, 𝑅))) | ||
Theorem | supex 8639 | A supremum is a set. (Contributed by NM, 22-May-1999.) |
⊢ 𝑅 Or 𝐴 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) ∈ V | ||
Theorem | sup00 8640 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ sup(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | sup0riota 8641* | The supremum of an empty set is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
⊢ (𝑅 Or 𝐴 → sup(∅, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥)) | ||
Theorem | sup0 8642* | The supremum of an empty set under a base set which has a unique smallest element is the smallest element of the base set. (Contributed by AV, 4-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑋) ∧ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) → sup(∅, 𝐴, 𝑅) = 𝑋) | ||
Theorem | supmax 8643* | 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 Jeff Hoffman, 17-Jun-2008.) (Proof shortened by OpenAI, 30-Mar-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | fisup2g 8644* | A finite set satisfies the conditions to have a supremum. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | fisupcl 8645 | A nonempty finite set contains its supremum. (Contributed by Jeff Madsen, 9-May-2011.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵) | ||
Theorem | supgtoreq 8646 | The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 = sup(𝐵, 𝐴, 𝑅)) ⇒ ⊢ (𝜑 → (𝐶𝑅𝑆 ∨ 𝐶 = 𝑆)) | ||
Theorem | suppr 8647 | The supremum of a pair. (Contributed by NM, 17-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → sup({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐶𝑅𝐵, 𝐵, 𝐶)) | ||
Theorem | supsn 8648 | The supremum of a singleton. (Contributed by NM, 2-Oct-2007.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → sup({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | supisolem 8649* | Lemma for supiso 8651. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) | ||
Theorem | supisoex 8650* | Lemma for supiso 8651. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))) | ||
Theorem | supiso 8651* | Image of a supremum under an isomorphism. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅))) | ||
Theorem | infeq1 8652 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1d 8653 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1i 8654 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) | ||
Theorem | infeq2 8655 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐶, 𝑅)) | ||
Theorem | infeq3 8656 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝑅 = 𝑆 → inf(𝐴, 𝐵, 𝑅) = inf(𝐴, 𝐵, 𝑆)) | ||
Theorem | infeq123d 8657 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → inf(𝐴, 𝐵, 𝐶) = inf(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfinf 8658 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥inf(𝐴, 𝐵, 𝑅) | ||
Theorem | infexd 8659 | An infimum is a set. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ V) | ||
Theorem | eqinf 8660* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝐶 ∧ ∀𝑦 ∈ 𝐴 (𝐶𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)) → inf(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqinfd 8661* | Sufficient condition for an element to be equal to the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝐶𝑅𝑦)) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | infval 8662* | Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦)))) | ||
Theorem | infcllem 8663* | Lemma for infcl 8664, inflb 8665, infglb 8666, etc. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦◡𝑅𝑧))) | ||
Theorem | infcl 8664* | An infimum belongs to its base class (closure law). See also inflb 8665 and infglb 8666. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | inflb 8665* | An infimum is a lower bound. See also infcl 8664 and infglb 8666. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ 𝐶𝑅inf(𝐵, 𝐴, 𝑅))) | ||
Theorem | infglb 8666* | An infimum is the greatest lower bound. See also infcl 8664 and inflb 8665. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ inf(𝐵, 𝐴, 𝑅)𝑅𝐶) → ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infglbb 8667* | Bidirectional form of infglb 8666. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (inf(𝐵, 𝐴, 𝑅)𝑅𝐶 ↔ ∃𝑧 ∈ 𝐵 𝑧𝑅𝐶)) | ||
Theorem | infnlb 8668* | A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧𝑅𝐶) → ¬ inf(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | infex 8669 | An infimum is a set. (Contributed by AV, 3-Sep-2020.) |
⊢ 𝑅 Or 𝐴 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) ∈ V | ||
Theorem | infmin 8670* | 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 AV, 3-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝑦𝑅𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | infmo 8671* | Any class 𝐵 has at most one infimum in 𝐴 (where 𝑅 is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | infeu 8672* | An infimum is unique. (Contributed by AV, 6-Oct-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | fimin2g 8673* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) | ||
Theorem | fiming 8674* | A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → 𝑥𝑅𝑦)) | ||
Theorem | fiinfg 8675* | Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐴 𝑧𝑅𝑦))) | ||
Theorem | fiinf2g 8676* | A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐵 𝑧𝑅𝑦))) | ||
Theorem | fiinfcl 8677 | A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → inf(𝐵, 𝐴, 𝑅) ∈ 𝐵) | ||
Theorem | infltoreq 8678 | The infimum of a finite set is less than or equal to all the elements of the set. (Contributed by AV, 4-Sep-2020.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 = inf(𝐵, 𝐴, 𝑅)) ⇒ ⊢ (𝜑 → (𝑆𝑅𝐶 ∨ 𝐶 = 𝑆)) | ||
Theorem | infpr 8679 | The infimum of a pair. (Contributed by AV, 4-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → inf({𝐵, 𝐶}, 𝐴, 𝑅) = if(𝐵𝑅𝐶, 𝐵, 𝐶)) | ||
Theorem | infsn 8680 | The infimum of a singleton. (Contributed by NM, 2-Oct-2007.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → inf({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | inf00 8681 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ inf(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | infempty 8682* | The infimum of an empty set under a base set which has a unique greatest element is the greatest element of the base set. (Contributed by AV, 4-Sep-2020.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑋𝑅𝑦) ∧ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦) → inf(∅, 𝐴, 𝑅) = 𝑋) | ||
Theorem | infiso 8683* | Image of an infimum under an isomorphism. (Contributed by AV, 4-Sep-2020.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦))) & ⊢ (𝜑 → 𝑅 Or 𝐴) ⇒ ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅))) | ||
Syntax | coi 8684 | Extend class definition to include the canonical order isomorphism to an ordinal. |
class OrdIso(𝑅, 𝐴) | ||
Definition | df-oi 8685* | Define the canonical order isomorphism from the well-order 𝑅 on 𝐴 to an ordinal. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅) | ||
Theorem | dfoi 8686* | Rewrite df-oi 8685 with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝐹 = recs(𝐺) ⇒ ⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (𝐹 ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}), ∅) | ||
Theorem | oieq1 8687 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ (𝑅 = 𝑆 → OrdIso(𝑅, 𝐴) = OrdIso(𝑆, 𝐴)) | ||
Theorem | oieq2 8688 | Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) |
⊢ (𝐴 = 𝐵 → OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐵)) | ||
Theorem | nfoi 8689 | Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥OrdIso(𝑅, 𝐴) | ||
Theorem | ordiso2 8690 | Generalize ordiso 8691 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵) | ||
Theorem | ordiso 8691* | 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 (𝐴, 𝐵))) | ||
Theorem | ordtypecbv 8692* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) ⇒ ⊢ recs((𝑓 ∈ V ↦ (℩𝑠 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) = 𝐹 | ||
Theorem | ordtypelem1 8693* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) | ||
Theorem | ordtypelem2 8694* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → Ord 𝑇) | ||
Theorem | ordtypelem3 8695* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | ||
Theorem | ordtypelem4 8696* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) | ||
Theorem | ordtypelem5 8697* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → (Ord dom 𝑂 ∧ 𝑂:dom 𝑂⟶𝐴)) | ||
Theorem | ordtypelem6 8698* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀))) | ||
Theorem | ordtypelem7 8699* | Lemma for ordtype 8707. ran 𝑂 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂)) | ||
Theorem | ordtypelem8 8700* | Lemma for ordtype 8707. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) & ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} & ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣)) & ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡} & ⊢ 𝑂 = OrdIso(𝑅, 𝐴) & ⊢ (𝜑 → 𝑅 We 𝐴) & ⊢ (𝜑 → 𝑅 Se 𝐴) ⇒ ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |