| Mathbox for Zhi Wang |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > dtrucor3 | Structured version Visualization version GIF version | ||
| Description: An example of how ax-5 1910 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5441 in the ZF set theory. axc16nf 2263 and euae 2660 demonstrate that the violation of dtru 5441 leads to a model with only one object assuming its existence (ax-6 1967). The conclusion is also provable in the empty model ( see emptyal 1908). See also nf5 2282 and nf5i 2146 for the relation between unconditional ax-5 1910 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.) |
| Ref | Expression |
|---|---|
| dtrucor3.1 | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
| dtrucor3.2 | ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦) |
| Ref | Expression |
|---|---|
| dtrucor3 | ⊢ ∀𝑥 𝑥 = 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax6ev 1969 | . 2 ⊢ ∃𝑥 𝑥 = 𝑦 | |
| 2 | dtrucor3.1 | . . . 4 ⊢ ¬ ∀𝑥 𝑥 = 𝑦 | |
| 3 | dtrucor3.2 | . . . 4 ⊢ (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦) | |
| 4 | 2, 3 | mto 197 | . . 3 ⊢ ¬ 𝑥 = 𝑦 |
| 5 | 4 | nex 1800 | . 2 ⊢ ¬ ∃𝑥 𝑥 = 𝑦 |
| 6 | 1, 5 | pm2.24ii 120 | 1 ⊢ ∀𝑥 𝑥 = 𝑦 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-6 1967 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |