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 2051 from
ax-13 2245 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 2044. Note that this theorem is also provable from ax-12 2044 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 1894 and spaev 1975 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 1979 | . . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → 𝑥 = 𝑦) | |
2 | 1 | adantl 482 | . . . 4 ⊢ ((𝑦 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑧) → 𝑥 = 𝑦) |
3 | 2 | a1d 25 | . . 3 ⊢ ((𝑦 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
4 | ax13v 2246 | . . . . . . 7 ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | |
5 | equtrr 1946 | . . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 → 𝑥 = 𝑧)) | |
6 | 5 | al2imi 1740 | . . . . . . . 8 ⊢ (∀𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑧)) |
7 | 6 | con3d 148 | . . . . . . 7 ⊢ (∀𝑥 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑥 = 𝑦)) |
8 | 4, 7 | syl6 35 | . . . . . 6 ⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑥 𝑥 = 𝑦))) |
9 | 8 | com13 88 | . . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑦 = 𝑧 → (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦))) |
10 | 9 | impcom 446 | . . . 4 ⊢ ((𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)) |
11 | 10 | con4d 114 | . . 3 ⊢ ((𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
12 | 3, 11 | pm2.61dan 831 | . 2 ⊢ (𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)) |
13 | ax6evr 1939 | . 2 ⊢ ∃𝑧 𝑦 = 𝑧 | |
14 | 12, 13 | exlimiiv 1856 | 1 ⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 ∀wal 1478 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-13 2245 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1702 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |