Description: A ZFC emulation of Hilbert's transfinite axiom. The set B has the properties of Hilbert's epsilon, except that it also depends on a well-ordering R . This theorem arose from discussions with Raph Levien on 5-Mar-2004 about translating the HOL proof language, which uses Hilbert's epsilon. See https://us.metamath.org/downloads/choice.txt (copy of obsolete link http://ghilbert.org/choice.txt) and https://us.metamath.org/downloads/megillaward2005he.pdf .
Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/ . This theorem differs from Hilbert's transfinite axiom described on that page in that it requires R We A as an antecedent. Class A collects the sets of the least rank for which ph ( x ) is true. Class B , which emulates Hilbert's epsilon, is the minimum element in a well-ordering R on A .
If a well-ordering R on A can be expressed in a closed form, as might be the case if we are working with say natural numbers, we can eliminate the antecedent with modus ponens, giving us the exact equivalent of Hilbert's transfinite axiom. Otherwise, we replace R with a dummy setvar variable, say w , and attach w We A as an antecedent in each step of the ZFC version of the HOL proof until the epsilon is eliminated. At that point, B (which will have w as a free variable) will no longer be present, and we can eliminate w We A by applying exlimiv and weth , using scottexs to establish the existence of A .
For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem . (Contributed by NM, 11-Mar-2004) (Revised by Mario Carneiro, 25-Jun-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hta.1 | |- A = { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } |
|
| hta.2 | |- B = ( iota_ z e. A A. w e. A -. w R z ) |
||
| Assertion | hta | |- ( R We A -> ( ph -> [. B / x ]. ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hta.1 | |- A = { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } |
|
| 2 | hta.2 | |- B = ( iota_ z e. A A. w e. A -. w R z ) |
|
| 3 | 19.8a | |- ( ph -> E. x ph ) |
|
| 4 | scott0s | |- ( E. x ph <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } =/= (/) ) |
|
| 5 | 1 | neeq1i | |- ( A =/= (/) <-> { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } =/= (/) ) |
| 6 | 4 5 | bitr4i | |- ( E. x ph <-> A =/= (/) ) |
| 7 | 3 6 | sylib | |- ( ph -> A =/= (/) ) |
| 8 | scottexs | |- { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } e. _V |
|
| 9 | 1 8 | eqeltri | |- A e. _V |
| 10 | 9 2 | htalem | |- ( ( R We A /\ A =/= (/) ) -> B e. A ) |
| 11 | 10 | ex | |- ( R We A -> ( A =/= (/) -> B e. A ) ) |
| 12 | simpl | |- ( ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) -> ph ) |
|
| 13 | 12 | ss2abi | |- { x | ( ph /\ A. y ( [. y / x ]. ph -> ( rank ` x ) C_ ( rank ` y ) ) ) } C_ { x | ph } |
| 14 | 1 13 | eqsstri | |- A C_ { x | ph } |
| 15 | 14 | sseli | |- ( B e. A -> B e. { x | ph } ) |
| 16 | df-sbc | |- ( [. B / x ]. ph <-> B e. { x | ph } ) |
|
| 17 | 15 16 | sylibr | |- ( B e. A -> [. B / x ]. ph ) |
| 18 | 7 11 17 | syl56 | |- ( R We A -> ( ph -> [. B / x ]. ph ) ) |