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

Metamath Proof Explorer

Theorem axdc3lem

Proof