Theorem htalem

Description: Lemma for defining an emulation of Hilbert's epsilon. Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/ . This theorem is equivalent to Hilbert's "transfinite axiom", described on that page, with the additional R We A antecedent. The element B is the epsilon that the theorem emulates. (Contributed by NM, 11-Mar-2004) (Revised by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Hypotheses	htalem.1	$$⊢A\in \mathrm{V}$$
	htalem.2	$$⊢B=\left(\iota x\in A|\forall y\in A\neg yRx\right)$$
Assertion	htalem	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to B\in A$$

Proof

Step	Hyp	Ref	Expression
1		htalem.1	$$⊢A\in \mathrm{V}$$
2		htalem.2	$$⊢B=\left(\iota x\in A|\forall y\in A\neg yRx\right)$$
3		simpl	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to R\mathrm{We}A$$
4	1	a1i	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to A\in \mathrm{V}$$
5		ssidd	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to A\subseteq A$$
6		simpr	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to A\ne \varnothing$$
7		wereu	$$⊢\left(R\mathrm{We}A\wedge \left(A\in \mathrm{V}\wedge A\subseteq A\wedge A\ne \varnothing \right)\right)\to \exists !x\in A\forall y\in A\neg yRx$$
8	3 4 5 6 7	syl13anc	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to \exists !x\in A\forall y\in A\neg yRx$$
9		riotacl	$$⊢\exists !x\in A\forall y\in A\neg yRx\to \left(\iota x\in A|\forall y\in A\neg yRx\right)\in A$$
10	8 9	syl	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to \left(\iota x\in A|\forall y\in A\neg yRx\right)\in A$$
11	2 10	eqeltrid	$$⊢\left(R\mathrm{We}A\wedge A\ne \varnothing \right)\to B\in A$$