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 V$
	htalem.2	$⊢ B = (ι x \in A \| \forall y \in A \neg y R x)$
Assertion	htalem	$⊢ (R We A \land A \neq \emptyset) \to B \in A$

Proof

Step	Hyp	Ref	Expression
1		htalem.1	$⊢ A \in V$
2		htalem.2	$⊢ B = (ι x \in A \| \forall y \in A \neg y R x)$
3		simpl	$⊢ (R We A \land A \neq \emptyset) \to R We A$
4	1	a1i	$⊢ (R We A \land A \neq \emptyset) \to A \in V$
5		ssidd	$⊢ (R We A \land A \neq \emptyset) \to A \subseteq A$
6		simpr	$⊢ (R We A \land A \neq \emptyset) \to A \neq \emptyset$
7		wereu	$⊢ (R We A \land (A \in V \land A \subseteq A \land A \neq \emptyset)) \to \exists! x \in A \forall y \in A \neg y R x$
8	3 4 5 6 7	syl13anc	$⊢ (R We A \land A \neq \emptyset) \to \exists! x \in A \forall y \in A \neg y R x$
9		riotacl	$⊢ \exists! x \in A \forall y \in A \neg y R x \to (ι x \in A \| \forall y \in A \neg y R x) \in A$
10	8 9	syl	$⊢ (R We A \land A \neq \emptyset) \to (ι x \in A \| \forall y \in A \neg y R x) \in A$
11	2 10	eqeltrid	$⊢ (R We A \land A \neq \emptyset) \to B \in A$

Metamath Proof Explorer

Theorem htalem

Proof