# 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}\in \mathrm{V}$
axdc3lem.2 ${⊢}{S}=\left\{{s}|\exists {n}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({s}:\mathrm{suc}{n}⟶{A}\wedge {s}\left(\varnothing \right)={C}\wedge \forall {k}\in {n}\phantom{\rule{.4em}{0ex}}{s}\left(\mathrm{suc}{k}\right)\in {F}\left({s}\left({k}\right)\right)\right)\right\}$
Assertion axdc3lem ${⊢}{S}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 axdc3lem.1 ${⊢}{A}\in \mathrm{V}$
2 axdc3lem.2 ${⊢}{S}=\left\{{s}|\exists {n}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({s}:\mathrm{suc}{n}⟶{A}\wedge {s}\left(\varnothing \right)={C}\wedge \forall {k}\in {n}\phantom{\rule{.4em}{0ex}}{s}\left(\mathrm{suc}{k}\right)\in {F}\left({s}\left({k}\right)\right)\right)\right\}$
3 dcomex ${⊢}\mathrm{\omega }\in \mathrm{V}$
4 3 1 xpex ${⊢}\mathrm{\omega }×{A}\in \mathrm{V}$
5 4 pwex ${⊢}𝒫\left(\mathrm{\omega }×{A}\right)\in \mathrm{V}$
6 fssxp ${⊢}{s}:\mathrm{suc}{n}⟶{A}\to {s}\subseteq \mathrm{suc}{n}×{A}$
7 peano2 ${⊢}{n}\in \mathrm{\omega }\to \mathrm{suc}{n}\in \mathrm{\omega }$
8 omelon2 ${⊢}\mathrm{\omega }\in \mathrm{V}\to \mathrm{\omega }\in \mathrm{On}$
9 3 8 ax-mp ${⊢}\mathrm{\omega }\in \mathrm{On}$
10 9 onelssi ${⊢}\mathrm{suc}{n}\in \mathrm{\omega }\to \mathrm{suc}{n}\subseteq \mathrm{\omega }$
11 xpss1 ${⊢}\mathrm{suc}{n}\subseteq \mathrm{\omega }\to \mathrm{suc}{n}×{A}\subseteq \mathrm{\omega }×{A}$
12 7 10 11 3syl ${⊢}{n}\in \mathrm{\omega }\to \mathrm{suc}{n}×{A}\subseteq \mathrm{\omega }×{A}$
13 6 12 sylan9ss ${⊢}\left({s}:\mathrm{suc}{n}⟶{A}\wedge {n}\in \mathrm{\omega }\right)\to {s}\subseteq \mathrm{\omega }×{A}$
14 velpw ${⊢}{s}\in 𝒫\left(\mathrm{\omega }×{A}\right)↔{s}\subseteq \mathrm{\omega }×{A}$
15 13 14 sylibr ${⊢}\left({s}:\mathrm{suc}{n}⟶{A}\wedge {n}\in \mathrm{\omega }\right)\to {s}\in 𝒫\left(\mathrm{\omega }×{A}\right)$
16 15 ancoms ${⊢}\left({n}\in \mathrm{\omega }\wedge {s}:\mathrm{suc}{n}⟶{A}\right)\to {s}\in 𝒫\left(\mathrm{\omega }×{A}\right)$
17 16 3ad2antr1 ${⊢}\left({n}\in \mathrm{\omega }\wedge \left({s}:\mathrm{suc}{n}⟶{A}\wedge {s}\left(\varnothing \right)={C}\wedge \forall {k}\in {n}\phantom{\rule{.4em}{0ex}}{s}\left(\mathrm{suc}{k}\right)\in {F}\left({s}\left({k}\right)\right)\right)\right)\to {s}\in 𝒫\left(\mathrm{\omega }×{A}\right)$
18 17 rexlimiva ${⊢}\exists {n}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({s}:\mathrm{suc}{n}⟶{A}\wedge {s}\left(\varnothing \right)={C}\wedge \forall {k}\in {n}\phantom{\rule{.4em}{0ex}}{s}\left(\mathrm{suc}{k}\right)\in {F}\left({s}\left({k}\right)\right)\right)\to {s}\in 𝒫\left(\mathrm{\omega }×{A}\right)$
19 18 abssi ${⊢}\left\{{s}|\exists {n}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({s}:\mathrm{suc}{n}⟶{A}\wedge {s}\left(\varnothing \right)={C}\wedge \forall {k}\in {n}\phantom{\rule{.4em}{0ex}}{s}\left(\mathrm{suc}{k}\right)\in {F}\left({s}\left({k}\right)\right)\right)\right\}\subseteq 𝒫\left(\mathrm{\omega }×{A}\right)$
20 2 19 eqsstri ${⊢}{S}\subseteq 𝒫\left(\mathrm{\omega }×{A}\right)$
21 5 20 ssexi ${⊢}{S}\in \mathrm{V}$