Theorem sdc

Description: Strong dependent choice. Suppose we may choose an element of A such that property ps holds, and suppose that if we have already chosen the first k elements (represented here by a function from 1 ... k to A ), we may choose another element so that all k + 1 elements taken together have property ps . Then there exists an infinite sequence of elements of A such that the first n terms of this sequence satisfy ps for all n . This theorem allows us to construct infinite seqeunces where each term depends on all the previous terms in the sequence. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 3-Jun-2014)

	Ref	Expression
Hypotheses	sdc.1	|- Z = ( ZZ>= ` M )
	sdc.2	|- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )
	sdc.3	|- ( n = M -> ( ps <-> ta ) )
	sdc.4	|- ( n = k -> ( ps <-> th ) )
	sdc.5	|- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )
	sdc.6	|- ( ph -> A e. V )
	sdc.7	|- ( ph -> M e. ZZ )
	sdc.8	|- ( ph -> E. g ( g : { M } --> A /\ ta ) )
	sdc.9	|- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
Assertion	sdc	|- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )

Proof

Step	Hyp	Ref	Expression
1		sdc.1	|- Z = ( ZZ>= ` M )
2		sdc.2	|- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )
3		sdc.3	|- ( n = M -> ( ps <-> ta ) )
4		sdc.4	|- ( n = k -> ( ps <-> th ) )
5		sdc.5	|- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )
6		sdc.6	|- ( ph -> A e. V )
7		sdc.7	|- ( ph -> M e. ZZ )
8		sdc.8	|- ( ph -> E. g ( g : { M } --> A /\ ta ) )
9		sdc.9	|- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
10		eqid	|- { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } = { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) }
11		eqid	|- Z = Z
12		oveq2	|- ( n = k -> ( M ... n ) = ( M ... k ) )
13	12	feq2d	|- ( n = k -> ( g : ( M ... n ) --> A <-> g : ( M ... k ) --> A ) )
14	13 4	anbi12d	|- ( n = k -> ( ( g : ( M ... n ) --> A /\ ps ) <-> ( g : ( M ... k ) --> A /\ th ) ) )
15	14	cbvrexvw	|- ( E. n e. Z ( g : ( M ... n ) --> A /\ ps ) <-> E. k e. Z ( g : ( M ... k ) --> A /\ th ) )
16	15	abbii	|- { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } = { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) }
17		eqid	|- { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) }
18	11 16 17	mpoeq123i	|- ( j e. Z , f e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } ) = ( j e. Z , f e. { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } )
19		eqidd	|- ( j = y -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } )
20		eqeq1	|- ( f = x -> ( f = ( h |` ( M ... k ) ) <-> x = ( h |` ( M ... k ) ) ) )
21	20	3anbi2d	|- ( f = x -> ( ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) <-> ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) )
22	21	rexbidv	|- ( f = x -> ( E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) <-> E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) ) )
23	22	abbidv	|- ( f = x -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
24	19 23	cbvmpov	|- ( j e. Z , f e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } ) = ( y e. Z , x e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
25	18 24	eqtr3i	|- ( j e. Z , f e. { g | E. k e. Z ( g : ( M ... k ) --> A /\ th ) } |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ f = ( h |` ( M ... k ) ) /\ si ) } ) = ( y e. Z , x e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
26	1 2 3 4 5 6 7 8 9 10 25	sdclem1	|- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )