MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ex-natded9.26 Structured version   Visualization version   GIF version

Theorem ex-natded9.26 27613
Description: Theorem 9.26 of [Clemente] p. 45, translated line by line using an interpretation of natural deduction in Metamath. This proof has some additional complications due to the fact that Metamath's existential elimination rule does not change bound variables, so we need to verify that 𝑥 is bound in the conclusion. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):
#MPE#ND Expression MPE TranslationND Rationale MPE Rationale
13 𝑥𝑦𝜓(𝑥, 𝑦) (𝜑 → ∃𝑥𝑦𝜓) Given $e.
26 ...| 𝑦𝜓(𝑥, 𝑦) ((𝜑 ∧ ∀𝑦𝜓) → ∀𝑦𝜓) ND hypothesis assumption simpr 473. Later statements will have this scope.
37;5,4 ... 𝜓(𝑥, 𝑦) ((𝜑 ∧ ∀𝑦𝜓) → 𝜓) E 2,y spsbcd 3654 (E), 5,6. To use it we need a1i 11 and vex 3401. This could be immediately done with 19.21bi 2225, but we want to show the general approach for substitution.
412;8,9,10,11 ... 𝑥𝜓(𝑥, 𝑦) ((𝜑 ∧ ∀𝑦𝜓) → ∃𝑥𝜓) I 3,a spesbcd 3724 (I), 11. To use it we need sylibr 225, which in turn requires sylib 209 and two uses of sbcid 3657. This could be more immediately done using 19.8a 2218, but we want to show the general approach for substitution.
513;1,2 𝑥𝜓(𝑥, 𝑦) (𝜑 → ∃𝑥𝜓) E 1,2,4,a exlimdd 2256 (E), 1,2,3,12. We'll need supporting assertions that the variable is free (not bound), as provided in nfv 2005 and nfe1 2195 (MPE# 1,2)
614 𝑦𝑥𝜓(𝑥, 𝑦) (𝜑 → ∀𝑦𝑥𝜓) I 5 alrimiv 2018 (I), 13

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including 𝜑 and uses the Metamath equivalents of the natural deduction rules. Below is the final Metamath proof (which reorders some steps).

Note that in the original proof, 𝜓(𝑥, 𝑦) has explicit parameters. In Metamath, these parameters are always implicit, and the parameters upon which a wff variable can depend are recorded in the "allowed substitution hints" below.

A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded9.26-2 27614.

(Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
Ref Expression
ex-natded9.26.1 (𝜑 → ∃𝑥𝑦𝜓)
Assertion
Ref Expression
ex-natded9.26 (𝜑 → ∀𝑦𝑥𝜓)
Distinct variable group:   𝑥,𝑦,𝜑
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem ex-natded9.26
StepHypRef Expression
1 nfv 2005 . . 3 𝑥𝜑
2 nfe1 2195 . . 3 𝑥𝑥𝜓
3 ex-natded9.26.1 . . 3 (𝜑 → ∃𝑥𝑦𝜓)
4 vex 3401 . . . . . . . 8 𝑦 ∈ V
54a1i 11 . . . . . . 7 ((𝜑 ∧ ∀𝑦𝜓) → 𝑦 ∈ V)
6 simpr 473 . . . . . . 7 ((𝜑 ∧ ∀𝑦𝜓) → ∀𝑦𝜓)
75, 6spsbcd 3654 . . . . . 6 ((𝜑 ∧ ∀𝑦𝜓) → [𝑦 / 𝑦]𝜓)
8 sbcid 3657 . . . . . 6 ([𝑦 / 𝑦]𝜓𝜓)
97, 8sylib 209 . . . . 5 ((𝜑 ∧ ∀𝑦𝜓) → 𝜓)
10 sbcid 3657 . . . . 5 ([𝑥 / 𝑥]𝜓𝜓)
119, 10sylibr 225 . . . 4 ((𝜑 ∧ ∀𝑦𝜓) → [𝑥 / 𝑥]𝜓)
1211spesbcd 3724 . . 3 ((𝜑 ∧ ∀𝑦𝜓) → ∃𝑥𝜓)
131, 2, 3, 12exlimdd 2256 . 2 (𝜑 → ∃𝑥𝜓)
1413alrimiv 2018 1 (𝜑 → ∀𝑦𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1635  wex 1859  wcel 2157  Vcvv 3398  [wsbc 3640
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-v 3400  df-sbc 3641
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator