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 x and y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 .
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext , ax-sep , or ax-pow . See dtruALT for a shorter proof using these axioms, and see dtruALT2 for a proof that uses ax-pow instead of ax-pr .
The proof makes use of dummy variables z and w which do not appear in the final theorem. They must be distinct from each other and from x and y . In other words, if we were to substitute x for z throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by Gino Giotto, 5-Sep-2023) Avoid ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024) Use ax-pr instead of ax-pow . (Revised by BTernaryTau, 3-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | dtru | ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | el | ⊢ ∃ 𝑤 𝑥 ∈ 𝑤 | |
2 | ax-nul | ⊢ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 | |
3 | elequ1 | ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝑧 ↔ 𝑤 ∈ 𝑧 ) ) | |
4 | 3 | notbid | ⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑤 ∈ 𝑧 ) ) |
5 | 4 | spw | ⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧 ) |
6 | 2 5 | eximii | ⊢ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧 |
7 | exdistrv | ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) ↔ ( ∃ 𝑤 𝑥 ∈ 𝑤 ∧ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧 ) ) | |
8 | 1 6 7 | mpbir2an | ⊢ ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) |
9 | ax9v2 | ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧 ) ) | |
10 | 9 | com12 | ⊢ ( 𝑥 ∈ 𝑤 → ( 𝑤 = 𝑧 → 𝑥 ∈ 𝑧 ) ) |
11 | 10 | con3dimp | ⊢ ( ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ¬ 𝑤 = 𝑧 ) |
12 | 11 | 2eximi | ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 ) |
13 | equequ2 | ⊢ ( 𝑧 = 𝑦 → ( 𝑤 = 𝑧 ↔ 𝑤 = 𝑦 ) ) | |
14 | 13 | notbid | ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦 ) ) |
15 | ax7v1 | ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → 𝑤 = 𝑦 ) ) | |
16 | 15 | con3d | ⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦 ) ) |
17 | 16 | spimevw | ⊢ ( ¬ 𝑤 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
18 | 14 17 | syl6bi | ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) ) |
19 | ax7v1 | ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) ) | |
20 | 19 | con3d | ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦 ) ) |
21 | 20 | spimevw | ⊢ ( ¬ 𝑧 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
22 | 21 | a1d | ⊢ ( ¬ 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) ) |
23 | 18 22 | pm2.61i | ⊢ ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
24 | 23 | exlimivv | ⊢ ( ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
25 | 8 12 24 | mp2b | ⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦 |
26 | exnal | ⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) | |
27 | 25 26 | mpbi | ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 |