![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dtru | Structured version Visualization version GIF version |
Description: At least two sets exist
(or in terms of first-order logic, the universe
of discourse has two or more objects). Note that we may not substitute
the same variable for both 𝑥 and 𝑦 (as indicated by the
distinct
variable requirement), for otherwise we would contradict stdpc6 2098.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2728 or ax-sep 4921. See dtruALT 5036 for a shorter proof using these axioms. The proof makes use of dummy variables 𝑧 and 𝑤 which do not appear in the final theorem. They must be distinct from each other and from 𝑥 and 𝑦. In other words, if we were to substitute 𝑥 for 𝑧 throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006.) |
Ref | Expression |
---|---|
dtru | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el 4984 | . . . 4 ⊢ ∃𝑤 𝑥 ∈ 𝑤 | |
2 | ax-nul 4929 | . . . . 5 ⊢ ∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 | |
3 | sp 2188 | . . . . 5 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) | |
4 | 2, 3 | eximii 1901 | . . . 4 ⊢ ∃𝑧 ¬ 𝑥 ∈ 𝑧 |
5 | eeanv 2315 | . . . 4 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) | |
6 | 1, 4, 5 | mpbir2an 993 | . . 3 ⊢ ∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
7 | ax9 2140 | . . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) | |
8 | 7 | com12 32 | . . . . 5 ⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
9 | 8 | con3dimp 456 | . . . 4 ⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
10 | 9 | 2eximi 1900 | . . 3 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
11 | equequ2 2096 | . . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) | |
12 | 11 | notbid 307 | . . . . . 6 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
13 | ax7 2086 | . . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) | |
14 | 13 | con3d 148 | . . . . . . 7 ⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
15 | 14 | spimev 2392 | . . . . . 6 ⊢ (¬ 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
16 | 12, 15 | syl6bi 243 | . . . . 5 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
17 | ax7 2086 | . . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) | |
18 | 17 | con3d 148 | . . . . . . 7 ⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
19 | 18 | spimev 2392 | . . . . . 6 ⊢ (¬ 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
20 | 19 | a1d 25 | . . . . 5 ⊢ (¬ 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
21 | 16, 20 | pm2.61i 176 | . . . 4 ⊢ (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
22 | 21 | exlimivv 1997 | . . 3 ⊢ (∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
23 | 6, 10, 22 | mp2b 10 | . 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦 |
24 | exnal 1891 | . 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | |
25 | 23, 24 | mpbi 220 | 1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∀wal 1618 ∃wex 1841 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-nul 4929 ax-pow 4980 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 |
This theorem is referenced by: axc16b 4995 eunex 4996 nfnid 5034 dtrucor 5037 dvdemo1 5039 brprcneu 6333 zfcndpow 9601 |
Copyright terms: Public domain | W3C validator |