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 ∈ n s ⁡ 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 ∈ n s ⁡ 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 ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k → s ∈ 𝒫 ω × A
18 17 rexlimiva ⊢ ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k → s ∈ 𝒫 ω × A
19 18 abssi ⊢ s | ∃ n ∈ ω s : suc ⁡ n ⟶ A ∧ s ⁡ ∅ = C ∧ ∀ k ∈ n s ⁡ suc ⁡ k ∈ F ⁡ s ⁡ k ⊆ 𝒫 ω × A
20 2 19 eqsstri ⊢ S ⊆ 𝒫 ω × A
21 5 20 ssexi ⊢ S ∈ V