Home | Metamath
Proof Explorer Theorem List (p. 358 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wl-cbvalnae 35701 | A more general version of cbval 2399 when nonfree properties depend on a distinctor. Such expressions arise in proofs aiming at the elimination of distinct variable constraints, specifically in application of dvelimf 2449, nfsb2 2488 or dveeq1 2381. (Contributed by Wolf Lammen, 4-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | wl-exeq 35702 | The semantics of ∃𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.) |
⊢ (∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) | ||
Theorem | wl-aleq 35703 | The semantics of ∀𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.) |
⊢ (∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))) | ||
Theorem | wl-nfeqfb 35704 | Extend nfeqf 2382 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.) |
⊢ (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) | ||
Theorem | wl-nfs1t 35705 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Closed form of nfs1 2493. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | wl-equsalvw 35706* |
Version of equsalv 2260 with a disjoint variable condition, and of equsal 2418
with two disjoint variable conditions, which requires fewer axioms. See
also the dual form equsexvw 2009.
This theorem lays the foundation to a transformation of expressions called substitution of set variables in a wff. Only in this particular context we additionally assume 𝜑 and 𝑦 disjoint, stated here as 𝜑(𝑥). Similarly the disjointness of 𝜓 and 𝑥 is expressed by 𝜓(𝑦). Both 𝜑 and 𝜓 may still depend on other set variables, but that is irrelevant here. We want to transform 𝜑(𝑥) into 𝜓(𝑦) such that 𝜓 depends on 𝑦 the same way as 𝜑 depends on 𝑥. This dependency is expressed in our hypothesis (called implicit substitution): (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)). For primitive enough 𝜑 a sort of textual substitution of 𝑥 by 𝑦 is sufficient for such transformation. But note: 𝜑 must not contain wff variables, and the substitution is no proper textual substitution either. We still need grammar information to not accidently replace the x in a token 'x.' denoting multiplication, but only catch set variables 𝑥. Our current stage of development allows only equations and quantifiers make up such primitives. Thanks to equequ1 2029 and cbvalvw 2040 we can then prove in a mechanical way that in fact the implicit substitution holds for each instance. If 𝜑 contains wff variables we cannot use textual transformation any longer, since we don't know how to replace 𝑦 for 𝑥 in placeholders of unknown structure. Our theorem now states, that the generic expression ∀𝑥(𝑥 = 𝑦 → 𝜑) formally behaves as if such a substitution was possible and made. (Contributed by BJ, 31-May-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | wl-equsald 35707 | Deduction version of equsal 2418. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒)) | ||
Theorem | wl-equsal 35708 | A useful equivalence related to substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) It seems proving wl-equsald 35707 first, and then deriving more specialized versions wl-equsal 35708 and wl-equsal1t 35709 then is more efficient than the other way round, which is possible, too. See also equsal 2418. (Revised by Wolf Lammen, 27-Jul-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | wl-equsal1t 35709 |
The expression 𝑥 = 𝑦 in antecedent position plays an
important role in
predicate logic, namely in implicit substitution. However, occasionally
it is irrelevant, and can safely be dropped. A sufficient condition for
this is when 𝑥 (or 𝑦 or both) is not free in
𝜑.
This theorem is more fundamental than equsal 2418, spimt 2387 or sbft 2263, to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | wl-equsalcom 35710 | This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑)) | ||
Theorem | wl-equsal1i 35711 | The antecedent 𝑥 = 𝑦 is irrelevant, if one or both setvar variables are not free in 𝜑. (Contributed by Wolf Lammen, 1-Sep-2018.) |
⊢ (Ⅎ𝑥𝜑 ∨ Ⅎ𝑦𝜑) & ⊢ (𝑥 = 𝑦 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | wl-sb6rft 35712 | A specialization of wl-equsal1t 35709. Closed form of sb6rf 2469. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (Ⅎ𝑥𝜑 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))) | ||
Theorem | wl-cbvalsbi 35713* | Change bounded variables in a special case. The reverse direction seems to involve ax-11 2155. My hope is that I will in some future be able to prove mo3 2565 with reversed quantifiers not using ax-11 2155. See also the remark in mo4 2567, which lead me to this effort. (Contributed by Wolf Lammen, 5-Mar-2024.) |
⊢ (∀𝑥𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | wl-sbrimt 35714 | Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2302. (Contributed by Wolf Lammen, 26-Jul-2019.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))) | ||
Theorem | wl-sblimt 35715 | Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2302. (Contributed by Wolf Lammen, 26-Jul-2019.) |
⊢ (Ⅎ𝑥𝜓 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))) | ||
Theorem | wl-sb8t 35716 | Substitution of variable in universal quantifier. Closed form of sb8 2522. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sb8et 35717 | Substitution of variable in universal quantifier. Closed form of sb8e 2523. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sbhbt 35718 | Closed form of sbhb 2526. Characterizing the expression 𝜑 → ∀𝑥𝜑 using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | wl-sbnf1 35719 | Two ways expressing that 𝑥 is effectively not free in 𝜑. Simplified version of sbnf2 2357. Note: This theorem shows that sbnf2 2357 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (Ⅎ𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | wl-equsb3 35720 | equsb3 2102 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧)) | ||
Theorem | wl-equsb4 35721 | Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable condition. (Contributed by Wolf Lammen, 26-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑦 / 𝑥]𝑦 = 𝑧 ↔ 𝑦 = 𝑧)) | ||
Theorem | wl-2sb6d 35722 | Version of 2sb6 2090 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.) |
⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥) & ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤) & ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧) & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧) ⇒ ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓))) | ||
Theorem | wl-sbcom2d-lem1 35723* | Lemma used to prove wl-sbcom2d 35725. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.) |
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))) | ||
Theorem | wl-sbcom2d-lem2 35724* | Lemma used to prove wl-sbcom2d 35725. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝜑))) | ||
Theorem | wl-sbcom2d 35725 | Version of sbcom2 2162 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.) |
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤) & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧) & ⊢ (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦) ⇒ ⊢ (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓)) | ||
Theorem | wl-sbalnae 35726 | A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-sbal1 35727* | 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 35726 now. See also sbal1 2534. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-sbal2 35728* | 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 35726 now. See also sbal2 2535. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-2spsbbi 35729 | spsbbi 2077 applied twice. (Contributed by Wolf Lammen, 5-Aug-2023.) |
⊢ (∀𝑎∀𝑏(𝜑 ↔ 𝜓) → ([𝑦 / 𝑏][𝑥 / 𝑎]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜓)) | ||
Theorem | wl-lem-exsb 35730* | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | wl-lem-nexmo 35731 | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧)) | ||
Theorem | wl-lem-moexsb 35732* |
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 35733 | This theorem extends alanimi 1819 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | wl-mo2df 35734 | Version of mof 2564 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 35735 | Closed form of mof 2564 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-eudf 35736 | Version of eu6 2575 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 35737 | Closed form of eu6 2575 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) | ||
Theorem | wl-euequf 35738 | euequ 2598 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦) | ||
Theorem | wl-mo2t 35739* | Closed form of mof 2564. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-mo3t 35740* | Closed form of mo3 2565. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) | ||
Theorem | wl-sb8eut 35741 | Substitution of variable in universal quantifier. Closed form of sb8eu 2601. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sb8mot 35742 |
Substitution of variable in universal quantifier. Closed form of
sb8mo 2602.
This theorem relates to wl-mo3t 35740, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2263 and sbco 2512. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 35740 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 35740 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 35743 |
Proving axc11r 2367 from axc11 2431. The hypotheses are two instances of
axc11 2431 used in the proof here. Some systems
introduce axc11 2431 as an
axiom, see for example System S2 in
https://us.metamath.org/downloads/finiteaxiom.pdf 2431.
By contrast, this database sees the variant axc11r 2367, directly derived from ax-12 2172, as foundational. Later axc11 2431 is proven somewhat trickily, requiring ax-10 2138 and ax-13 2373, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.) |
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥)) & ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) ⇒ ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Axiom | ax-wl-11v 35744* | Version of ax-11 2155 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2155. It will later be converted into a theorem directly based on ax-11 2155. (Contributed by Wolf Lammen, 28-Jun-2019.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | wl-ax11-lem1 35745 | A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧)) | ||
Theorem | wl-ax11-lem2 35746* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem3 35747* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem4 35748* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | wl-ax11-lem5 35749 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem6 35750* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem7 35751 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem8 35752* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem9 35753 | The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem10 35754* | We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 191 can be used in conjunction with wl-ax11-lem9 35753 to eliminate the second antecedent. Missing is something along the lines of ax-6 1972, 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 35755* |
Variant of df-clab 2717, 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 2710,
df-clel 2817 and df-cleq 2731. 𝑥 ∈ 𝐴 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 2109, ax-9 2117, or df-clel 2817. Theorem cleljust 2116 shows that a possible choice does not matter. The original df-clab 2717 can be rederived, see wl-dfclab 35756. 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 35756 | Rederive df-clab 2717 from wl-clabv 35755. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.) |
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑) | ||
Theorem | wl-clabtv 35757* | Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 35758. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Theorem | wl-clabt 35758 | Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 35757. (Contributed by Wolf Lammen, 29-May-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
Theorem | rabiun 35759* | Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.) |
⊢ {𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑} = ∪ 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | iundif1 35760* | Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶) | ||
Theorem | imadifss 35761 | The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵)) | ||
Theorem | cureq 35762 | Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → curry 𝐴 = curry 𝐵) | ||
Theorem | unceq 35763 | Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵) | ||
Theorem | curf 35764 | Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵)) | ||
Theorem | uncf 35765 | Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶) | ||
Theorem | curfv 35766 | Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | uncov 35767 | Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵)) | ||
Theorem | curunc 35768 | Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹) | ||
Theorem | unccur 35769 | Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → uncurry curry 𝐹 = 𝐹) | ||
Theorem | phpreu 35770* | Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶)) | ||
Theorem | finixpnum 35771* | A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈ 𝐴 𝐵 ∈ dom card) | ||
Theorem | fin2solem 35772* | Lemma for fin2so 35773. (Contributed by Brendan Leahy, 29-Jun-2019.) |
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) → (𝑦𝑅𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})) | ||
Theorem | fin2so 35773 | 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 35774 | Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) < 𝐵 ↔ 𝐴 < -(⌊‘-𝐵))) | ||
Theorem | leceifl 35775 | Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-(⌊‘-𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (⌊‘𝐵))) | ||
Theorem | sin2h 35776 | Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.) |
⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2))) | ||
Theorem | cos2h 35777 | Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2))) | ||
Theorem | tan2h 35778 | Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.) |
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴))))) | ||
Theorem | lindsadd 35779 | 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 35780 | 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 35781 | 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 35782 | One direction of matunitlindf 35784. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅))) | ||
Theorem | matunitlindflem2 35783 | One direction of matunitlindf 35784. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅)) | ||
Theorem | matunitlindf 35784 | 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 35785* | 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 35786* | 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 35787* | Lemma for poimir 35819- 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 35788* | Lemma for poimir 35819- 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 35789* | Lemma for poimir 35819 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 35790* | Lemma for poimir 35819 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 35791* | Lemma for poimir 35819 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 35792* | Lemma for poimir 35819 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 ‘𝑇))‘𝑀)) | ||
Theorem | poimirlem7 35793* | Lemma for poimir 35819, similar to poimirlem6 35792, but for vertices after the opposite vertex. (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))) & ⊢ (𝜑 → 𝑀 ∈ ((((2nd ‘𝑇) + 1) + 1)...𝑁)) ⇒ ⊢ (𝜑 → (℩𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st ‘𝑇))‘𝑀)) | ||
Theorem | poimirlem8 35794* | Lemma for poimir 35819, establishing that away from the opposite vertex the walks in poimirlem9 35795 yield the same vertices. (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))) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → ((2nd ‘(1st ‘𝑈)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)})) = ((2nd ‘(1st ‘𝑇)) ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))) | ||
Theorem | poimirlem9 35795* | Lemma for poimir 35819, establishing the two walks that yield a given face when the opposite vertex is neither first nor last. (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))) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘(1st ‘𝑈)) ≠ (2nd ‘(1st ‘𝑇))) ⇒ ⊢ (𝜑 → (2nd ‘(1st ‘𝑈)) = ((2nd ‘(1st ‘𝑇)) ∘ ({〈(2nd ‘𝑇), ((2nd ‘𝑇) + 1)〉, 〈((2nd ‘𝑇) + 1), (2nd ‘𝑇)〉} ∪ ( I ↾ ((1...𝑁) ∖ {(2nd ‘𝑇), ((2nd ‘𝑇) + 1)}))))) | ||
Theorem | poimirlem10 35796* | Lemma for poimir 35819 establishing the cube that yields the simplex that yields a face if the opposite vertex was first 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...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) = 0) ⇒ ⊢ (𝜑 → ((𝐹‘(𝑁 − 1)) ∘f − ((1...𝑁) × {1})) = (1st ‘(1st ‘𝑇))) | ||
Theorem | poimirlem11 35797* | Lemma for poimir 35819 connecting walks that could yield from a given cube a given face opposite the first vertex of 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...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) = 0) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑈) = 0) & ⊢ (𝜑 → 𝑀 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀))) | ||
Theorem | poimirlem12 35798* | Lemma for poimir 35819 connecting walks that could yield from a given cube a given face opposite the final vertex of 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...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑇) = 𝑁) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → (2nd ‘𝑈) = 𝑁) & ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1))) ⇒ ⊢ (𝜑 → ((2nd ‘(1st ‘𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st ‘𝑈)) “ (1...𝑀))) | ||
Theorem | poimirlem13 35799* | Lemma for poimir 35819- for at most one simplex associated with a shared face is the opposite vertex first 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...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) ⇒ ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 0) | ||
Theorem | poimirlem14 35800* | Lemma for poimir 35819- for at most one simplex associated with a shared face is the opposite vertex last 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...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁))) ⇒ ⊢ (𝜑 → ∃*𝑧 ∈ 𝑆 (2nd ‘𝑧) = 𝑁) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |