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 ⊢ 𝐴 ∈ 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 𝐴 ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ 𝐴 )