This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )