Metamath Proof Explorer

Theorem axdc3lem

Description: The class S of finite approximations to the DC sequence is a set. (We derive here the stronger statement that S is a subset of a specific set, namely ~P ( _om X. A ) .) (Contributed by Mario Carneiro, 27-Jan-2013) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 18-Mar-2014)

Ref Expression
Hypotheses axdc3lem.1 ⊢A∈V
axdc3lem.2 ⊢S=s|∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k
Assertion axdc3lem ⊢S∈V

Proof

Step Hyp Ref Expression
1 axdc3lem.1 ⊢A∈V
2 axdc3lem.2 ⊢S=s|∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k
3 dcomex ⊢ω∈V
4 3 1 xpex ⊢ω×A∈V
5 4 pwex ⊢𝒫ω×A∈V
6 fssxp ⊢s:suc⁡n⟶A→s⊆suc⁡n×A
7 peano2 ⊢n∈ω→suc⁡n∈ω
8 omelon2 ⊢ω∈V→ω∈On
9 3 8 ax-mp ⊢ω∈On
10 9 onelssi ⊢suc⁡n∈ω→suc⁡n⊆ω
11 xpss1 ⊢suc⁡n⊆ω→suc⁡n×A⊆ω×A
12 7 10 11 3syl ⊢n∈ω→suc⁡n×A⊆ω×A
13 6 12 sylan9ss ⊢s:suc⁡n⟶A∧n∈ω→s⊆ω×A
14 velpw ⊢s∈𝒫ω×A↔s⊆ω×A
15 13 14 sylibr ⊢s:suc⁡n⟶A∧n∈ω→s∈𝒫ω×A
16 15 ancoms ⊢n∈ω∧s:suc⁡n⟶A→s∈𝒫ω×A
17 16 3ad2antr1 ⊢n∈ω∧s:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k→s∈𝒫ω×A
18 17 rexlimiva ⊢∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k→s∈𝒫ω×A
19 18 abssi ⊢s|∃n∈ωs:suc⁡n⟶A∧s⁡∅=C∧∀k∈ns⁡suc⁡k∈F⁡s⁡k⊆𝒫ω×A
20 2 19 eqsstri ⊢S⊆𝒫ω×A
21 5 20 ssexi ⊢S∈V