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 e. _V
	axdc3lem.2	|- S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
Assertion	axdc3lem	|- S e. _V

Proof

Step	Hyp	Ref	Expression
1		axdc3lem.1	|- A e. _V
2		axdc3lem.2	|- S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
3		dcomex	|- _om e. _V
4	3 1	xpex	|- ( _om X. A ) e. _V
5	4	pwex	|- ~P ( _om X. A ) e. _V
6		fssxp	|- ( s : suc n --> A -> s C_ ( suc n X. A ) )
7		peano2	|- ( n e. _om -> suc n e. _om )
8		omelon2	|- ( _om e. _V -> _om e. On )
9	3 8	ax-mp	|- _om e. On
10	9	onelssi	|- ( suc n e. _om -> suc n C_ _om )
11		xpss1	|- ( suc n C_ _om -> ( suc n X. A ) C_ ( _om X. A ) )
12	7 10 11	3syl	|- ( n e. _om -> ( suc n X. A ) C_ ( _om X. A ) )
13	6 12	sylan9ss	|- ( ( s : suc n --> A /\ n e. _om ) -> s C_ ( _om X. A ) )
14		velpw	|- ( s e. ~P ( _om X. A ) <-> s C_ ( _om X. A ) )
15	13 14	sylibr	|- ( ( s : suc n --> A /\ n e. _om ) -> s e. ~P ( _om X. A ) )
16	15	ancoms	|- ( ( n e. _om /\ s : suc n --> A ) -> s e. ~P ( _om X. A ) )
17	16	3ad2antr1	|- ( ( n e. _om /\ ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) -> s e. ~P ( _om X. A ) )
18	17	rexlimiva	|- ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> s e. ~P ( _om X. A ) )
19	18	abssi	|- { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ ~P ( _om X. A )
20	2 19	eqsstri	|- S C_ ~P ( _om X. A )
21	5 20	ssexi	|- S e. _V