Home | Intuitionistic Logic Explorer Theorem List (p. 69 of 133) | < 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 | en2eqpr 6801 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵})) | ||
Theorem | exmidpw 6802 | 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 6803 | Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) | ||
Theorem | nnwetri 6804* | 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 6805 | Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ On) → 𝐵 ⊆ 𝐴) | ||
Theorem | unfiexmid 6806* | 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 6807 | Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∪ {𝐵}) ∈ Fin) | ||
Theorem | unsnfidcex 6808 | The 𝐵 ∈ 𝑉 condition in unsnfi 6807. This is intended to show that unsnfi 6807 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 6809 | The ¬ 𝐵 ∈ 𝐴 condition in unsnfi 6807. This is intended to show that unsnfi 6807 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 6810 | The union of two disjoint finite sets is finite. (Contributed by Jim Kingdon, 25-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ∈ Fin) | ||
Theorem | undifdcss 6811* | Union of complementary parts into whole and decidability. (Contributed by Jim Kingdon, 17-Jun-2022.) |
⊢ (𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵)) ↔ (𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵)) | ||
Theorem | undifdc 6812* | Union of complementary parts into whole. This is a case where we can strengthen undifss 3443 from subset to equality. (Contributed by Jim Kingdon, 17-Jun-2022.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))) | ||
Theorem | undiffi 6813 | Union of complementary parts into whole. This is a case where we can strengthen undifss 3443 from subset to equality. (Contributed by Jim Kingdon, 2-Mar-2022.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → 𝐴 = (𝐵 ∪ (𝐴 ∖ 𝐵))) | ||
Theorem | unfiin 6814 | 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 6815 | A pair is finite if it consists of two unequal sets. For the case where 𝐴 = 𝐵, see snfig 6708. For the cases where one or both is a proper class, see prprc1 3631, prprc2 3632, or prprc 3633. (Contributed by Jim Kingdon, 31-May-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ Fin) | ||
Theorem | tpfidisj 6816 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ Fin) | ||
Theorem | fiintim 6817* |
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 6818 | 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 6819 | The Cartesian product of three finite sets is a finite set. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ (𝑉 ∈ Fin → ((𝑉 × 𝑉) × 𝑉) ∈ Fin) | ||
Theorem | fisseneq 6820 | A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≈ 𝐵) → 𝐴 = 𝐵) | ||
Theorem | phpeqd 6821 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6759 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | ssfirab 6822* | 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 6823* | 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 6824 | An ordinal which is a singleton is {∅}. (Contributed by Jim Kingdon, 19-Oct-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝐴} ∈ On) → 𝐴 = ∅) | ||
Theorem | fnfi 6825 | A version of fnex 5642 for finite sets. (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ Fin) | ||
Theorem | fundmfi 6826 | The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.) |
⊢ ((𝐴 ∈ Fin ∧ Fun 𝐴) → dom 𝐴 ∈ Fin) | ||
Theorem | fundmfibi 6827 | A function is finite if and only if its domain is finite. (Contributed by AV, 10-Jan-2020.) |
⊢ (Fun 𝐹 → (𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin)) | ||
Theorem | resfnfinfinss 6828 | 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 6829 | If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.) |
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ Fin) → ◡𝐴 ∈ Fin) | ||
Theorem | funrnfi 6830 | 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 6831 | 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 6832 | A one-to-one function whose domain is a set is finite if and only if its range is finite. See also f1vrnfibi 6833. (Contributed by AV, 10-Jan-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
Theorem | f1vrnfibi 6833 | A one-to-one function which is a set is finite if and only if its range is finite. See also f1dmvrnfibi 6832. (Contributed by AV, 10-Jan-2020.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (𝐹 ∈ Fin ↔ ran 𝐹 ∈ Fin)) | ||
Theorem | iunfidisj 6834* | 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 6835 | 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 6836 | A set with one element is a singleton. (Contributed by FL, 18-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o) → 𝐵 = {𝐴}) | ||
Theorem | en1eqsnbi 6837 | 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 6838* | A case where the antecedent of snexg 4108 is not needed. The class {𝑥 ∣ 𝜑} is from dcextest 4495. (Contributed by Mario Carneiro and Jim Kingdon, 4-Jul-2022.) |
⊢ {{𝑥 ∣ 𝜑}} ∈ V | ||
Theorem | preimaf1ofi 6839 | 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 6840* | Lemma for fidcenum 6844. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
⊢ (𝐴 ∈ Fin → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑛 ∈ ω ∃𝑓 𝑓:𝑛–onto→𝐴)) | ||
Theorem | fidcenumlemrks 6841* | Lemma for fidcenum 6844. Induction step for fidcenumlemrk 6842. (Contributed by Jim Kingdon, 20-Oct-2022.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝐽 ∈ ω) & ⊢ (𝜑 → suc 𝐽 ⊆ 𝑁) & ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐽))) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ suc 𝐽) ∨ ¬ 𝑋 ∈ (𝐹 “ suc 𝐽))) | ||
Theorem | fidcenumlemrk 6842* | Lemma for fidcenum 6844. (Contributed by Jim Kingdon, 20-Oct-2022.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝐾 ∈ ω) & ⊢ (𝜑 → 𝐾 ⊆ 𝑁) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝐹 “ 𝐾) ∨ ¬ 𝑋 ∈ (𝐹 “ 𝐾))) | ||
Theorem | fidcenumlemr 6843* | Lemma for fidcenum 6844. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) & ⊢ (𝜑 → 𝐹:𝑁–onto→𝐴) & ⊢ (𝜑 → 𝑁 ∈ ω) ⇒ ⊢ (𝜑 → 𝐴 ∈ Fin) | ||
Theorem | fidcenum 6844* | 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 6845* | Lemma for isbth 6855. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) | ||
Theorem | sbthlem2 6846* | Lemma for isbth 6855. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷) | ||
Theorem | sbthlemi3 6847* | Lemma for isbth 6855. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ((EXMID ∧ ran 𝑔 ⊆ 𝐴) → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷)) | ||
Theorem | sbthlemi4 6848* | Lemma for isbth 6855. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) | ||
Theorem | sbthlemi5 6849* | Lemma for isbth 6855. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((EXMID ∧ (dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴)) → dom 𝐻 = 𝐴) | ||
Theorem | sbthlemi6 6850* | Lemma for isbth 6855. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ (((EXMID ∧ ran 𝑓 ⊆ 𝐵) ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) | ||
Theorem | sbthlem7 6851* | Lemma for isbth 6855. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) | ||
Theorem | sbthlemi8 6852* | Lemma for isbth 6855. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ (((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) | ||
Theorem | sbthlemi9 6853* | Lemma for isbth 6855. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((EXMID ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) | ||
Theorem | sbthlemi10 6854* | Lemma for isbth 6855. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((EXMID ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵) | ||
Theorem | isbth 6855 | 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 6845 through sbthlemi10 6854; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlemi10 6854. 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 13218. (Contributed by NM, 8-Jun-1998.) |
⊢ ((EXMID ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) → 𝐴 ≈ 𝐵) | ||
Syntax | cfi 6856 | 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 6857* | 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 6860). (Contributed by FL, 27-Apr-2008.) |
⊢ fi = (𝑥 ∈ V ↦ {𝑧 ∣ ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑧 = ∩ 𝑦}) | ||
Theorem | fival 6858* | 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 6859* | Specific properties of an element of (fi‘𝐵). (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ (𝒫 𝐵 ∩ Fin)𝐴 = ∩ 𝑥)) | ||
Theorem | elfi2 6860* | The empty intersection need not be considered in the set of finite intersections. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (fi‘𝐵) ↔ ∃𝑥 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝐴 = ∩ 𝑥)) | ||
Theorem | elfir 6861 | Sufficient condition for an element of (fi‘𝐵). (Contributed by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ∈ (fi‘𝐵)) | ||
Theorem | ssfii 6862 | 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 6863 | The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (fi‘∅) = ∅ | ||
Theorem | fieq0 6864 | 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 6865 | Subset relationship for function fi. (Contributed by Jeff Hankins, 7-Oct-2009.) (Revised by Mario Carneiro, 24-Nov-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (fi‘𝐴) ⊆ (fi‘𝐵)) | ||
Theorem | fiuni 6866 | 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 6867 | 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 6868* | Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝐹 = (𝑦 ∈ ((𝒫 𝐴 ∩ Fin) ∖ {∅}) ↦ ∩ 𝑦) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐹:((𝒫 𝐴 ∩ Fin) ∖ {∅})–onto→(fi‘𝐴)) | ||
Syntax | csup 6869 | 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 6870 | 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 6871* | 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 6872 | 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 6873 | Equality theorem for supremum. (Contributed by NM, 22-May-1999.) |
⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1d 6874 | Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)) | ||
Theorem | supeq1i 6875 | Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅) | ||
Theorem | supeq2 6876 | Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝐵 = 𝐶 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐶, 𝑅)) | ||
Theorem | supeq3 6877 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → sup(𝐴, 𝐵, 𝑅) = sup(𝐴, 𝐵, 𝑆)) | ||
Theorem | supeq123d 6878 | Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ (𝜑 → 𝐴 = 𝐷) & ⊢ (𝜑 → 𝐵 = 𝐸) & ⊢ (𝜑 → 𝐶 = 𝐹) ⇒ ⊢ (𝜑 → sup(𝐴, 𝐵, 𝐶) = sup(𝐷, 𝐸, 𝐹)) | ||
Theorem | nfsup 6879 | Hypothesis builder for supremum. (Contributed by Mario Carneiro, 20-Mar-2014.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑅 ⇒ ⊢ Ⅎ𝑥sup(𝐴, 𝐵, 𝑅) | ||
Theorem | supmoti 6880* | Any class 𝐵 has at most one supremum in 𝐴 (where 𝑅 is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7844) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ∃*𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) | ||
Theorem | supeuti 6881* | 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 6882* | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = (℩𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)))) | ||
Theorem | eqsupti 6883* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝐶𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐶 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧)) → sup(𝐵, 𝐴, 𝑅) = 𝐶)) | ||
Theorem | eqsuptid 6884* | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ¬ 𝐶𝑅𝑦) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝐶)) → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = 𝐶) | ||
Theorem | supclti 6885* | A supremum belongs to its base class (closure law). See also supubti 6886 and suplubti 6887. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐴) | ||
Theorem | supubti 6886* |
A supremum is an upper bound. See also supclti 6885 and suplubti 6887.
This proof demonstrates how to expand an iota-based definition (df-iota 5088) using riotacl2 5743. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝐵 → ¬ sup(𝐵, 𝐴, 𝑅)𝑅𝐶)) | ||
Theorem | suplubti 6887* | A supremum is the least upper bound. See also supclti 6885 and supubti 6886. (Contributed by Jim Kingdon, 24-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ((𝐶 ∈ 𝐴 ∧ 𝐶𝑅sup(𝐵, 𝐴, 𝑅)) → ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | suplub2ti 6888* | Bidirectional form of suplubti 6887. (Contributed by Jim Kingdon, 17-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐶𝑅sup(𝐵, 𝐴, 𝑅) ↔ ∃𝑧 ∈ 𝐵 𝐶𝑅𝑧)) | ||
Theorem | supelti 6889* | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐶 (∀𝑦 ∈ 𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐵 𝑦𝑅𝑧))) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) ∈ 𝐶) | ||
Theorem | sup00 6890 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
⊢ sup(𝐵, ∅, 𝑅) = ∅ | ||
Theorem | supmaxti 6891* | 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 6892* | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup({𝐵}, 𝐴, 𝑅) = 𝐵) | ||
Theorem | isotilem 6893* | Lemma for isoti 6894. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 = 𝑦 ↔ (¬ 𝑥𝑆𝑦 ∧ ¬ 𝑦𝑆𝑥)) → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)))) | ||
Theorem | isoti 6894* | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢)) ↔ ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (𝑢 = 𝑣 ↔ (¬ 𝑢𝑆𝑣 ∧ ¬ 𝑣𝑆𝑢)))) | ||
Theorem | supisolem 6895* | Lemma for supisoti 6897. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝐷 ∈ 𝐴) → ((∀𝑦 ∈ 𝐶 ¬ 𝐷𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝐷 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧)) ↔ (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ (𝐹‘𝐷)𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆(𝐹‘𝐷) → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣)))) | ||
Theorem | supisoex 6896* | Lemma for supisoti 6897. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐵 (∀𝑤 ∈ (𝐹 “ 𝐶) ¬ 𝑢𝑆𝑤 ∧ ∀𝑤 ∈ 𝐵 (𝑤𝑆𝑢 → ∃𝑣 ∈ (𝐹 “ 𝐶)𝑤𝑆𝑣))) | ||
Theorem | supisoti 6897* | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → ∃𝑧 ∈ 𝐶 𝑦𝑅𝑧))) & ⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) → (𝑢 = 𝑣 ↔ (¬ 𝑢𝑅𝑣 ∧ ¬ 𝑣𝑅𝑢))) ⇒ ⊢ (𝜑 → sup((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘sup(𝐶, 𝐴, 𝑅))) | ||
Theorem | infeq1 6898 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝐵 = 𝐶 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1d 6899 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅)) | ||
Theorem | infeq1i 6900 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
⊢ 𝐵 = 𝐶 ⇒ ⊢ inf(𝐵, 𝐴, 𝑅) = inf(𝐶, 𝐴, 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |