Theorem hta 3619

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-04 about translating the HOL proof language, which uses Hilbert's epsilon.

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 952 and weth 3602, using scottexs 3543 to establish the existence of A.

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

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 group(s):   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 2190	. . . . 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 6	. . . 4 |- (R We A <-> R We {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
4		scottexs 3543	. . . . . 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 925	. . . . . . . . . . . . . . . 16 |- (ph -> A.yph)
7		hba1 698	. . . . . . . . . . . . . . . 16 |- (A.y([y / x]ph -> (rank` x) (_ (rank` y)) -> A.yA.y([y / x]ph -> (rank` x) (_ (rank` y)))
8	6, 7	hban 704	. . . . . . . . . . . . . . 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 1096	. . . . . . . . . . . . . 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	eleq2i 1153	. . . . . . . . . . . . . 14 |- (z e. A <-> z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
11	10	bial 695	. . . . . . . . . . . . . 14 |- (A.y z e. A <-> A.y z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
12	9, 10, 11	3imtr4 192	. . . . . . . . . . . . 13 |- (z e. A -> A.y z e. A)
13	12, 9	raleqf 1321	. . . . . . . . . . . 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))
14	1, 13	ax-mp 6	. . . . . . . . . . 11 |- (A.y e. A -. yRx <-> A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx)
15	14	a1i 7	. . . . . . . . . 10 |- (x e. A -> (A.y e. A -. yRx <-> A.y e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))} -. yRx))
16	15	birabi 1342	. . . . . . . . 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}
17		hbab1 1095	. . . . . . . . . . . 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)))})
18	10	bial 695	. . . . . . . . . . . 12 |- (A.x z e. A <-> A.x z e. {x | (ph /\ A.y([y / x]ph -> (rank` x) (_ (rank` y)))})
19	17, 10, 18	3imtr4 192	. . . . . . . . . . 11 |- (z e. A -> A.x z e. A)
20	19, 17	rabeqf 1345	. . . . . . . . . 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})
21	1, 20	ax-mp 6	. . . . . . . . 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}
22		hbab1 1095	. . . . . . . . . . 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)))})
23		ax-17 925	. . . . . . . . . . 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)))})
24		ax-17 925	. . . . . . . . . . 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)
25		hbab1 1095	. . . . . . . . . . . 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)))})
26		ax-17 925	. . . . . . . . . . . 12 |- (-. yRz -> A.x -. yRz)
27	25, 26	hbral 1236	. . . . . . . . . . 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)
28		breq2 2066	. . . . . . . . . . . . 13 |- (x = z -> (yRx <-> yRz))
29	28	negbid 463	. . . . . . . . . . . 12 |- (x = z -> (-. yRx <-> -. yRz))
30	29	biraldv 1219	. . . . . . . . . . 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))
31	22, 23, 24, 27, 30	cbvrab 1425	. . . . . . . . . 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}
32		ax-17 925	. . . . . . . . . . . . 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)))})
33		ax-17 925	. . . . . . . . . . . . 13 |- (-. yRz -> A.v -. yRz)
34		ax-17 925	. . . . . . . . . . . . 13 |- (-. vRz -> A.y -. vRz)
35		breq1 2065	. . . . . . . . . . . . . 14 |- (y = v -> (yRz <-> vRz))
36	35	negbid 463	. . . . . . . . . . . . 13 |- (y = v -> (-. yRz <-> -. vRz))
37	9, 32, 33, 34, 36	cbvralf 1330	. . . . . . . . . . . 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)
38	37	a1i 7	. . . . . . . . . . 11 |- (z e. {x | (