Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f , but this proof is based on fewer axioms.
By the way, swapping x , y and ph , ps leads to an expression for E* y ps , which is equivalent to E* x ph (is a proof line), so the right hand side is a rare instance of an expression where swapping the quantifiers can be done without ax-11 . (Contributed by NM, 26-Jul-1995) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mo4.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | mo4 | ⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mo4.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | df-mo | ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) | |
| 3 | equequ1 | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) ) | |
| 4 | 1 3 | imbi12d | ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → 𝑥 = 𝑧 ) ↔ ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 5 | 4 | cbvalvw | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 6 | 5 | biimpi | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 7 | pm2.27 | ⊢ ( 𝜑 → ( ( 𝜑 → 𝑥 = 𝑧 ) → 𝑥 = 𝑧 ) ) | |
| 8 | pm2.27 | ⊢ ( 𝜓 → ( ( 𝜓 → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) ) | |
| 9 | 7 8 | im2anan9 | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝜑 → 𝑥 = 𝑧 ) ∧ ( 𝜓 → 𝑦 = 𝑧 ) ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑧 ) ) ) |
| 10 | equtr2 | ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑧 ) → 𝑥 = 𝑦 ) | |
| 11 | 9 10 | syl6com | ⊢ ( ( ( 𝜑 → 𝑥 = 𝑧 ) ∧ ( 𝜓 → 𝑦 = 𝑧 ) ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 12 | 11 | ex | ⊢ ( ( 𝜑 → 𝑥 = 𝑧 ) → ( ( 𝜓 → 𝑦 = 𝑧 ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 13 | 12 | alimdv | ⊢ ( ( 𝜑 → 𝑥 = 𝑧 ) → ( ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) → ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 14 | 13 | com12 | ⊢ ( ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) → ( ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 15 | 14 | alimdv | ⊢ ( ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 16 | 6 15 | mpcom | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 17 | 16 | exlimiv | ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 18 | 2 17 | sylbi | ⊢ ( ∃* 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 19 | 1 | cbvexvw | ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) |
| 20 | 19 | biimpri | ⊢ ( ∃ 𝑦 𝜓 → ∃ 𝑥 𝜑 ) |
| 21 | ax6evr | ⊢ ∃ 𝑧 𝑥 = 𝑧 | |
| 22 | pm3.2 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) ) | |
| 23 | 22 | imim1d | ⊢ ( 𝜑 → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → 𝑥 = 𝑦 ) ) ) |
| 24 | ax7 | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) ) | |
| 25 | 23 24 | syl8 | ⊢ ( 𝜑 → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) ) ) ) |
| 26 | 25 | com4r | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → 𝑦 = 𝑧 ) ) ) ) |
| 27 | 26 | impcom | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑧 ) → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 28 | 27 | alimdv | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑧 ) → ( ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 29 | 28 | impancom | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ( 𝑥 = 𝑧 → ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 30 | 29 | eximdv | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ( ∃ 𝑧 𝑥 = 𝑧 → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 31 | 21 30 | mpi | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 32 | df-mo | ⊢ ( ∃* 𝑦 𝜓 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) | |
| 33 | 31 32 | sylibr | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ∃* 𝑦 𝜓 ) |
| 34 | 33 | expcom | ⊢ ( ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜑 → ∃* 𝑦 𝜓 ) ) |
| 35 | 34 | aleximi | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ∃* 𝑦 𝜓 ) ) |
| 36 | ax5e | ⊢ ( ∃ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 𝜓 ) | |
| 37 | 20 35 36 | syl56 | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑦 𝜓 → ∃* 𝑦 𝜓 ) ) |
| 38 | 5 | exbii | ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 39 | 38 2 32 | 3bitr4i | ⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 ) |
| 40 | moabs | ⊢ ( ∃* 𝑦 𝜓 ↔ ( ∃ 𝑦 𝜓 → ∃* 𝑦 𝜓 ) ) | |
| 41 | 39 40 | bitri | ⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑦 𝜓 → ∃* 𝑦 𝜓 ) ) |
| 42 | 37 41 | sylibr | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ∃* 𝑥 𝜑 ) |
| 43 | 18 42 | impbii | ⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |