Theorem hta 4708

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 http://ghilbert.org/choice.txt and http://us.metamath.org/downloads/megillaward2004.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 least rank for which ph(x) is true. Class B, which emulates the 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 set 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 19.23aiv 1293 and weth 4767, using scottexs 4698 to establish the existence of A.

For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 4707.

Hypotheses

Ref	Expression
hta.1	|- A = {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))}
hta.2	|- B = U.{x e. A | A.y e. A -. yRx}

Assertion

Ref	Expression
hta	|- (R We A -> (ph -> [B / x]ph))

Distinct variable groups:   x,y,R   ph,y

Proof of Theorem hta

Step	Hyp	Ref	Expression
1		hta.1	. . . . 5 |- A = {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))}
2		weeq2 2933	. . . . 5 |- (A = {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> (R We A <-> R We {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))}))
3	1, 2	ax-mp 7	. . . 4 |- (R We A <-> R We {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
4		scottexs 4698	. . . . . 6 |- {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} e. V
5		hta.2	. . . . . . 7 |- B = U.{x e. A | A.y e. A -. yRx}
6		ax-17 969	. . . . . . . . . . . . . . . 16 |- (ph -> A.yph)
7		hba1 1001	. . . . . . . . . . . . . . . 16 |- (A.y([y / x]ph -> (rank` x) (_ (rank` y)) -> A.yA.y([y / x]ph -> (rank` x) (_ (rank` y)))
8	6, 7	hban 1007	. . . . . . . . . . . . . . 15 |- ((ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y))) -> A.y(ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y))))
9	8	hbab 1465	. . . . . . . . . . . . . 14 |- (z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> A.y z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
10	1, 9	hbxfr 1560	. . . . . . . . . . . . 13 |- (z e. A -> A.y z e. A)
11	10, 9	raleq1f 1780	. . . . . . . . . . . 12 |- (A = {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> (A.y e. A -. yRx <-> A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx))
12	1, 11	ax-mp 7	. . . . . . . . . . 11 |- (A.y e. A -. yRx <-> A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx)
13	12	a1i 8	. . . . . . . . . 10 |- (x e. A -> (A.y e. A -. yRx <-> A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx))
14	13	rabbii 1801	. . . . . . . . 9 |- {x e. A | A.y e. A -. yRx} = {x e. A | A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx}
15		hbab1 1464	. . . . . . . . . . . 12 |- (z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> A.x z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
16	1, 15	hbxfr 1560	. . . . . . . . . . 11 |- (z e. A -> A.x z e. A)
17	16, 15	rabeqf 1804	. . . . . . . . . 10 |- (A = {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> {x e. A | A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx} = {x e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} | A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx})
18	1, 17	ax-mp 7	. . . . . . . . 9 |- {x e. A | A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx} = {x e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} | A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx}
19		hbab1 1464	. . . . . . . . . . 11 |- (v e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> A.x v e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
20		ax-17 969	. . . . . . . . . . 11 |- (v e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> A.z v e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
21		ax-17 969	. . . . . . . . . . 11 |- (A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx -> A.zA.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx)
22		hbab1 1464	. . . . . . . . . . . 12 |- (y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> A.x y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
23		ax-17 969	. . . . . . . . . . . 12 |- (-. yRz -> A.x -. yRz)
24	22, 23	hbral 1683	. . . . . . . . . . 11 |- (A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRz -> A.xA.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRz)
25		breq2 2618	. . . . . . . . . . . . 13 |- (x = z -> (yRx <-> yRz))
26	25	negbid 610	. . . . . . . . . . . 12 |- (x = z -> (-. yRx <-> -. yRz))
27	26	ralbidv 1660	. . . . . . . . . . 11 |- (x = z -> (A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx <-> A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRz))
28	19, 20, 21, 24, 27	cbvrab 1906	. . . . . . . . . 10 |- {x e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} | A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx} = {z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} | A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRz}
29		ax-17 969	. . . . . . . . . . . . 13 |- (z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> A.v z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
30		ax-17 969	. . . . . . . . . . . . 13 |- (-. yRz -> A.v -. yRz)
31		ax-17 969	. . . . . . . . . . . . 13 |- (-. vRz -> A.y -. vRz)
32		breq1 2617	. . . . . . . . . . . . . 14 |- (y = v -> (yRz <-> vRz))
33	32	negbid 610	. . . . . . . . . . . . 13 |- (y = v -> (-. yRz <-> -. vRz))
34	9, 29, 30, 31, 33	cbvralf 1793	. . . . . . . . . . . 12 |- (A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRz <-> A.v e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. vRz)
35	34	a1i 8	. . . . . . . . . . 11 |- (z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -> (A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRz <-> A.v e. {x | (ph /\ A.y([y / x]ph