![]() |
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 2770 or ax-sep 5167. See dtruALT 5254 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 2379. (Revised by Gino Giotto, 5-Sep-2023.) |
Ref | Expression |
---|---|
dtru | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el 5235 | . . . 4 ⊢ ∃𝑤 𝑥 ∈ 𝑤 | |
2 | ax-nul 5174 | . . . . 5 ⊢ ∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 | |
3 | sp 2180 | . . . . 5 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) | |
4 | 2, 3 | eximii 1838 | . . . 4 ⊢ ∃𝑧 ¬ 𝑥 ∈ 𝑧 |
5 | exdistrv 1956 | . . . 4 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) | |
6 | 1, 4, 5 | mpbir2an 710 | . . 3 ⊢ ∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
7 | ax9v2 2124 | . . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) | |
8 | 7 | com12 32 | . . . . 5 ⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
9 | 8 | con3dimp 412 | . . . 4 ⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
10 | 9 | 2eximi 1837 | . . 3 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
11 | equequ2 2033 | . . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) | |
12 | 11 | notbid 321 | . . . . . 6 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
13 | nfv 1915 | . . . . . . 7 ⊢ Ⅎ𝑥 ¬ 𝑤 = 𝑦 | |
14 | ax7v1 2017 | . . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) | |
15 | 14 | con3d 155 | . . . . . . 7 ⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
16 | 13, 15 | spimefv 2196 | . . . . . 6 ⊢ (¬ 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
17 | 12, 16 | syl6bi 256 | . . . . 5 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
18 | nfv 1915 | . . . . . . 7 ⊢ Ⅎ𝑥 ¬ 𝑧 = 𝑦 | |
19 | ax7v1 2017 | . . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) | |
20 | 19 | con3d 155 | . . . . . . 7 ⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
21 | 18, 20 | spimefv 2196 | . . . . . 6 ⊢ (¬ 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
22 | 21 | a1d 25 | . . . . 5 ⊢ (¬ 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
23 | 17, 22 | pm2.61i 185 | . . . 4 ⊢ (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
24 | 23 | exlimivv 1933 | . . 3 ⊢ (∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
25 | 6, 10, 24 | mp2b 10 | . 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦 |
26 | exnal 1828 | . 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | |
27 | 25, 26 | mpbi 233 | 1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∀wal 1536 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-12 2175 ax-nul 5174 ax-pow 5231 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1541 df-ex 1782 df-nf 1786 |
This theorem is referenced by: dtrucor 5237 dvdemo1 5239 nfnid 5241 axc16b 5255 eunex 5256 brprcneu 6637 zfcndpow 10027 |
Copyright terms: Public domain | W3C validator |