![]() |
Intuitionistic Logic Explorer Theorem List (p. 69 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 | tridc 6801* | A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.) |
⊢ (𝜑 → 𝑅 Po 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) ⇒ ⊢ (𝜑 → DECID 𝐵𝑅𝐶) | ||
Theorem | fimax2gtrilemstep 6802* | Lemma for fimax2gtri 6803. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.) |
⊢ (𝜑 → 𝑅 Po 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ (𝜑 → 𝑈 ⊆ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑉 ∈ 𝐴) & ⊢ (𝜑 → ¬ 𝑉 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑦 ∈ 𝑈 ¬ 𝑍𝑅𝑦) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝑈 ∪ {𝑉}) ¬ 𝑥𝑅𝑦) | ||
Theorem | fimax2gtri 6803* | A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.) |
⊢ (𝜑 → 𝑅 Po 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥𝑅𝑦) | ||
Theorem | finexdc 6804* | Decidability of existence, over a finite set and defined by a decidable proposition. (Contributed by Jim Kingdon, 12-Jul-2022.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → DECID ∃𝑥 ∈ 𝐴 𝜑) | ||
Theorem | dfrex2fin 6805* | Relationship between universal and existential quantifiers over a finite set. Remark in Section 2.2.1 of [Pierik], p. 8. Although Pierik does not mention the decidability condition explicitly, it does say "only finitely many x to check" which means there must be some way of checking each value of x. (Contributed by Jim Kingdon, 11-Jul-2022.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝜑) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)) | ||
Theorem | infm 6806* | An infinite set is inhabited. (Contributed by Jim Kingdon, 18-Feb-2022.) |
⊢ (ω ≼ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴) | ||
Theorem | infn0 6807 | An infinite set is not empty. (Contributed by NM, 23-Oct-2004.) |
⊢ (ω ≼ 𝐴 → 𝐴 ≠ ∅) | ||
Theorem | inffiexmid 6808* | If any given set is either finite or infinite, excluded middle follows. (Contributed by Jim Kingdon, 15-Jun-2022.) |
⊢ (𝑥 ∈ Fin ∨ ω ≼ 𝑥) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | en2eqpr 6809 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵})) | ||
Theorem | exmidpw 6810 | Excluded middle is equivalent to the power set of 1o having two elements. Remark of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 30-Jun-2022.) |
⊢ (EXMID ↔ 𝒫 1o ≈ 2o) | ||
Theorem | fientri3 6811 | Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) | ||
Theorem | nnwetri 6812* | A natural number is well-ordered by E. More specifically, this order both satisfies We and is trichotomous. (Contributed by Jim Kingdon, 25-Sep-2021.) |
⊢ (𝐴 ∈ ω → ( E We 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))) | ||
Theorem | onunsnss 6813 | Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ⊆ 𝐴) | ||
Theorem | unfiexmid 6814* | If the union of any two finite sets is finite, excluded middle follows. Remark 8.1.17 of [AczelRathjen], p. 74. (Contributed by Mario Carneiro and Jim Kingdon, 5-Mar-2022.) |
⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑥 ∪ 𝑦) ∈ Fin) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) | ||
Theorem | unsnfi 6815 | Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∪ {𝐵}) ∈ Fin) | ||
Theorem | unsnfidcex 6816 | The 𝐵 ∈ 𝑉 condition in unsnfi 6815. This is intended to show that unsnfi 6815 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵 ∈ V) | ||
Theorem | unsnfidcel 6817 | The ¬ 𝐵 ∈ 𝐴 condition in unsnfi 6815. This is intended to show that unsnfi 6815 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵 ∈ 𝐴) | ||
Theorem | unfidisj 6818 | The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ Fin) | ||
Theorem | undifdcss 6819* | Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.) |
⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵)) | ||
Theorem | undifdc 6820* | Union of complementary parts into whole. This is a case where we can strengthen undifss 3448 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))) | ||
Theorem | undiffi 6821 | Union of complementary parts into whole. This is a case where we can strengthen undifss 3448 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))) | ||
Theorem | unfiin 6822 | The union of two finite sets is finite if their intersection is. (Contributed by Jim Kingdon, 2-Mar-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin) | ||
Theorem | prfidisj 6823 | A pair is finite if it consists of two unequal sets. For the case where 𝐴 = 𝐵, see snfig 6716. For the cases where one or both is a proper class, see prprc1 3639, prprc2 3640, or prprc 3641. (Contributed by Jim Kingdon, 31-May-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ Fin) | ||
Theorem | tpfidisj 6824 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ Fin) | ||
Theorem | fiintim 6825* |
If a class is closed under pairwise intersections, then it is closed
under nonempty finite intersections. The converse would appear to
require an additional condition, such as 𝑥 and 𝑦 not
being
equal, or 𝐴 having decidable equality.
This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∩ 𝑦) ∈ 𝐴 → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐴)) | ||
Theorem | xpfi 6826 | The Cartesian product of two finite sets is finite. Lemma 8.1.16 of [AczelRathjen], p. 74. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 × 𝐵) ∈ Fin) | ||
Theorem | 3xpfi 6827 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) | ||
Theorem | fisseneq 6828 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
Theorem | phpeqd 6829 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6767 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ssfirab 6830* | A subset of a finite set is finite if it is defined by a decidable property. (Contributed by Jim Kingdon, 27-May-2022.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 DECID 𝜓) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ Fin) | ||
Theorem | ssfidc 6831* | A subset of a finite set is finite if membership in the subset is decidable. (Contributed by Jim Kingdon, 27-May-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin) | ||
Theorem | snon0 6832 | An ordinal which is a singleton is {∅}. (Contributed by Jim Kingdon, 19-Oct-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐴} ∈ On) → 𝐴 = ∅) | ||
Theorem | fnfi 6833 | A version of fnex 5650 for finite sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin) | ||
Theorem | fundmfi 6834 | The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ Fun 𝐴) → dom 𝐴 ∈ Fin) | ||
Theorem | fundmfibi 6835 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin)) | ||
Theorem | resfnfinfinss 6836 | The restriction of a function to a finite subset of its domain is finite. (Contributed by Alexander van der Vekens, 3-Feb-2018.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵) ∈ Fin) | ||
Theorem | relcnvfi 6837 | If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.) |
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ◡𝐴 ∈ Fin) | ||
Theorem | funrnfi 6838 | The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.) |
⊢ ((Rel 𝐴 ∧ Fun ◡𝐴 ∧ 𝐴 ∈ Fin) → ran 𝐴 ∈ Fin) | ||
Theorem | f1ofi 6839 | If a 1-1 and onto function has a finite domain, its range is finite. (Contributed by Jim Kingdon, 21-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐵 ∈ Fin) | ||
Theorem | f1dmvrnfibi 6840 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 6841. (Contributed by AV, 10-Jan-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
Theorem | f1vrnfibi 6841 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 6840. (Contributed by AV, 10-Jan-2020.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
Theorem | iunfidisj 6842* | The finite union of disjoint finite sets is finite. Note that 𝐵 depends on 𝑥, i.e. can be thought of as 𝐵(𝑥). (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin ∧ Disj 𝑥 ∈ 𝐴 𝐵) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ Fin) | ||
Theorem | f1finf1o 6843 | Any injection from one finite set to another of equal size must be a bijection. (Contributed by Jeff Madsen, 5-Jun-2010.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐹:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | ||
Theorem | en1eqsn 6844 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnbi 6845 | A set containing an element has exactly one element iff it is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ (𝐴 ∈ 𝐵 → (𝐵 ≈ 1o ↔ 𝐵 = {𝐴})) | ||
Theorem | snexxph 6846* | A case where the antecedent of snexg 4116 is not needed. The class {𝑥 ∣ 𝜑} is from dcextest 4503. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.) |
⊢ {{𝑥 ∣ 𝜑}} ∈ V | ||
Theorem | preimaf1ofi 6847 | The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.) |
⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐶 ∈ Fin) ⇒ ⊢ (𝜑 → (◡𝐹 “ 𝐶) ∈ Fin) | ||
Theorem | fidcenumlemim 6848* | Lemma for fidcenum 6852. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
⊢ (𝐴 ∈ Fin → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴)) | ||
Theorem | fidcenumlemrks 6849* | Lemma for fidcenum 6852. Induction step for fidcenumlemrk 6850. (Contributed by Jim Kingdon, 20-Oct-2022.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝐽 ∈ ω) & ⊢ (𝜑 → suc 𝐽 ⊆ 𝑁) & ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐽))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽))) | ||
Theorem | fidcenumlemrk 6850* | Lemma for fidcenum 6852. (Contributed by Jim Kingdon, 20-Oct-2022.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝐾 ∈ ω) & ⊢ (𝜑 → 𝐾 ⊆ 𝑁) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐾) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐾))) | ||
Theorem | fidcenumlemr 6851* | Lemma for fidcenum 6852. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝑁 ∈ ω) ⇒ ⊢ (𝜑 → 𝐴 ∈ Fin) | ||
Theorem | fidcenum 6852* | A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as ∃𝑛 ∈ ω∃𝑓𝑓:𝑛–onto→𝐴 is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.) |
⊢ (𝐴 ∈ Fin ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴)) | ||
Theorem | sbthlem1 6853* | Lemma for isbth 6863. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) | ||
Theorem | sbthlem2 6854* | Lemma for isbth 6863. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷) | ||
Theorem | sbthlemi3 6855* | Lemma for isbth 6863. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ((EXMID ∧ ran 𝑔 ⊆ 𝐴) → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷)) | ||
Theorem | sbthlemi4 6856* | Lemma for isbth 6863. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) | ||
Theorem | sbthlemi5 6857* | Lemma for isbth 6863. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴)) → dom 𝐻 = 𝐴) | ||
Theorem | sbthlemi6 6858* | Lemma for isbth 6863. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ (((EXMID ∧ ran 𝑓 ⊆ 𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) | ||
Theorem | sbthlem7 6859* | Lemma for isbth 6863. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) | ||
Theorem | sbthlemi8 6860* | Lemma for isbth 6863. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ (((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) | ||
Theorem | sbthlemi9 6861* | Lemma for isbth 6863. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) | ||
Theorem | sbthlemi10 6862* | Lemma for isbth 6863. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((EXMID ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵) | ||
Theorem | isbth 6863 | Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set 𝐴 is smaller (has lower cardinality) than 𝐵 and vice-versa, then 𝐴 and 𝐵 are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 6853 through sbthlemi10 6862; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 6862. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity. The proof does require the law of the excluded middle which cannot be avoided as shown at exmidsbthr 13393. (Contributed by NM, 8-Jun-1998.) |
⊢ ((EXMID ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵) | ||
Syntax | cfi 6864 | Extend class notation with the function whose value is the class of finite intersections of the elements of a given set. |
class fi | ||
Definition | df-fi 6865* | Function whose value is the class of finite intersections of the elements of the argument. Note that the empty intersection being the universal class, hence a proper class, it cannot be an element of that class. Therefore, the function value is the class of nonempty finite intersections of elements of the argument (see elfi2 6868). (Contributed by FL, 27-Apr-2008.) |
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) | ||
Theorem | fival 6866* | The set of all the finite intersections of the elements of 𝐴. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) | ||
Theorem | elfi 6867* | Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) | ||
Theorem | elfi2 6868* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥)) | ||
Theorem | elfir 6869 | Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵)) | ||
Theorem | ssfii 6870 | 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 6871 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘∅) = ∅ | ||
Theorem | fieq0 6872 | 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 6873 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵)) | ||
Theorem | fiuni 6874 | 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 6875 | 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 6876* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) | ||
Syntax | csup 6877 | 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 6878 | 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 6879* | 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 6880 | 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 6881 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1d 6882 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1i 6883 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) | ||
Theorem | supeq2 6884 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅)) | ||
Theorem | supeq3 6885 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆)) | ||
Theorem | supeq123d 6886 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfsup 6887 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅) | ||
Theorem | supmoti 6888* | Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7868) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | supeuti 6889* | 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 6890* | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))) | ||
Theorem | eqsupti 6891* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqsuptid 6892* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | supclti 6893* | A supremum belongs to its base class (closure law). See also supubti 6894 and suplubti 6895. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supubti 6894* |
A supremum is an upper bound. See also supclti 6893 and suplubti 6895.
This proof demonstrates how to expand an iota-based definition (df-iota 5096) using riotacl2 5751. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | suplubti 6895* | A supremum is the least upper bound. See also supclti 6893 and supubti 6894. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | suplub2ti 6896* | Bidirectional form of suplubti 6895. (Contributed by Jim Kingdon, 17-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | supelti 6897* | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐶 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐶) | ||
Theorem | sup00 6898 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ sup(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | supmaxti 6899* | 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 6900* | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup({𝐵}, 𝐴, 𝑅) = 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |