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 2026.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2790 or ax-sep 5194. See dtruALT 5279 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 2381. (Revised by Gino Giotto, 5-Sep-2023.) |
Ref | Expression |
---|---|
dtru | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el 5261 | . . . 4 ⊢ ∃𝑤 𝑥 ∈ 𝑤 | |
2 | ax-nul 5201 | . . . . 5 ⊢ ∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 | |
3 | sp 2172 | . . . . 5 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) | |
4 | 2, 3 | eximii 1828 | . . . 4 ⊢ ∃𝑧 ¬ 𝑥 ∈ 𝑧 |
5 | exdistrv 1947 | . . . 4 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) | |
6 | 1, 4, 5 | mpbir2an 707 | . . 3 ⊢ ∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
7 | ax9v2 2118 | . . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) | |
8 | 7 | com12 32 | . . . . 5 ⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
9 | 8 | con3dimp 409 | . . . 4 ⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
10 | 9 | 2eximi 1827 | . . 3 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
11 | equequ2 2024 | . . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) | |
12 | 11 | notbid 319 | . . . . . 6 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
13 | nfv 1906 | . . . . . . 7 ⊢ Ⅎ𝑥 ¬ 𝑤 = 𝑦 | |
14 | ax7v1 2008 | . . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) | |
15 | 14 | con3d 155 | . . . . . . 7 ⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
16 | 13, 15 | spimefv 2188 | . . . . . 6 ⊢ (¬ 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
17 | 12, 16 | syl6bi 254 | . . . . 5 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
18 | nfv 1906 | . . . . . . 7 ⊢ Ⅎ𝑥 ¬ 𝑧 = 𝑦 | |
19 | ax7v1 2008 | . . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) | |
20 | 19 | con3d 155 | . . . . . . 7 ⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
21 | 18, 20 | spimefv 2188 | . . . . . 6 ⊢ (¬ 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
22 | 21 | a1d 25 | . . . . 5 ⊢ (¬ 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
23 | 17, 22 | pm2.61i 183 | . . . 4 ⊢ (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
24 | 23 | exlimivv 1924 | . . 3 ⊢ (∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
25 | 6, 10, 24 | mp2b 10 | . 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦 |
26 | exnal 1818 | . 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | |
27 | 25, 26 | mpbi 231 | 1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-12 2167 ax-nul 5201 ax-pow 5257 |
This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1531 df-ex 1772 df-nf 1776 |
This theorem is referenced by: dtrucor 5263 dvdemo1 5265 nfnid 5267 axc16b 5280 eunex 5281 brprcneu 6655 zfcndpow 10026 |
Copyright terms: Public domain | W3C validator |