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	⊢ 𝐴 ∈ V
	htalem.2	⊢ 𝐵 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
Assertion	htalem	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		htalem.1	⊢ 𝐴 ∈ V
2		htalem.2	⊢ 𝐵 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
3		simpl	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝑅 We 𝐴 )
4	1	a1i	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ V )
5		ssidd	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ 𝐴 )
6		simpr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
7		wereu	⊢ ( ( 𝑅 We 𝐴 ∧ ( 𝐴 ∈ V ∧ 𝐴 ⊆ 𝐴 ∧ 𝐴 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
8	3 4 5 6 7	syl13anc	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
9		riotacl	⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) ∈ 𝐴 )
10	8 9	syl	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) ∈ 𝐴 )
11	2 10	eqeltrid	⊢ ( ( 𝑅 We 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ 𝐴 )