Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

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 φ(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∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}
hta.2	⊢ B = ∪{x ∈ A∣∀y ∈ A ¬ yRx}

**Assertion**
Ref	Expression
hta	⊢ (R We A → (φ → [B / x]φ))

Distinct variable group(s): x,y,R φ,y

**Proof of Theorem hta**
Step	Hyp	Ref	Expression
1		hta.1	. . . . 5 ⊢ A = {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}
2		weeq2 2190	. . . . 5 ⊢ (A = {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → (R We A ↔ R We {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}))
3	1, 2	ax-mp 6	. . . 4 ⊢ (R We A ↔ R We {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
4		scottexs 3543	. . . . . 6 ⊢ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ∈ V
5		hta.2	. . . . . . 7 ⊢ B = ∪{x ∈ A∣∀y ∈ A ¬ yRx}
6		ax-17 925	. . . . . . . . . . . . . . . 16 ⊢ (φ → ∀yφ)
7		hba1 698	. . . . . . . . . . . . . . . 16 ⊢ (∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)) → ∀y∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))
8	6, 7	hban 704	. . . . . . . . . . . . . . 15 ⊢ ((φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y))) → ∀y(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y))))
9	8	hbab 1096	. . . . . . . . . . . . . 14 ⊢ (z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → ∀y z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
10	1	eleq2i 1153	. . . . . . . . . . . . . 14 ⊢ (z ∈ A ↔ z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
11	10	bial 695	. . . . . . . . . . . . . 14 ⊢ (∀y z ∈ A ↔ ∀y z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
12	9, 10, 11	3imtr4 192	. . . . . . . . . . . . 13 ⊢ (z ∈ A → ∀y z ∈ A)
13	12, 9	raleqf 1321	. . . . . . . . . . . 12 ⊢ (A = {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → (∀y ∈ A ¬ yRx ↔ ∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx))
14	1, 13	ax-mp 6	. . . . . . . . . . 11 ⊢ (∀y ∈ A ¬ yRx ↔ ∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx)
15	14	a1i 7	. . . . . . . . . 10 ⊢ (x ∈ A → (∀y ∈ A ¬ yRx ↔ ∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx))
16	15	birabi 1342	. . . . . . . . 9 ⊢ {x ∈ A∣∀y ∈ A ¬ yRx} = {x ∈ A∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx}
17		hbab1 1095	. . . . . . . . . . . 12 ⊢ (z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → ∀x z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
18	10	bial 695	. . . . . . . . . . . 12 ⊢ (∀x z ∈ A ↔ ∀x z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
19	17, 10, 18	3imtr4 192	. . . . . . . . . . 11 ⊢ (z ∈ A → ∀x z ∈ A)
20	19, 17	rabeqf 1345	. . . . . . . . . 10 ⊢ (A = {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → {x ∈ A∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx} = {x ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx})
21	1, 20	ax-mp 6	. . . . . . . . 9 ⊢ {x ∈ A∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx} = {x ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx}
22		hbab1 1095	. . . . . . . . . . 11 ⊢ (v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → ∀x v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
23		ax-17 925	. . . . . . . . . . 11 ⊢ (v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → ∀z v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
24		ax-17 925	. . . . . . . . . . 11 ⊢ (∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx → ∀z∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx)
25		hbab1 1095	. . . . . . . . . . . 12 ⊢ (y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → ∀x y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
26		ax-17 925	. . . . . . . . . . . 12 ⊢ (¬ yRz → ∀x ¬ yRz)
27	25, 26	hbral 1236	. . . . . . . . . . 11 ⊢ (∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRz → ∀x∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (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 → (∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx ↔ ∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRz))
31	22, 23, 24, 27, 30	cbvrab 1425	. . . . . . . . . 10 ⊢ {x ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx} = {z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRz}
32		ax-17 925	. . . . . . . . . . . . 13 ⊢ (z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → ∀v z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
33		ax-17 925	. . . . . . . . . . . . 13 ⊢ (¬ yRz → ∀v ¬ yRz)
34		ax-17 925	. . . . . . . . . . . . 13 ⊢ (¬ vRz → ∀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 ⊢ (∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRz ↔ ∀v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ vRz)
38	37	a1i 7	. . . . . . . . . . 11 ⊢ (z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → (∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRz ↔ ∀v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ vRz))
39	38	birabi 1342	. . . . . . . . . 10 ⊢ {z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRz} = {z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ vRz}
40	31, 39	eqtr 1119	. . . . . . . . 9 ⊢ {x ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀y ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ yRx} = {z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ vRz}
41	16, 21, 40	3eqtr 1123	. . . . . . . 8 ⊢ {x ∈ A∣∀y ∈ A ¬ yRx} = {z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ vRz}
42	41	unieqi 1928	. . . . . . 7 ⊢ ∪{x ∈ A∣∀y ∈ A ¬ yRx} = ∪{z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ vRz}
43	5, 42	eqtr 1119	. . . . . 6 ⊢ B = ∪{z ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}∣∀v ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ¬ vRz}
44	4, 43	htalem 3618	. . . . 5 ⊢ ((R We {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ∧ ¬ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} = ∅) → B ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))})
45	44	exp 291	. . . 4 ⊢ (R We {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → (¬ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} = ∅ → B ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}))
46	3, 45	sylbi 174	. . 3 ⊢ (R We A → (¬ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} = ∅ → B ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}))
47		pm3.26 256	. . . . . 6 ⊢ ((φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y))) → φ)
48	47	ss2abi 1552	. . . . 5 ⊢ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} ⊆ {x∣φ}
49	48	sseli 1504	. . . 4 ⊢ (B ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → B ∈ {x∣φ})
50	1, 4	eqeltr 1159	. . . . . . . 8 ⊢ A ∈ V
51		ax-17 925	. . . . . . . . . . 11 ⊢ (z ∈ v → ∀x z ∈ v)
52	51, 19	hbel 1172	. . . . . . . . . 10 ⊢ (v ∈ A → ∀x v ∈ A)
53		ax-17 925	. . . . . . . . . 10 ⊢ (v ∈ A → ∀z v ∈ A)
54		ax-17 925	. . . . . . . . . 10 ⊢ (∀y ∈ A ¬ yRx → ∀z∀y ∈ A ¬ yRx)
55		ax-17 925	. . . . . . . . . . . 12 ⊢ (z ∈ y → ∀x z ∈ y)
56	55, 19	hbel 1172	. . . . . . . . . . 11 ⊢ (y ∈ A → ∀x y ∈ A)
57	56, 26	hbral 1236	. . . . . . . . . 10 ⊢ (∀y ∈ A ¬ yRz → ∀x∀y ∈ A ¬ yRz)
58	29	biraldv 1219	. . . . . . . . . 10 ⊢ (x = z → (∀y ∈ A ¬ yRx ↔ ∀y ∈ A ¬ yRz))
59	52, 53, 54, 57, 58	cbvrab 1425	. . . . . . . . 9 ⊢ {x ∈ A∣∀y ∈ A ¬ yRx} = {z ∈ A∣∀y ∈ A ¬ yRz}
60		ssrab 1556	. . . . . . . . 9 ⊢ {z ∈ A∣∀y ∈ A ¬ yRz} ⊆ A
61	59, 60	eqsstr 1530	. . . . . . . 8 ⊢ {x ∈ A∣∀y ∈ A ¬ yRx} ⊆ A
62	50, 61	ssexi 1701	. . . . . . 7 ⊢ {x ∈ A∣∀y ∈ A ¬ yRx} ∈ V
63	62	uniex 1947	. . . . . 6 ⊢ ∪{x ∈ A∣∀y ∈ A ¬ yRx} ∈ V
64	5, 63	eqeltr 1159	. . . . 5 ⊢ B ∈ V
65	64	elabs 1458	. . . 4 ⊢ (B ∈ {x∣φ} ↔ [B / x]φ)
66	49, 65	sylib 173	. . 3 ⊢ (B ∈ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} → [B / x]φ)
67	46, 66	syl6 23	. 2 ⊢ (R We A → (¬ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} = ∅ → [B / x]φ))
68		19.8a 712	. . 3 ⊢ (φ → ∃xφ)
69		scott0s 3544	. . 3 ⊢ (∃xφ ↔ ¬ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} = ∅)
70	68, 69	sylib 173	. 2 ⊢ (φ → ¬ {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))} = ∅)
71	67, 70	syl5 22	1 ⊢ (R We A → (φ → [B / x]φ))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∀wal 672 ∃wex 678 = weq 797 ∈ wel 803 [wsb 852 {cab 1090 = wceq 1091 ∈ wcel 1092 ∀wral 1201 {crab 1204 Vcvv 1348 [wsbc 1440 ⊆ wss 1487 ∅c0 1707 ∪cuni 1919 class class class wbr 2054 We wwe 2062 ‘cfv 2422 rankcrnk 3486

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-iin 1997 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-r1 3487 df-rank 3488

metamath.org