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	⊢ 𝐴 ∈ V
	axdc3lem.2	⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
Assertion	axdc3lem	⊢ 𝑆 ∈ V

Proof

Step	Hyp	Ref	Expression
1		axdc3lem.1	⊢ 𝐴 ∈ V
2		axdc3lem.2	⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) }
3		dcomex	⊢ ω ∈ V
4	3 1	xpex	⊢ ( ω × 𝐴 ) ∈ V
5	4	pwex	⊢ 𝒫 ( ω × 𝐴 ) ∈ V
6		fssxp	⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → 𝑠 ⊆ ( suc 𝑛 × 𝐴 ) )
7		peano2	⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
8		omelon2	⊢ ( ω ∈ V → ω ∈ On )
9	3 8	ax-mp	⊢ ω ∈ On
10	9	onelssi	⊢ ( suc 𝑛 ∈ ω → suc 𝑛 ⊆ ω )
11		xpss1	⊢ ( suc 𝑛 ⊆ ω → ( suc 𝑛 × 𝐴 ) ⊆ ( ω × 𝐴 ) )
12	7 10 11	3syl	⊢ ( 𝑛 ∈ ω → ( suc 𝑛 × 𝐴 ) ⊆ ( ω × 𝐴 ) )
13	6 12	sylan9ss	⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ 𝑛 ∈ ω ) → 𝑠 ⊆ ( ω × 𝐴 ) )
14		velpw	⊢ ( 𝑠 ∈ 𝒫 ( ω × 𝐴 ) ↔ 𝑠 ⊆ ( ω × 𝐴 ) )
15	13 14	sylibr	⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ 𝑛 ∈ ω ) → 𝑠 ∈ 𝒫 ( ω × 𝐴 ) )
16	15	ancoms	⊢ ( ( 𝑛 ∈ ω ∧ 𝑠 : suc 𝑛 ⟶ 𝐴 ) → 𝑠 ∈ 𝒫 ( ω × 𝐴 ) )
17	16	3ad2antr1	⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) → 𝑠 ∈ 𝒫 ( ω × 𝐴 ) )
18	17	rexlimiva	⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → 𝑠 ∈ 𝒫 ( ω × 𝐴 ) )
19	18	abssi	⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ 𝒫 ( ω × 𝐴 )
20	2 19	eqsstri	⊢ 𝑆 ⊆ 𝒫 ( ω × 𝐴 )
21	5 20	ssexi	⊢ 𝑆 ∈ V