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 2035.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2793 or ax-sep 5203. See dtruALT 5289 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.) Avoid ax-13 2390. (Revised by Gino Giotto, 5-Sep-2023.) |
Ref | Expression |
---|---|
dtru | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el 5270 | . . . 4 ⊢ ∃𝑤 𝑥 ∈ 𝑤 | |
2 | ax-nul 5210 | . . . . 5 ⊢ ∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 | |
3 | sp 2182 | . . . . 5 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) | |
4 | 2, 3 | eximii 1837 | . . . 4 ⊢ ∃𝑧 ¬ 𝑥 ∈ 𝑧 |
5 | exdistrv 1956 | . . . 4 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) | |
6 | 1, 4, 5 | mpbir2an 709 | . . 3 ⊢ ∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
7 | ax9v2 2127 | . . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) | |
8 | 7 | com12 32 | . . . . 5 ⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
9 | 8 | con3dimp 411 | . . . 4 ⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
10 | 9 | 2eximi 1836 | . . 3 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
11 | equequ2 2033 | . . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) | |
12 | 11 | notbid 320 | . . . . . 6 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
13 | nfv 1915 | . . . . . . 7 ⊢ Ⅎ𝑥 ¬ 𝑤 = 𝑦 | |
14 | ax7v1 2017 | . . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) | |
15 | 14 | con3d 155 | . . . . . . 7 ⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
16 | 13, 15 | spimefv 2198 | . . . . . 6 ⊢ (¬ 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
17 | 12, 16 | syl6bi 255 | . . . . 5 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
18 | nfv 1915 | . . . . . . 7 ⊢ Ⅎ𝑥 ¬ 𝑧 = 𝑦 | |
19 | ax7v1 2017 | . . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) | |
20 | 19 | con3d 155 | . . . . . . 7 ⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
21 | 18, 20 | spimefv 2198 | . . . . . 6 ⊢ (¬ 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
22 | 21 | a1d 25 | . . . . 5 ⊢ (¬ 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
23 | 17, 22 | pm2.61i 184 | . . . 4 ⊢ (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
24 | 23 | exlimivv 1933 | . . 3 ⊢ (∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
25 | 6, 10, 24 | mp2b 10 | . 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦 |
26 | exnal 1827 | . 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | |
27 | 25, 26 | mpbi 232 | 1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 ∀wal 1535 ∃wex 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-12 2177 ax-nul 5210 ax-pow 5266 |
This theorem depends on definitions: df-bi 209 df-an 399 df-tru 1540 df-ex 1781 df-nf 1785 |
This theorem is referenced by: dtrucor 5272 dvdemo1 5274 nfnid 5276 axc16b 5290 eunex 5291 brprcneu 6662 zfcndpow 10038 |
Copyright terms: Public domain | W3C validator |