Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-spae | Structured version Visualization version GIF version |
Description: Prove an instance of sp 2041 from
ax-13 2234 and Tarski's FOL only, without
distinct variable conditions. The antecedent ∀𝑥𝑥 = 𝑦 holds in a
multi-object universe only if 𝑦 is substituted for 𝑥, or
vice
versa, i.e. both variables are effectively the same. The converse
¬ ∀𝑥𝑥 = 𝑦 indicates that both variables are
distinct, and it so
provides a simple translation of a distinct variable condition to a
logical term. In case studies ∀𝑥𝑥 = 𝑦 and ¬
∀𝑥𝑥 = 𝑦 can
help eliminating distinct variable conditions.
The antecedent ∀𝑥𝑥 = 𝑦 is expressed in the theorem's name by the abbreviation ae standing for 'all equal'. Note that we cannot provide a logical predicate telling us directly whether a logical expression contains a particular variable, as such a construct would usually contradict ax-12 2034. Note that this theorem is also provable from ax-12 2034 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 1884 and spaev 1965 having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021.) |
Ref | Expression |
---|---|
wl-spae | ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aeveq 1969 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → 𝑥 = 𝑦) | |
2 | 1 | adantl 481 | . . . 4 ⊢ ((𝑦 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑧) → 𝑥 = 𝑦) |
3 | 2 | a1d 25 | . . 3 ⊢ ((𝑦 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
4 | ax13v 2235 | . . . . . . 7 ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | |
5 | equtrr 1936 | . . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 → 𝑥 = 𝑧)) | |
6 | 5 | al2imi 1733 | . . . . . . . 8 ⊢ (∀𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑧)) |
7 | 6 | con3d 147 | . . . . . . 7 ⊢ (∀𝑥 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑥 = 𝑦)) |
8 | 4, 7 | syl6 34 | . . . . . 6 ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑥 = 𝑦))) |
9 | 8 | com13 86 | . . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑦 = 𝑧 → (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦))) |
10 | 9 | impcom 445 | . . . 4 ⊢ ((𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)) |
11 | 10 | con4d 113 | . . 3 ⊢ ((𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
12 | 3, 11 | pm2.61dan 828 | . 2 ⊢ (𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
13 | ax6evr 1929 | . 2 ⊢ ∃𝑧 𝑦 = 𝑧 | |
14 | 12, 13 | exlimiiv 1846 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-13 2234 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |