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 e. _V
	htalem.2	|- B = ( iota_ x e. A A. y e. A -. y R x )
Assertion	htalem	|- ( ( R We A /\ A =/= (/) ) -> B e. A )

Proof

Step	Hyp	Ref	Expression
1		htalem.1	|- A e. _V
2		htalem.2	|- B = ( iota_ x e. A A. y e. A -. y R x )
3		simpl	|- ( ( R We A /\ A =/= (/) ) -> R We A )
4	1	a1i	|- ( ( R We A /\ A =/= (/) ) -> A e. _V )
5		ssidd	|- ( ( R We A /\ A =/= (/) ) -> A C_ A )
6		simpr	|- ( ( R We A /\ A =/= (/) ) -> A =/= (/) )
7		wereu	|- ( ( R We A /\ ( A e. _V /\ A C_ A /\ A =/= (/) ) ) -> E! x e. A A. y e. A -. y R x )
8	3 4 5 6 7	syl13anc	|- ( ( R We A /\ A =/= (/) ) -> E! x e. A A. y e. A -. y R x )
9		riotacl	|- ( E! x e. A A. y e. A -. y R x -> ( iota_ x e. A A. y e. A -. y R x ) e. A )
10	8 9	syl	|- ( ( R We A /\ A =/= (/) ) -> ( iota_ x e. A A. y e. A -. y R x ) e. A )
11	2 10	eqeltrid	|- ( ( R We A /\ A =/= (/) ) -> B e. A )