Description: Remove dependency on ax-13 from dtru . (Contributed by BJ, 31-May-2019)
TODO: This predates the removal of ax-13 in dtru . But actually, sn-dtru is better than either, so move it to Main with sn-el (and determine whether bj-dtru should be kept as ALT or deleted).
(Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-dtru | ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | el | ⊢ ∃ 𝑤 𝑥 ∈ 𝑤 | |
| 2 | ax-nul | ⊢ ∃ 𝑧 ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 | |
| 3 | sp | ⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧 ) | |
| 4 | 2 3 | eximii | ⊢ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧 |
| 5 | exdistrv | ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) ↔ ( ∃ 𝑤 𝑥 ∈ 𝑤 ∧ ∃ 𝑧 ¬ 𝑥 ∈ 𝑧 ) ) | |
| 6 | 1 4 5 | mpbir2an | ⊢ ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) |
| 7 | ax9 | ⊢ ( 𝑤 = 𝑧 → ( 𝑥 ∈ 𝑤 → 𝑥 ∈ 𝑧 ) ) | |
| 8 | 7 | com12 | ⊢ ( 𝑥 ∈ 𝑤 → ( 𝑤 = 𝑧 → 𝑥 ∈ 𝑧 ) ) |
| 9 | 8 | con3dimp | ⊢ ( ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ¬ 𝑤 = 𝑧 ) |
| 10 | 9 | 2eximi | ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑥 ∈ 𝑤 ∧ ¬ 𝑥 ∈ 𝑧 ) → ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 ) |
| 11 | 6 10 | ax-mp | ⊢ ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 |
| 12 | equequ2 | ⊢ ( 𝑧 = 𝑦 → ( 𝑤 = 𝑧 ↔ 𝑤 = 𝑦 ) ) | |
| 13 | 12 | notbid | ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 ↔ ¬ 𝑤 = 𝑦 ) ) |
| 14 | ax7 | ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = 𝑦 → 𝑤 = 𝑦 ) ) | |
| 15 | 14 | con3d | ⊢ ( 𝑥 = 𝑤 → ( ¬ 𝑤 = 𝑦 → ¬ 𝑥 = 𝑦 ) ) |
| 16 | 15 | spimevw | ⊢ ( ¬ 𝑤 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
| 17 | 13 16 | syl6bi | ⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) ) |
| 18 | ax7 | ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → 𝑧 = 𝑦 ) ) | |
| 19 | 18 | con3d | ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑧 = 𝑦 → ¬ 𝑥 = 𝑦 ) ) |
| 20 | 19 | spimevw | ⊢ ( ¬ 𝑧 = 𝑦 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
| 21 | 20 | a1d | ⊢ ( ¬ 𝑧 = 𝑦 → ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) ) |
| 22 | 17 21 | pm2.61i | ⊢ ( ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
| 23 | 22 | exlimivv | ⊢ ( ∃ 𝑤 ∃ 𝑧 ¬ 𝑤 = 𝑧 → ∃ 𝑥 ¬ 𝑥 = 𝑦 ) |
| 24 | 11 23 | ax-mp | ⊢ ∃ 𝑥 ¬ 𝑥 = 𝑦 |
| 25 | exnal | ⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) | |
| 26 | 24 25 | mpbi | ⊢ ¬ ∀ 𝑥 𝑥 = 𝑦 |