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 2031.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2709, ax-sep 5222, or ax-pow 5287. See dtruALT 5310 for a shorter proof using these axioms, and see dtruALT2 5292 for a proof that uses ax-pow 5287 instead of ax-pr 5351. 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 2372. (Revised by Gino Giotto, 5-Sep-2023.) Avoid ax-12 2171. (Revised by Rohan Ridenour, 9-Oct-2024.) Use ax-pr 5351 instead of ax-pow 5287. (Revised by BTernaryTau, 3-Dec-2024.) |
Ref | Expression |
---|---|
dtru | ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el 5356 | . . . 4 ⊢ ∃𝑤 𝑥 ∈ 𝑤 | |
2 | ax-nul 5229 | . . . . 5 ⊢ ∃𝑧∀𝑥 ¬ 𝑥 ∈ 𝑧 | |
3 | elequ1 2113 | . . . . . . 7 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝑧 ↔ 𝑤 ∈ 𝑧)) | |
4 | 3 | notbid 318 | . . . . . 6 ⊢ (𝑥 = 𝑤 → (¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑤 ∈ 𝑧)) |
5 | 4 | spw 2037 | . . . . 5 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧) |
6 | 2, 5 | eximii 1839 | . . . 4 ⊢ ∃𝑧 ¬ 𝑥 ∈ 𝑧 |
7 | exdistrv 1959 | . . . 4 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) ↔ (∃𝑤 𝑥 ∈ 𝑤 ∧ ∃𝑧 ¬ 𝑥 ∈ 𝑧)) | |
8 | 1, 6, 7 | mpbir2an 708 | . . 3 ⊢ ∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) |
9 | ax9v2 2119 | . . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧)) | |
10 | 9 | com12 32 | . . . . 5 ⊢ (𝑥 ∈ 𝑤 → (𝑤 = 𝑧 → 𝑥 ∈ 𝑧)) |
11 | 10 | con3dimp 409 | . . . 4 ⊢ ((𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ¬ 𝑤 = 𝑧) |
12 | 11 | 2eximi 1838 | . . 3 ⊢ (∃𝑤∃𝑧(𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧) → ∃𝑤∃𝑧 ¬ 𝑤 = 𝑧) |
13 | equequ2 2029 | . . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑤 = 𝑧 ↔ 𝑤 = 𝑦)) | |
14 | 13 | notbid 318 | . . . . . 6 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦)) |
15 | ax7v1 2013 | . . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝑦 → 𝑤 = 𝑦)) | |
16 | 15 | con3d 152 | . . . . . . 7 ⊢ (𝑥 = 𝑤 → (¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦)) |
17 | 16 | spimevw 1998 | . . . . . 6 ⊢ (¬ 𝑤 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
18 | 14, 17 | syl6bi 252 | . . . . 5 ⊢ (𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
19 | ax7v1 2013 | . . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 → 𝑧 = 𝑦)) | |
20 | 19 | con3d 152 | . . . . . . 7 ⊢ (𝑥 = 𝑧 → (¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦)) |
21 | 20 | spimevw 1998 | . . . . . 6 ⊢ (¬ 𝑧 = 𝑦 → ∃𝑥 ¬ 𝑥 = 𝑦) |
22 | 21 | a1d 25 | . . . . 5 ⊢ (¬ 𝑧 = 𝑦 → (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦)) |
23 | 18, 22 | pm2.61i 182 | . . . 4 ⊢ (¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
24 | 23 | exlimivv 1935 | . . 3 ⊢ (∃𝑤∃𝑧 ¬ 𝑤 = 𝑧 → ∃𝑥 ¬ 𝑥 = 𝑦) |
25 | 8, 12, 24 | mp2b 10 | . 2 ⊢ ∃𝑥 ¬ 𝑥 = 𝑦 |
26 | exnal 1829 | . 2 ⊢ (∃𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦) | |
27 | 25, 26 | mpbi 229 | 1 ⊢ ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∀wal 1537 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-nul 5229 ax-pr 5351 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-ex 1783 |
This theorem is referenced by: brprcneu 6757 zfcndpow 10360 |
Copyright terms: Public domain | W3C validator |