| Metamath
Proof Explorer Theorem List (p. 371 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | bj-cpr1 37001 | Syntax for the first class tuple projection. (Contributed by BJ, 6-Apr-2019.) |
| class pr1 𝐴 | ||
| Definition | df-bj-pr1 37002 | Definition of the first projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr1eq 37003, bj-pr11val 37006, bj-pr21val 37014, bj-pr1ex 37007. (Contributed by BJ, 6-Apr-2019.) (New usage is discouraged.) |
| ⊢ pr1 𝐴 = (∅ Proj 𝐴) | ||
| Theorem | bj-pr1eq 37003 | Substitution property for pr1. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (𝐴 = 𝐵 → pr1 𝐴 = pr1 𝐵) | ||
| Theorem | bj-pr1un 37004 | The first projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ pr1 (𝐴 ∪ 𝐵) = (pr1 𝐴 ∪ pr1 𝐵) | ||
| Theorem | bj-pr1val 37005 | Value of the first projection. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ pr1 ({𝐴} × tag 𝐵) = if(𝐴 = ∅, 𝐵, ∅) | ||
| Theorem | bj-pr11val 37006 | Value of the first projection of a monuple. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ pr1 ⦅𝐴⦆ = 𝐴 | ||
| Theorem | bj-pr1ex 37007 | Sethood of the first projection. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → pr1 𝐴 ∈ V) | ||
| Theorem | bj-1uplth 37008 | The characteristic property of monuples. Note that this holds without sethood hypotheses. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (⦅𝐴⦆ = ⦅𝐵⦆ ↔ 𝐴 = 𝐵) | ||
| Theorem | bj-1uplex 37009 | A monuple is a set if and only if its coordinates are sets. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ (⦅𝐴⦆ ∈ V ↔ 𝐴 ∈ V) | ||
| Theorem | bj-1upln0 37010 | A monuple is nonempty. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ ⦅𝐴⦆ ≠ ∅ | ||
| Syntax | bj-c2uple 37011 | Syntax for Morse couple. (Contributed by BJ, 6-Oct-2018.) |
| class ⦅𝐴, 𝐵⦆ | ||
| Definition | df-bj-2upl 37012 | Definition of the Morse couple. See df-bj-1upl 36999. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-2upleq 37013, bj-2uplth 37022, bj-2uplex 37023, and the properties of the projections (see df-bj-pr1 37002 and df-bj-pr2 37016). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
| ⊢ ⦅𝐴, 𝐵⦆ = (⦅𝐴⦆ ∪ ({1o} × tag 𝐵)) | ||
| Theorem | bj-2upleq 37013 | Substitution property for ⦅ − , − ⦆. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐷 → ⦅𝐴, 𝐶⦆ = ⦅𝐵, 𝐷⦆)) | ||
| Theorem | bj-pr21val 37014 | Value of the first projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ pr1 ⦅𝐴, 𝐵⦆ = 𝐴 | ||
| Syntax | bj-cpr2 37015 | Syntax for the second class tuple projection. (Contributed by BJ, 6-Oct-2018.) |
| class pr2 𝐴 | ||
| Definition | df-bj-pr2 37016 | Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq 37017, bj-pr22val 37020, bj-pr2ex 37021. (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) |
| ⊢ pr2 𝐴 = (1o Proj 𝐴) | ||
| Theorem | bj-pr2eq 37017 | Substitution property for pr2. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵) | ||
| Theorem | bj-pr2un 37018 | The second projection preserves unions. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ pr2 (𝐴 ∪ 𝐵) = (pr2 𝐴 ∪ pr2 𝐵) | ||
| Theorem | bj-pr2val 37019 | Value of the second projection. (Contributed by BJ, 6-Apr-2019.) |
| ⊢ pr2 ({𝐴} × tag 𝐵) = if(𝐴 = 1o, 𝐵, ∅) | ||
| Theorem | bj-pr22val 37020 | Value of the second projection of a couple. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ pr2 ⦅𝐴, 𝐵⦆ = 𝐵 | ||
| Theorem | bj-pr2ex 37021 | Sethood of the second projection. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → pr2 𝐴 ∈ V) | ||
| Theorem | bj-2uplth 37022 | The characteristic property of couples. Note that this holds without sethood hypotheses (compare opth 5481). (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (⦅𝐴, 𝐵⦆ = ⦅𝐶, 𝐷⦆ ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | bj-2uplex 37023 | A couple is a set if and only if its coordinates are sets. For the advantages offered by the reverse closure property, see the section head comment. (Contributed by BJ, 6-Oct-2018.) |
| ⊢ (⦅𝐴, 𝐵⦆ ∈ V ↔ (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
| Theorem | bj-2upln0 37024 | A couple is nonempty. (Contributed by BJ, 21-Apr-2019.) |
| ⊢ ⦅𝐴, 𝐵⦆ ≠ ∅ | ||
| Theorem | bj-2upln1upl 37025 | A couple is never equal to a monuple. It is in order to have this "non-clashing" result that tagging was used. Without tagging, we would have ⦅𝐴, ∅⦆ = ⦅𝐴⦆. Note that in the context of Morse tuples, it is natural to define the 0-tuple as the empty set. Therefore, the present theorem together with bj-1upln0 37010 and bj-2upln0 37024 tell us that an m-tuple may equal an n-tuple only when m = n, at least for m, n <= 2, but this result would extend as soon as we define n-tuples for higher values of n. (Contributed by BJ, 21-Apr-2019.) |
| ⊢ ⦅𝐴, 𝐵⦆ ≠ ⦅𝐶⦆ | ||
Some elementary set-theoretic operations "relative to a universe" (by which is merely meant some given class considered as a universe). | ||
| Theorem | bj-rcleqf 37026 | Relative version of cleqf 2934. (Contributed by BJ, 27-Dec-2023.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 & ⊢ Ⅎ𝑥𝑉 ⇒ ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
| Theorem | bj-rcleq 37027* | Relative version of dfcleq 2730. (Contributed by BJ, 27-Dec-2023.) |
| ⊢ ((𝑉 ∩ 𝐴) = (𝑉 ∩ 𝐵) ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
| Theorem | bj-reabeq 37028* | Relative form of eqabb 2881. (Contributed by BJ, 27-Dec-2023.) |
| ⊢ ((𝑉 ∩ 𝐴) = {𝑥 ∈ 𝑉 ∣ 𝜑} ↔ ∀𝑥 ∈ 𝑉 (𝑥 ∈ 𝐴 ↔ 𝜑)) | ||
| Theorem | bj-disj2r 37029 | Relative version of ssdifin0 4486, allowing a biconditional, and of disj2 4458. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssdifin0 4486 nor disj2 4458. (Proof modification is discouraged.) |
| ⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∩ 𝑉) = ∅) | ||
| Theorem | bj-sscon 37030 | Contraposition law for relative subclasses. Relative and generalized version of ssconb 4142, which it can shorten, as well as conss2 44462. (Contributed by BJ, 11-Nov-2021.) This proof does not rely, even indirectly, on ssconb 4142 nor conss2 44462. (Proof modification is discouraged.) |
| ⊢ ((𝐴 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐵) ↔ (𝐵 ∩ 𝑉) ⊆ (𝑉 ∖ 𝐴)) | ||
In this section, we introduce the axiom of singleton ax-bj-sn 37034 and the axiom of binary union ax-bj-bun 37038. Both axioms are implied by the standard axioms of unordered pair ax-pr 5432 and of union ax-un 7755 (see snex 5436 and unex 7764). Conversely, the axiom of unordered pair ax-pr 5432 is implied by the axioms of singleton and of binary union, as proved in bj-prexg 37040 and bj-prex 37041. The axioms of union ax-un 7755 and of powerset ax-pow 5365 are independent of these axioms: consider respectively the class of pseudo-hereditarily sets of cardinality less than a given singular strong limit cardinal, see Greg Oman, On the axiom of union, Arch. Math. Logic (2010) 49:283--289 (that model does have finite unions), and the class of well-founded hereditarily countable sets (or hereditarily less than a given uncountable regular cardinal). See also https://mathoverflow.net/questions/81815 5365 and https://mathoverflow.net/questions/48365 5365. A proof by finite induction shows that the existence of finite unions is equivalent to the existence of binary unions and of nullary unions (the latter being the axiom of the empty set ax-nul 5306). The axiom of binary union is useful in theories without the axioms of union ax-un 7755 and of powerset ax-pow 5365. For instance, the class of well-founded sets hereditarily of cardinality at most 𝑛 ∈ ℕ0 with ordinary membership relation is a model of { ax-ext 2708, ax-rep 5279, ax-sep 5296, ax-nul 5306, ax-reg 9632 } and the axioms of existence of unordered 𝑚-tuples for all 𝑚 ≤ 𝑛, and in most cases one would like to rule out such models, hence the need for extra axioms, typically variants of powersets or unions. The axiom of adjunction ax-bj-adj 37043 is more widely used, and is an axiom of General Set Theory. We prove how to retrieve it from binary union and singleton in bj-adjfrombun 37047 and conversely how to prove from adjunction singleton (bj-snfromadj 37045) and unordered pair (bj-prfromadj 37046). | ||
| Theorem | bj-abex 37031* | Two ways of stating that the extension of a formula is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ ({𝑥 ∣ 𝜑} ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)) | ||
| Theorem | bj-clex 37032* | Two ways of stating that a class is a set. (Contributed by BJ, 18-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑) ⇒ ⊢ (𝐴 ∈ V ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑)) | ||
| Theorem | bj-axsn 37033* | Two ways of stating the axiom of singleton (which is the universal closure of either side, see ax-bj-sn 37034). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ ({𝑥} ∈ V ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥)) | ||
| Axiom | ax-bj-sn 37034* | Axiom of singleton. (Contributed by BJ, 12-Jan-2025.) |
| ⊢ ∀𝑥∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 = 𝑥) | ||
| Theorem | bj-snexg 37035 | A singleton built on a set is a set. Contrary to bj-snex 37036, this proof is intuitionistically valid and does not require ax-nul 5306. (Contributed by NM, 7-Aug-1994.) Extract it from snex 5436 and prove it from ax-bj-sn 37034. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) | ||
| Theorem | bj-snex 37036 | A singleton is a set. See also snex 5436, snexALT 5383. (Contributed by NM, 7-Aug-1994.) Prove it from ax-bj-sn 37034. (Revised by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ {𝐴} ∈ V | ||
| Theorem | bj-axbun 37037* | Two ways of stating the axiom of binary union (which is the universal closure of either side, see ax-bj-bun 37038). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ ((𝑥 ∪ 𝑦) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦))) | ||
| Axiom | ax-bj-bun 37038* | Axiom of binary union. (Contributed by BJ, 12-Jan-2025.) |
| ⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 ∈ 𝑦)) | ||
| Theorem | bj-unexg 37039 | Existence of binary unions of sets, proved from ax-bj-bun 37038. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) | ||
| Theorem | bj-prexg 37040 | Existence of unordered pairs formed on sets, proved from ax-bj-sn 37034 and ax-bj-bun 37038. Contrary to bj-prex 37041, this proof is intuitionistically valid and does not require ax-nul 5306. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) | ||
| Theorem | bj-prex 37041 | Existence of unordered pairs proved from ax-bj-sn 37034 and ax-bj-bun 37038. (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ {𝐴, 𝐵} ∈ V | ||
| Theorem | bj-axadj 37042* | Two ways of stating the axiom of adjunction (which is the universal closure of either side, see ax-bj-adj 37043). (Contributed by BJ, 12-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ ((𝑥 ∪ {𝑦}) ∈ V ↔ ∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦))) | ||
| Axiom | ax-bj-adj 37043* | Axiom of adjunction. (Contributed by BJ, 19-Jan-2025.) |
| ⊢ ∀𝑥∀𝑦∃𝑧∀𝑡(𝑡 ∈ 𝑧 ↔ (𝑡 ∈ 𝑥 ∨ 𝑡 = 𝑦)) | ||
| Theorem | bj-adjg1 37044 | Existence of the result of the adjunction (generalized only in the first term since this suffices for current applications). (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ {𝑥}) ∈ V) | ||
| Theorem | bj-snfromadj 37045 | Singleton from adjunction and empty set. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ {𝑥} ∈ V | ||
| Theorem | bj-prfromadj 37046 | Unordered pair from adjunction. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ {𝑥, 𝑦} ∈ V | ||
| Theorem | bj-adjfrombun 37047 | Adjunction from singleton and binary union. (Contributed by BJ, 19-Jan-2025.) (Proof modification is discouraged.) |
| ⊢ (𝑥 ∪ {𝑦}) ∈ V | ||
Miscellaneous theorems of set theory. | ||
| Theorem | eleq2w2ALT 37048 | Alternate proof of eleq2w2 2733 and special instance of eleq2 2830. (Contributed by BJ, 22-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | ||
| Theorem | bj-clel3gALT 37049* | Alternate proof of clel3g 3661. (Contributed by BJ, 1-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))) | ||
| Theorem | bj-pw0ALT 37050 | Alternate proof of pw0 4812. The proofs have a similar structure: pw0 4812 uses the definitions of powerclass and singleton as class abstractions, whereas bj-pw0ALT 37050 uses characterizations of their elements. Both proofs then use transitivity of a congruence relation (equality for pw0 4812 and biconditional for bj-pw0ALT 37050) to translate the property ss0b 4401 into the wanted result. To translate a biconditional into a class equality, pw0 4812 uses abbii 2809 (which yields an equality of class abstractions), while bj-pw0ALT 37050 uses eqriv 2734 (which requires a biconditional of membership of a given setvar variable). Note that abbii 2809, through its closed form abbi 2807, is proved from eqrdv 2735, which is the deduction form of eqriv 2734. In the other direction, velpw 4605 and velsn 4642 are proved from the definitions of powerclass and singleton using elabg 3676, which is a version of abbii 2809 suited for membership characterizations. (Contributed by BJ, 14-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝒫 ∅ = {∅} | ||
| Theorem | bj-sselpwuni 37051 | Quantitative version of ssexg 5323: a subset of an element of a class is an element of the powerclass of the union of that class. (Contributed by BJ, 6-Apr-2024.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉) → 𝐴 ∈ 𝒫 ∪ 𝑉) | ||
| Theorem | bj-unirel 37052 | Quantitative version of uniexr 7783: if the union of a class is an element of a class, then that class is an element of the double powerclass of the union of this class. (Contributed by BJ, 6-Apr-2024.) |
| ⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝒫 ∪ 𝑉) | ||
| Theorem | bj-elpwg 37053 | If the intersection of two classes is a set, then inclusion among these classes is equivalent to membership in the powerclass. Common generalization of elpwg 4603 and elpw2g 5333 (the latter of which could be proved from it). (Contributed by BJ, 31-Dec-2023.) |
| ⊢ ((𝐴 ∩ 𝐵) ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
| Theorem | bj-velpwALT 37054* | This theorem bj-velpwALT 37054 and the next theorem bj-elpwgALT 37055 are alternate proofs of velpw 4605 and elpwg 4603 respectively, where one proves first the setvar case and then generalizes using vtoclbg 3557 instead of proving first the general case using elab2g 3680 and then specifying. Here, this results in needing an extra DV condition, a longer combined proof and use of ax-12 2177. In other cases, that order is better (e.g., vsnex 5434 proved before snexg 5435). (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | ||
| Theorem | bj-elpwgALT 37055 | Alternate proof of elpwg 4603. See comment for bj-velpwALT 37054. (Contributed by BJ, 17-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | ||
| Theorem | bj-vjust 37056 | Justification theorem for dfv2 3483 if it were the definition. See also vjust 3481. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
| ⊢ {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} | ||
| Theorem | bj-nul 37057* | Two formulations of the axiom of the empty set ax-nul 5306. Proposal: place it right before ax-nul 5306. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
| ⊢ (∅ ∈ V ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
| Theorem | bj-nuliota 37058* | Definition of the empty set using the definite description binder. See also bj-nuliotaALT 37059. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
| ⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
| Theorem | bj-nuliotaALT 37059* | Alternate proof of bj-nuliota 37058. Note that this alternate proof uses the fact that ℩𝑥𝜑 evaluates to ∅ when there is no 𝑥 satisfying 𝜑 (iotanul 6539). This is an implementation detail of the encoding currently used in set.mm and should be avoided. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ∅ = (℩𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) | ||
| Theorem | bj-vtoclgfALT 37060 | Alternate proof of vtoclgf 3569. Proof from vtoclgft 3552. (This may have been the original proof before shortening.) (Contributed by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝜓) | ||
| Theorem | bj-elsn12g 37061 | Join of elsng 4640 and elsn2g 4664. (Contributed by BJ, 18-Nov-2023.) |
| ⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | ||
| Theorem | bj-elsnb 37062 | Biconditional version of elsng 4640. (Contributed by BJ, 18-Nov-2023.) |
| ⊢ (𝐴 ∈ {𝐵} ↔ (𝐴 ∈ V ∧ 𝐴 = 𝐵)) | ||
| Theorem | bj-pwcfsdom 37063 | Remove hypothesis from pwcfsdom 10623. Illustration of how to remove a "proof-facilitating hypothesis". (Can use it to shorten theorems using pwcfsdom 10623.) (Contributed by BJ, 14-Sep-2019.) |
| ⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) | ||
| Theorem | bj-grur1 37064 | Remove hypothesis from grur1 10860. Illustration of how to remove a "definitional hypothesis". This makes its uses longer, but the theorem feels more self-contained. It looks preferable when the defined term appears only once in the conclusion. (Contributed by BJ, 14-Sep-2019.) |
| ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘(𝑈 ∩ On))) | ||
| Theorem | bj-bm1.3ii 37065* |
The extension of a predicate (𝜑(𝑧)) is included in a set
(𝑥) if and only if it is a set (𝑦).
Sufficiency is obvious,
and necessity is the content of the axiom of separation ax-sep 5296.
Similar to Theorem 1.3(ii) of [BellMachover] p. 463. (Contributed by
NM, 21-Jun-1993.) Generalized to a closed form biconditional with
existential quantifications using two different setvars 𝑥, 𝑦 (which
need not be disjoint). (Revised by BJ, 8-Aug-2022.)
TODO: move after sepexi 5301. Relabel ("sepbi"?). |
| ⊢ (∃𝑥∀𝑧(𝜑 → 𝑧 ∈ 𝑥) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝜑)) | ||
| Theorem | bj-dfid2ALT 37066 | Alternate version of dfid2 5580. (Contributed by BJ, 9-Nov-2024.) (Proof modification is discouraged.) Use df-id 5578 instead to make the semantics of the construction df-opab 5206 clearer. (New usage is discouraged.) |
| ⊢ I = {〈𝑥, 𝑥〉 ∣ ⊤} | ||
| Theorem | bj-0nelopab 37067 |
The empty set is never an element in an ordered-pair class abstraction.
(Contributed by Alexander van der Vekens, 5-Nov-2017.) (Proof shortened
by BJ, 22-Jul-2023.)
TODO: move to the main section when one can reorder sections so that we can use relopab 5834 (this is a very limited reordering). |
| ⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
| Theorem | bj-brrelex12ALT 37068 | Two classes related by a binary relation are both sets. Alternate proof of brrelex12 5737. (Contributed by BJ, 14-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
| Theorem | bj-epelg 37069 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5587 and closed form of epeli 5586. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) TODO: move it to the main section after reordering to have brrelex1i 5741 available. (Proof shortened by BJ, 14-Jul-2023.) (Proof modification is discouraged.) |
| ⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
| Theorem | bj-epelb 37070 | Two classes are related by the membership relation if and only if they are related by the membership relation (i.e., the first is an element of the second) and the second is a set (hence so is the first). TODO: move to Main after reordering to have brrelex2i 5742 available. Check if it is shorter to prove bj-epelg 37069 first or bj-epelb 37070 first. (Contributed by BJ, 14-Jul-2023.) |
| ⊢ (𝐴 E 𝐵 ↔ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V)) | ||
| Theorem | bj-nsnid 37071 | A set does not contain the singleton formed on it. More precisely, one can prove that a class contains the singleton formed on it if and only if it is proper and contains the empty set (since it is "the singleton formed on" any proper class, see snprc 4717): ⊢ ¬ ({𝐴} ∈ 𝐴 ↔ (∅ ∈ 𝐴 → 𝐴 ∈ V)). (Contributed by BJ, 4-Feb-2023.) |
| ⊢ (𝐴 ∈ 𝑉 → ¬ {𝐴} ∈ 𝐴) | ||
| Theorem | bj-rdg0gALT 37072 | Alternate proof of rdg0g 8467. More direct since it bypasses tz7.44-1 8446 and rdg0 8461 (and vtoclg 3554, vtoclga 3577). (Contributed by NM, 25-Apr-1995.) More direct proof. (Revised by BJ, 17-Nov-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 𝑉 → (rec(𝐹, 𝐴)‘∅) = 𝐴) | ||
This section treats the existing predicate Slot (df-slot 17219) as "evaluation at a class" and for the moment does not introduce new syntax for it. | ||
| Theorem | bj-evaleq 37073 | Equality theorem for the Slot construction. This is currently a duplicate of sloteq 17220 but may diverge from it if/when a token Eval is introduced for evaluation in order to separate it from Slot and any of its possible modifications. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
| ⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵) | ||
| Theorem | bj-evalfun 37074 | The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021.) |
| ⊢ Fun Slot 𝐴 | ||
| Theorem | bj-evalfn 37075 | The evaluation at a class is a function on the universal class. (General form of slotfn 17221). (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by BJ, 27-Dec-2021.) |
| ⊢ Slot 𝐴 Fn V | ||
| Theorem | bj-evalval 37076 | Value of the evaluation at a class. (Closed form of strfvnd 17222 and strfvn 17223). (Contributed by NM, 9-Sep-2011.) (Revised by Mario Carneiro, 15-Nov-2014.) (Revised by BJ, 27-Dec-2021.) |
| ⊢ (𝐹 ∈ 𝑉 → (Slot 𝐴‘𝐹) = (𝐹‘𝐴)) | ||
| Theorem | bj-evalid 37077 | The evaluation at a set of the identity function is that set. (General form of ndxarg 17233.) The restriction to a set 𝑉 is necessary since the argument of the function Slot 𝐴 (like that of any function) has to be a set for the evaluation to be meaningful. (Contributed by BJ, 27-Dec-2021.) |
| ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → (Slot 𝐴‘( I ↾ 𝑉)) = 𝐴) | ||
| Theorem | bj-ndxarg 37078 | Proof of ndxarg 17233 from bj-evalid 37077. (Contributed by BJ, 27-Dec-2021.) (Proof modification is discouraged.) |
| ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
| Theorem | bj-evalidval 37079 | Closed general form of strndxid 17235. Both sides are equal to (𝐹‘𝐴) by bj-evalid 37077 and bj-evalval 37076 respectively, but bj-evalidval 37079 adds something to bj-evalid 37077 and bj-evalval 37076 in that Slot 𝐴 appears on both sides. (Contributed by BJ, 27-Dec-2021.) |
| ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑈) → (𝐹‘(Slot 𝐴‘( I ↾ 𝑉))) = (Slot 𝐴‘𝐹)) | ||
| Syntax | celwise 37080 | Syntax for elementwise operations. |
| class elwise | ||
| Definition | df-elwise 37081* | Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11185), so if 𝐴 and 𝐵 are sets of complex numbers, then (𝐴(elwise‘ + )𝐵) is the set of numbers of the form (𝑥 + 𝑦) with 𝑥 ∈ 𝐴 and 𝑦 ∈ 𝐵. The set of odd natural numbers is (({2}(elwise‘ · )ℕ0)(elwise‘ + ){1}), or less formally 2ℕ0 + 1. (Contributed by BJ, 22-Dec-2021.) |
| ⊢ elwise = (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢 ∈ 𝑥 ∃𝑣 ∈ 𝑦 𝑧 = (𝑢𝑜𝑣)})) | ||
Many kinds of structures are given by families of subsets of a given set: Moore collections (df-mre 17629), topologies (df-top 22900), pi-systems, rings of sets, delta-rings, lambda-systems/Dynkin systems, algebras/fields of sets, sigma-algebras/sigma-fields/tribes (df-siga 34110), sigma rings, monotone classes, matroids/independent sets, bornologies, filters. There is a natural notion of structure induced on a subset. It is often given by an elementwise intersection, namely, the family of intersections of sets in the original family with the given subset. In this subsection, we define this notion and prove its main properties. Classical conditions on families of subsets include being nonempty, containing the whole set, containing the empty set, being stable under unions, intersections, subsets, supersets, (relative) complements. Therefore, we prove related properties for the elementwise intersection. We will call (𝑋 ↾t 𝐴) the elementwise intersection on the family 𝑋 by the class 𝐴. REMARK: many theorems are already in set.mm: "MM> SEARCH *rest* / JOIN". | ||
| Theorem | bj-rest00 37082 | An elementwise intersection on the empty family is the empty set. TODO: this is 0rest 17474. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (∅ ↾t 𝐴) = ∅ | ||
| Theorem | bj-restsn 37083 | An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 37086 and bj-restsnid 37088. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ({𝑌} ↾t 𝐴) = {(𝑌 ∩ 𝐴)}) | ||
| Theorem | bj-restsnss 37084 | Special case of bj-restsn 37083. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑌) → ({𝑌} ↾t 𝐴) = {𝐴}) | ||
| Theorem | bj-restsnss2 37085 | Special case of bj-restsn 37083. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ⊆ 𝐴) → ({𝑌} ↾t 𝐴) = {𝑌}) | ||
| Theorem | bj-restsn0 37086 | An elementwise intersection on the singleton on the empty set is the singleton on the empty set. Special case of bj-restsn 37083 and bj-restsnss2 37085. TODO: this is restsn 23178. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
| Theorem | bj-restsn10 37087 | Special case of bj-restsn 37083, bj-restsnss 37084, and bj-rest10 37089. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → ({𝑋} ↾t ∅) = {∅}) | ||
| Theorem | bj-restsnid 37088 | The elementwise intersection on the singleton on a class by that class is the singleton on that class. Special case of bj-restsn 37083 and bj-restsnss 37084. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ({𝐴} ↾t 𝐴) = {𝐴} | ||
| Theorem | bj-rest10 37089 | An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 23177 and could replace it. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝑋 ≠ ∅ → (𝑋 ↾t ∅) = {∅})) | ||
| Theorem | bj-rest10b 37090 | Alternate version of bj-rest10 37089. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (𝑋 ∈ (𝑉 ∖ {∅}) → (𝑋 ↾t ∅) = {∅}) | ||
| Theorem | bj-restn0 37091 | An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ≠ ∅ → (𝑋 ↾t 𝐴) ≠ ∅)) | ||
| Theorem | bj-restn0b 37092 | Alternate version of bj-restn0 37091. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑋 ∈ (𝑉 ∖ {∅}) ∧ 𝐴 ∈ 𝑊) → (𝑋 ↾t 𝐴) ≠ ∅) | ||
| Theorem | bj-restpw 37093 | The elementwise intersection on a powerset is the powerset of the intersection. This allows to prove for instance that the topology induced on a subset by the discrete topology is the discrete topology on that subset. See also restdis 23186 (which uses distop 23002 and restopn2 23185). (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝒫 𝑌 ↾t 𝐴) = 𝒫 (𝑌 ∩ 𝐴)) | ||
| Theorem | bj-rest0 37094 | An elementwise intersection on a family containing the empty set contains the empty set. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (∅ ∈ 𝑋 → ∅ ∈ (𝑋 ↾t 𝐴))) | ||
| Theorem | bj-restb 37095 | An elementwise intersection by a set on a family containing a superset of that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
| Theorem | bj-restv 37096 | An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝐴 ⊆ ∪ 𝑋 ∧ ∪ 𝑋 ∈ 𝑋) → 𝐴 ∈ (𝑋 ↾t 𝐴)) | ||
| Theorem | bj-resta 37097 | An elementwise intersection by a set on a family containing that set contains that set. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝐴 ∈ 𝑋 → 𝐴 ∈ (𝑋 ↾t 𝐴))) | ||
| Theorem | bj-restuni 37098 | The union of an elementwise intersection by a set is equal to the intersection with that set of the union of the family. See also restuni 23170 and restuni2 23175. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → ∪ (𝑋 ↾t 𝐴) = (∪ 𝑋 ∩ 𝐴)) | ||
| Theorem | bj-restuni2 37099 | The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni 23170 and restuni2 23175. (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ ∪ 𝑋) → ∪ (𝑋 ↾t 𝐴) = 𝐴) | ||
| Theorem | bj-restreg 37100 | A reformulation of the axiom of regularity using elementwise intersection. (RK: might have to be placed later since theorems in this section are to be moved early (in the section related to the algebra of sets).) (Contributed by BJ, 27-Apr-2021.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∅ ∈ (𝐴 ↾t 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |