Theorem hta 9901

Description: A ZFC emulation of Hilbert's transfinite axiom. The set 𝐵 has the properties of Hilbert's epsilon, except that it also depends on a well-ordering 𝑅. 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 𝑅 We 𝐴 as an antecedent. Class 𝐴 collects the sets of the least rank for which 𝜑(𝑥) is true. Class 𝐵, which emulates Hilbert's epsilon, is the minimum element in a well-ordering 𝑅 on 𝐴.

If a well-ordering 𝑅 on 𝐴 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 𝑅 with a dummy setvar variable, say 𝑤, and attach 𝑤 We 𝐴 as an antecedent in each step of the ZFC version of the HOL proof until the epsilon is eliminated. At that point, 𝐵 (which will have 𝑤 as a free variable) will no longer be present, and we can eliminate 𝑤 We 𝐴 by applying exlimiv 1963 and weth 10497, using scottex 9872 to establish the existence of 𝐴.

For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 9900. (Contributed by NM, 11-Mar-2004.) (Revised by Mario Carneiro, 25-Jun-2015.) Use the Scott operation. (Revised by BTernaryTau, 22-Jul-2026.)

Hypotheses

Ref	Expression
hta.1	⊢ 𝐴 = Scott {𝑥 ∣ 𝜑}
hta.2	⊢ 𝐵 = (℩𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ¬ 𝑧𝑅𝑦)

Assertion

Ref	Expression
hta	⊢ (𝑅 We 𝐴 → (𝜑 → [𝐵 / 𝑥]𝜑))

Distinct variable groups:   𝑦,𝐴,𝑧   𝑦,𝑅,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧)   𝐴(𝑥)   𝐵(𝑥, 𝑦, 𝑧)   𝑅(𝑥)

Proof of Theorem hta

Step	Hyp	Ref	Expression
1		19.8a 2217	. . 3 ⊢ (𝜑 → ∃𝑥𝜑)
2		scott0bs 9883	. . . 4 ⊢ (∃𝑥𝜑 ↔ Scott {𝑥 ∣ 𝜑} ≠ ∅)
3		hta.1	. . . . 5 ⊢ 𝐴 = Scott {𝑥 ∣ 𝜑}
4	3	neeq1i 3019	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ Scott {𝑥 ∣ 𝜑} ≠ ∅)
5	2, 4	bitr4i 281	. . 3 ⊢ (∃𝑥𝜑 ↔ 𝐴 ≠ ∅)
6	1, 5	sylib 221	. 2 ⊢ (𝜑 → 𝐴 ≠ ∅)
7		scottex 9872	. . . . 5 ⊢ Scott {𝑥 ∣ 𝜑} ∈ V
8	3, 7	eqeltri 2856	. . . 4 ⊢ 𝐴 ∈ V
9		hta.2	. . . 4 ⊢ 𝐵 = (℩𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ¬ 𝑧𝑅𝑦)
10	8, 9	htalem 9900	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝐴 ≠ ∅) → 𝐵 ∈ 𝐴)
11	10	ex 418	. 2 ⊢ (𝑅 We 𝐴 → (𝐴 ≠ ∅ → 𝐵 ∈ 𝐴))
12		scottss 9874	. . . . 5 ⊢ Scott {𝑥 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑}
13	3, 12	eqsstri 3977	. . . 4 ⊢ 𝐴 ⊆ {𝑥 ∣ 𝜑}
14	13	sseli 3927	. . 3 ⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ {𝑥 ∣ 𝜑})
15		df-sbc 3740	. . 3 ⊢ ([𝐵 / 𝑥]𝜑 ↔ 𝐵 ∈ {𝑥 ∣ 𝜑})
16	14, 15	sylibr 237	. 2 ⊢ (𝐵 ∈ 𝐴 → [𝐵 / 𝑥]𝜑)
17	6, 11, 16	syl56 37	1 ⊢ (𝑅 We 𝐴 → (𝜑 → [𝐵 / 𝑥]𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738   ≠ wne 2955  ∀wral 3076  Vcvv 3450  [wsbc 3739  ∅c0 4279   class class class wbr 5103   We wwe 5607  ℩crio 7369  Scott cscott 9867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-reg 9564  ax-inf2 9620

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-r1 9746  df-rank 9747  df-scott 9868

This theorem is used by: (None)