Home | Metamath
Proof Explorer Theorem List (p. 349 of 450) | < 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: | Metamath Proof Explorer
(1-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wl-sbal1 34801* | A theorem used in elimination of disjoint variable restriction on 𝑥 and 𝑦 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 15-May-1993.) Proof is based on wl-sbalnae 34800 now. See also sbal1 2572. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-sbal2 34802* | Move quantifier in and out of substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 2-Jan-2002.) Proof is based on wl-sbalnae 34800 now. See also sbal2 2573. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-2spsbbi 34803 | spsbbi 2078 applied twice. (Contributed by Wolf Lammen, 5-Aug-2023.) |
⊢ (∀𝑎∀𝑏(𝜑 ↔ 𝜓) → ([𝑦 / 𝑏][𝑥 / 𝑎]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜓)) | ||
Theorem | wl-lem-exsb 34804* | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | wl-lem-nexmo 34805 | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧)) | ||
Theorem | wl-lem-moexsb 34806* |
The antecedent ∀𝑥(𝜑 → 𝑥 = 𝑧) relates to ∃*𝑥𝜑, but is
better suited for usage in proofs. Note that no distinct variable
restriction is placed on 𝜑.
This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → (∃𝑥𝜑 ↔ [𝑧 / 𝑥]𝜑)) | ||
Theorem | wl-alanbii 34807 | This theorem extends alanimi 1817 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | wl-mo2df 34808 | Version of mof 2647 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦) & ⊢ (𝜑 → Ⅎ𝑦𝜓) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦))) | ||
Theorem | wl-mo2tf 34809 | Closed form of mof 2647 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-eudf 34810 | Version of eu6 2659 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦) & ⊢ (𝜑 → Ⅎ𝑦𝜓) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 ↔ 𝑥 = 𝑦))) | ||
Theorem | wl-eutf 34811 | Closed form of eu6 2659 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) | ||
Theorem | wl-euequf 34812 | euequ 2683 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦) | ||
Theorem | wl-mo2t 34813* | Closed form of mof 2647. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-mo3t 34814* | Closed form of mo3 2648. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) | ||
Theorem | wl-sb8eut 34815 | Substitution of variable in universal quantifier. Closed form of sb8eu 2686. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sb8mot 34816 |
Substitution of variable in universal quantifier. Closed form of
sb8mo 2687.
This theorem relates to wl-mo3t 34814, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2270 and sbco 2549. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 34814 in a simple fashion, unfortunately only if 𝑥 and 𝑦 are known to be distinct. To avoid any hassle with distinctors, we prefer to derive this theorem independently, ignoring the close connection between both theorems. From an educational standpoint, one would assume wl-mo3t 34814 to be more fundamental, as it hints how the "at most one" objects on both sides of the biconditional correlate (they are the same), if they exist at all, and then prove this theorem from it. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-axc11rc11 34817 |
Proving axc11r 2386 from axc11 2452. The hypotheses are two instances of
axc11 2452 used in the proof here. Some systems
introduce axc11 2452 as an
axiom, see for example System S2 in
https://us.metamath.org/downloads/finiteaxiom.pdf .
By contrast, this database sees the variant axc11r 2386, directly derived from ax-12 2177, as foundational. Later axc11 2452 is proven somewhat trickily, requiring ax-10 2145 and ax-13 2390, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.) |
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)) & ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-wl-11v 34818* | Version of ax-11 2161 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2161. It will later be converted into a theorem directly based on ax-11 2161. (Contributed by Wolf Lammen, 28-Jun-2019.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | wl-ax11-lem1 34819 | A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧)) | ||
Theorem | wl-ax11-lem2 34820* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem3 34821* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem4 34822* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | wl-ax11-lem5 34823 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem6 34824* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem7 34825 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem8 34826* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem9 34827 | The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem10 34828* | We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 194 can be used in conjunction with wl-ax11-lem9 34827 to eliminate the second antecedent. Missing is something along the lines of ax-6 1970, so we could remove the first antecedent. But the Metamath axioms cannot accomplish this. Such a rule must reside one abstraction level higher than all others: It says that a distinctor implies a distinct variable condition on its contained setvar. This is only needed if such conditions are required, as ax-11v does. The result of this study is for me, that you cannot introduce a setvar capturing this condition, and hope to eliminate it later. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑦 𝑦 = 𝑢 → (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑))) | ||
Theorem | wl-clabv 34829* |
Variant of df-clab 2802, where the element 𝑥 is required to be
disjoint from the class it is taken from. This restriction meets
similar ones found in other definitions and axioms like ax-ext 2795,
df-clel 2895 and df-cleq 2816. 𝑥 ∈ 𝐴 with 𝐴 depending on 𝑥 can
be the source of side effects, that you rather want to be aware of. So
here we eliminate one possible way of letting this slip in instead.
An expression 𝑥 ∈ 𝐴 with 𝑥, 𝐴 not disjoint, is now only introduced either via ax-8 2116, ax-9 2124, or df-clel 2895. Theorem cleljust 2123 shows that a possible choice does not matter. The original df-clab 2802 can be rederived, see wl-dfclab 34830. In an implementation this theorem is the only user of df-clab. (Contributed by NM, 26-May-1993.) Element and class are disjoint. (Revised by Wolf Lammen, 31-May-2023.) |
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | ||
Theorem | wl-dfclab 34830 | Rederive df-clab 2802 from wl-clabv 34829. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | ||
Theorem | wl-clabtv 34831* | Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 34832. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Theorem | wl-clabt 34832 | Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 34831. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Syntax | wl-ral 34833 | Redefine the restricted universal quantifier context to avoid overloading and syntax check errors in mmj2. This operator is to be distinguished from ∀𝑥 ∈ 𝐴𝜑 with a similiar semantics, but using 𝑥 as a formal parameter rather than assuming true elementhood. |
wff ∀(𝑥 : 𝐴)𝜑 | ||
Syntax | wl-rex 34834 | Redefine the restricted existential quantifier context to avoid overloading and syntax check errors in mmj2. This operator is to be distinguished from ∃𝑥 ∈ 𝐴𝜑 with a similiar semantics, but using 𝑥 as a formal parameter rather than assuming true elementhood. |
wff ∃(𝑥 : 𝐴)𝜑 | ||
Syntax | wl-rmo 34835 | Redefine the restricted "at most one" quantifier context to avoid overloading and syntax check errors in mmj2. This operator is to be distinguished from ∃*𝑥 ∈ 𝐴𝜑 with a similiar semantics, but using 𝑥 as a formal parameter rather than assuming true elementhood. |
wff ∃*(𝑥 : 𝐴)𝜑 | ||
Syntax | wl-reu 34836 | Redefine the restricted existential uniqueness context to avoid overloading and syntax check errors in mmj2. This operator is to be distinguished from ∃!𝑥 ∈ 𝐴𝜑 with a similiar semantics, but using 𝑥 as a formal parameter rather than assuming true elementhood. |
wff ∃!(𝑥 : 𝐴)𝜑 | ||
Syntax | wl-crab 34837 | Redefine extended class notation to include the restricted class abstraction (class builder). |
class {𝑥 : 𝐴 ∣ 𝜑} | ||
Definition | df-wl-ral 34838* |
The definiens of df-ral 3145, ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) is a short and
simple expression, but has a severe downside: It allows for two
substantially different interpretations. One, and this is the common
case, wants this expression to denote that 𝜑 holds for all elements
of 𝐴. To this end, 𝑥 must
not be free in 𝐴, though .
Should instead 𝐴 vary with 𝑥, then we rather focus on
those
𝑥, that happen to be an element of
their respective 𝐴(𝑥).
Such interpretation is rare, but must nevertheless be considered in
design and comments.
In addition, many want definitions be designed to express just a single idea, not many. Our definition here introduces a dummy variable 𝑦, disjoint from all other variables, to describe an element in 𝐴. It lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurrences in 𝜑 are still honored. The resulting subexpression ∀𝑥(𝑥 = 𝑦 → 𝜑) is [𝑦 / 𝑥]𝜑 in disguise (see wl-dfralsb 34839). If 𝑥 is not free in 𝐴, a simplification is possible ( see wl-dfralf 34841, wl-dfralv 34843). (Contributed by NM, 19-Aug-1993.) Isolate 𝑥 from 𝐴, idea of Mario Carneiro. (Revised by Wolf Lammen, 21-May-2023.) |
⊢ (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | wl-dfralsb 34839* | An alternate definition of restricted universal quantification (df-wl-ral 34838) using substitution. (Contributed by Wolf Lammen, 25-May-2023.) |
⊢ (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-dfralflem 34840* | Lemma for wl-dfralf 34841 and wl-dfralv . (Contributed by Wolf Lammen, 23-May-2023.) |
⊢ (∀𝑦∀𝑥(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | wl-dfralf 34841 | Restricted universal quantification (df-wl-ral 34838) allows a simplification, if we can assume all appearences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 23-May-2023.) |
⊢ (Ⅎ𝑥𝐴 → (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))) | ||
Theorem | wl-dfralfi 34842 | Restricted universal quantification (df-wl-ral 34838) allows allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 26-May-2023.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | wl-dfralv 34843* | Alternate definition of restricted universal quantification (df-wl-ral ) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 23-May-2023.) |
⊢ (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | ||
Theorem | wl-rgen 34844* | Generalization rule for restricted quantification. (Contributed by Wolf Lammen, 10-Jun-2023.) |
⊢ (𝑥 ∈ 𝐴 → 𝜑) ⇒ ⊢ ∀(𝑥 : 𝐴)𝜑 | ||
Theorem | wl-rgenw 34845 | Generalization rule for restricted quantification. (Contributed by Wolf Lammen, 10-Jun-2023.) |
⊢ 𝜑 ⇒ ⊢ ∀(𝑥 : 𝐴)𝜑 | ||
Theorem | wl-rgen2w 34846 | Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by Wolf Lammen, 10-Jun-2023.) |
⊢ 𝜑 ⇒ ⊢ ∀(𝑥 : 𝐴)∀(𝑦 : 𝐵)𝜑 | ||
Theorem | wl-ralel 34847* | All elements of a class are elements of the class. (Contributed by Wolf Lammen, 10-Jun-2023.) |
⊢ ∀(𝑥 : 𝐴)𝑥 ∈ 𝐴 | ||
Definition | df-wl-rex 34848 |
Restrict an existential quantifier to a class 𝐴. This version does
not interpret elementhood verbatim as ∃𝑥 ∈ 𝐴𝜑 does. Assuming a
real elementhood can lead to awkward consequences should the class 𝐴
depend on 𝑥. Instead we base the definition on
df-wl-ral 34838, where
this is ruled out. Other definitions are wl-dfrexsb 34853 and
wl-dfrexex 34852. If 𝑥 is not free in 𝐴, the defining expression
can be simplified (see wl-dfrexf 34849, wl-dfrexv 34851).
This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurrences in 𝜑 are fully honored. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 25-May-2023.) |
⊢ (∃(𝑥 : 𝐴)𝜑 ↔ ¬ ∀(𝑥 : 𝐴) ¬ 𝜑) | ||
Theorem | wl-dfrexf 34849 | Restricted existential quantification (df-wl-rex 34848) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 25-May-2023.) |
⊢ (Ⅎ𝑥𝐴 → (∃(𝑥 : 𝐴)𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
Theorem | wl-dfrexfi 34850 | Restricted universal quantification (df-wl-rex 34848) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 26-May-2023.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (∃(𝑥 : 𝐴)𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | wl-dfrexv 34851* | Alternate definition of restricted universal quantification (df-wl-rex 34848) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 25-May-2023.) |
⊢ (∃(𝑥 : 𝐴)𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | wl-dfrexex 34852* | Alternate definition of the restricted existential quantification (df-wl-rex 34848), according to the pattern given in df-wl-ral 34838. (Contributed by Wolf Lammen, 25-May-2023.) |
⊢ (∃(𝑥 : 𝐴)𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | wl-dfrexsb 34853* | An alternate definition of restricted existential quantification (df-wl-rex 34848) using substitution. (Contributed by Wolf Lammen, 25-May-2023.) |
⊢ (∃(𝑥 : 𝐴)𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)) | ||
Definition | df-wl-rmo 34854* |
Restrict "at most one" to a given class 𝐴. This version does not
interpret elementhood verbatim like ∃*𝑥 ∈ 𝐴𝜑 does. Assuming a
real elementhood can lead to awkward consequences should the class 𝐴
depend on 𝑥. Instead we base the definition on
df-wl-ral 34838, where
this is already ruled out.
This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurrences in 𝜑 are fully honored. Alternate definitions are given in wl-dfrmosb 34855 and, if 𝑥 is not free in 𝐴, wl-dfrmov 34856 and wl-dfrmof 34857. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 26-May-2023.) |
⊢ (∃*(𝑥 : 𝐴)𝜑 ↔ ∃𝑦∀(𝑥 : 𝐴)(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | wl-dfrmosb 34855* | An alternate definition of restricted "at most one" (df-wl-rmo 34854) using substitution. (Contributed by Wolf Lammen, 27-May-2023.) |
⊢ (∃*(𝑥 : 𝐴)𝜑 ↔ ∃*𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-dfrmov 34856* | Alternate definition of restricted "at most one" (df-wl-rmo 34854) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 28-May-2023.) |
⊢ (∃*(𝑥 : 𝐴)𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | wl-dfrmof 34857 | Restricted "at most one" (df-wl-rmo 34854) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 28-May-2023.) |
⊢ (Ⅎ𝑥𝐴 → (∃*(𝑥 : 𝐴)𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
Definition | df-wl-reu 34858 |
Restrict existential uniqueness to a given class 𝐴. This version
does not interpret elementhood verbatim like ∃!𝑥 ∈
𝐴𝜑 does.
Assuming a real elementhood can lead to awkward consequences should the
class 𝐴 depend on 𝑥. Instead we base the
definition on
df-wl-ral 34838, where this is ruled out.
This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurrences in 𝜑 are fully honored. Alternate definitions are given in wl-dfreusb 34859 and, if 𝑥 is not free in 𝐴, wl-dfreuv 34860 and wl-dfreuf 34861. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 28-May-2023.) |
⊢ (∃!(𝑥 : 𝐴)𝜑 ↔ (∃(𝑥 : 𝐴)𝜑 ∧ ∃*(𝑥 : 𝐴)𝜑)) | ||
Theorem | wl-dfreusb 34859* | An alternate definition of restricted existential uniqueness (df-wl-reu 34858) using substitution. (Contributed by Wolf Lammen, 28-May-2023.) |
⊢ (∃!(𝑥 : 𝐴)𝜑 ↔ ∃!𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-dfreuv 34860* | Alternate definition of restricted existential uniqueness (df-wl-reu 34858) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 28-May-2023.) |
⊢ (∃!(𝑥 : 𝐴)𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | ||
Theorem | wl-dfreuf 34861 | Restricted existential uniqueness (df-wl-reu 34858) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 28-May-2023.) |
⊢ (Ⅎ𝑥𝐴 → (∃!(𝑥 : 𝐴)𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | ||
Definition | df-wl-rab 34862* | Define a restricted class abstraction (class builder), which is the class of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.) Isolate x from A. (Revised by Wolf Lammen, 28-May-2023.) |
⊢ {𝑥 : 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))} | ||
Theorem | wl-dfrabsb 34863* | Alternate definition of restricted class abstraction (df-wl-rab 34862), using substitution. (Contributed by Wolf Lammen, 28-May-2023.) |
⊢ {𝑥 : 𝐴 ∣ 𝜑} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)} | ||
Theorem | wl-dfrabv 34864* | Alternate definition of restricted class abstraction (df-wl-rab 34862), when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ {𝑥 : 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | ||
Theorem | wl-clelsb3df 34865 | Deduction version of clelsb3f 2984. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝐴) ⇒ ⊢ (𝜑 → ([𝑥 / 𝑦]𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) | ||
Theorem | wl-dfrabf 34866 | Alternate definition of restricted class abstraction (df-wl-rab 34862), when 𝑥 is not free in 𝐴. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ (Ⅎ𝑥𝐴 → {𝑥 : 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}) | ||
Theorem | rabiun 34867* | Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.) |
⊢ {𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑} = ∪ 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | iundif1 34868* | Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶) | ||
Theorem | imadifss 34869 | The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵)) | ||
Theorem | cureq 34870 | Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → curry 𝐴 = curry 𝐵) | ||
Theorem | unceq 34871 | Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵) | ||
Theorem | curf 34872 | Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) | ||
Theorem | uncf 34873 | Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶) | ||
Theorem | curfv 34874 | Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | uncov 34875 | Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵)) | ||
Theorem | curunc 34876 | Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹) | ||
Theorem | unccur 34877 | Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → uncurry curry 𝐹 = 𝐹) | ||
Theorem | phpreu 34878* | Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶)) | ||
Theorem | finixpnum 34879* | A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈ 𝐴 𝐵 ∈ dom card) | ||
Theorem | fin2solem 34880* | Lemma for fin2so 34881. (Contributed by Brendan Leahy, 29-Jun-2019.) |
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) → (𝑦𝑅𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})) | ||
Theorem | fin2so 34881 | Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.) |
⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin) | ||
Theorem | ltflcei 34882 | Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) < 𝐵 ↔ 𝐴 < -(⌊‘-𝐵))) | ||
Theorem | leceifl 34883 | Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-(⌊‘-𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (⌊‘𝐵))) | ||
Theorem | sin2h 34884 | Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.) |
⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2))) | ||
Theorem | cos2h 34885 | Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2))) | ||
Theorem | tan2h 34886 | Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴))))) | ||
Theorem | lindsadd 34887 | In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023.) |
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊)) | ||
Theorem | lindsdom 34888 | A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ 𝐼) | ||
Theorem | lindsenlbs 34889 | A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → 𝑋 ∈ (LBasis‘(𝑅 freeLMod 𝐼))) | ||
Theorem | matunitlindflem1 34890 | One direction of matunitlindf 34892. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅))) | ||
Theorem | matunitlindflem2 34891 | One direction of matunitlindf 34892. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)) | ||
Theorem | matunitlindf 34892 | A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼))) | ||
Theorem | ptrest 34893* | Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆)))) | ||
Theorem | ptrecube 34894* | Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.) |
⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))})) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) | ||
Theorem | poimirlem1 34895* | Lemma for poimir 34927- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) & ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) ⇒ ⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) | ||
Theorem | poimirlem2 34896* | Lemma for poimir 34927- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))) & ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ) & ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁)) & ⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉})) ⇒ ⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)) | ||
Theorem | poimirlem3 34897* | Lemma for poimir 34927 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 < 𝑁) & ⊢ (𝜑 → 𝑇:(1...𝑀)⟶(0..^𝐾)) & ⊢ (𝜑 → 𝑈:(1...𝑀)–1-1-onto→(1...𝑀)) ⇒ ⊢ (𝜑 → (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋((𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵 → (〈(𝑇 ∪ {〈(𝑀 + 1), 0〉}), (𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})〉 ∈ (((0..^𝐾) ↑m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∧ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((𝑇 ∪ {〈(𝑀 + 1), 0〉}) ∘f + ((((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ (1...𝑗)) × {1}) ∪ (((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉}) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((𝑇 ∪ {〈(𝑀 + 1), 0〉})‘(𝑀 + 1)) = 0 ∧ ((𝑈 ∪ {〈(𝑀 + 1), (𝑀 + 1)〉})‘(𝑀 + 1)) = (𝑀 + 1))))) | ||
Theorem | poimirlem4 34898* | Lemma for poimir 34927 connecting the admissible faces on the back face of the (𝑀 + 1)-cube to admissible simplices in the 𝑀-cube. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 < 𝑁) ⇒ ⊢ (𝜑 → {𝑠 ∈ (((0..^𝐾) ↑m (1...𝑀)) × {𝑓 ∣ 𝑓:(1...𝑀)–1-1-onto→(1...𝑀)}) ∣ ∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...𝑀)) × {0}))) ∪ (((𝑀 + 1)...𝑁) × {0})) / 𝑝⦌𝐵} ≈ {𝑠 ∈ (((0..^𝐾) ↑m (1...(𝑀 + 1))) × {𝑓 ∣ 𝑓:(1...(𝑀 + 1))–1-1-onto→(1...(𝑀 + 1))}) ∣ (∀𝑖 ∈ (0...𝑀)∃𝑗 ∈ (0...𝑀)𝑖 = ⦋(((1st ‘𝑠) ∘f + ((((2nd ‘𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd ‘𝑠) “ ((𝑗 + 1)...(𝑀 + 1))) × {0}))) ∪ ((((𝑀 + 1) + 1)...𝑁) × {0})) / 𝑝⦌𝐵 ∧ ((1st ‘𝑠)‘(𝑀 + 1)) = 0 ∧ ((2nd ‘𝑠)‘(𝑀 + 1)) = (𝑀 + 1))}) | ||
Theorem | poimirlem5 34899* | Lemma for poimir 34927 to establish that, for the simplices defined by a walk along the edges of an 𝑁-cube, if the starting vertex is not opposite a given face, it is the earliest vertex of the face on the walk. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 0 < (2nd ‘𝑇)) ⇒ ⊢ (𝜑 → (𝐹‘0) = (1st ‘(1st ‘𝑇))) | ||
Theorem | poimirlem6 34900* | Lemma for poimir 34927 establishing, for a face of a simplex defined by a walk along the edges of an 𝑁-cube, the single dimension in which successive vertices before the opposite vertex differ. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓 ∣ 𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < (2nd ‘𝑡), 𝑦, (𝑦 + 1)) / 𝑗⦌((1st ‘(1st ‘𝑡)) ∘f + ((((2nd ‘(1st ‘𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st ‘𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 ∈ (1...((2nd ‘𝑇) − 1))) ⇒ ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |