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 | 7 | adantr | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 → 𝑥 = 𝑧 ) → 𝑥 = 𝑧 ) ) |
| 9 | pm2.27 | ⊢ ( 𝜓 → ( ( 𝜓 → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) ) | |
| 10 | 9 | adantl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜓 → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) ) |
| 11 | 8 10 | anim12d | ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝜑 → 𝑥 = 𝑧 ) ∧ ( 𝜓 → 𝑦 = 𝑧 ) ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑧 ) ) ) |
| 12 | equtr2 | ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑧 ) → 𝑥 = 𝑦 ) | |
| 13 | 11 12 | syl6com | ⊢ ( ( ( 𝜑 → 𝑥 = 𝑧 ) ∧ ( 𝜓 → 𝑦 = 𝑧 ) ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 14 | 13 | ex | ⊢ ( ( 𝜑 → 𝑥 = 𝑧 ) → ( ( 𝜓 → 𝑦 = 𝑧 ) → ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 15 | 14 | alimdv | ⊢ ( ( 𝜑 → 𝑥 = 𝑧 ) → ( ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) → ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 16 | 15 | com12 | ⊢ ( ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) → ( ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 17 | 16 | alimdv | ⊢ ( ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) ) |
| 18 | 6 17 | mpcom | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 19 | 18 | exlimiv | ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 20 | 2 19 | sylbi | ⊢ ( ∃* 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |
| 21 | 1 | cbvexvw | ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 ) |
| 22 | 21 | biimpri | ⊢ ( ∃ 𝑦 𝜓 → ∃ 𝑥 𝜑 ) |
| 23 | ax6evr | ⊢ ∃ 𝑧 𝑥 = 𝑧 | |
| 24 | pm3.2 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) ) | |
| 25 | 24 | imim1d | ⊢ ( 𝜑 → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → 𝑥 = 𝑦 ) ) ) |
| 26 | ax7 | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) ) | |
| 27 | 25 26 | syl8 | ⊢ ( 𝜑 → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) ) ) ) |
| 28 | 27 | com4r | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → 𝑦 = 𝑧 ) ) ) ) |
| 29 | 28 | impcom | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑧 ) → ( ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 30 | 29 | alimdv | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑧 ) → ( ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 31 | 30 | impancom | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ( 𝑥 = 𝑧 → ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 32 | 31 | eximdv | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ( ∃ 𝑧 𝑥 = 𝑧 → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) ) |
| 33 | 23 32 | mpi | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 34 | df-mo | ⊢ ( ∃* 𝑦 𝜓 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) | |
| 35 | 33 34 | sylibr | ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) → ∃* 𝑦 𝜓 ) |
| 36 | 35 | expcom | ⊢ ( ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( 𝜑 → ∃* 𝑦 𝜓 ) ) |
| 37 | 36 | aleximi | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ∃* 𝑦 𝜓 ) ) |
| 38 | ax5e | ⊢ ( ∃ 𝑥 ∃* 𝑦 𝜓 → ∃* 𝑦 𝜓 ) | |
| 39 | 22 37 38 | syl56 | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑦 𝜓 → ∃* 𝑦 𝜓 ) ) |
| 40 | 5 | exbii | ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) ) |
| 41 | 40 2 34 | 3bitr4i | ⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 ) |
| 42 | moabs | ⊢ ( ∃* 𝑦 𝜓 ↔ ( ∃ 𝑦 𝜓 → ∃* 𝑦 𝜓 ) ) | |
| 43 | 41 42 | bitri | ⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑦 𝜓 → ∃* 𝑦 𝜓 ) ) |
| 44 | 39 43 | sylibr | ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) → ∃* 𝑥 𝜑 ) |
| 45 | 20 44 | impbii | ⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) ) |