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 to construct infinite sequences 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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	sdc.2	⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) → ( 𝜓 ↔ 𝜒 ) )
	sdc.3	⊢ ( 𝑛 = 𝑀 → ( 𝜓 ↔ 𝜏 ) )
	sdc.4	⊢ ( 𝑛 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
	sdc.5	⊢ ( ( 𝑔 = ℎ ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝜓 ↔ 𝜎 ) )
	sdc.6	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sdc.7	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	sdc.8	⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
	sdc.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
Assertion	sdc	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sdc.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		sdc.2	⊢ ( 𝑔 = ( 𝑓 ↾ ( 𝑀 ... 𝑛 ) ) → ( 𝜓 ↔ 𝜒 ) )
3		sdc.3	⊢ ( 𝑛 = 𝑀 → ( 𝜓 ↔ 𝜏 ) )
4		sdc.4	⊢ ( 𝑛 = 𝑘 → ( 𝜓 ↔ 𝜃 ) )
5		sdc.5	⊢ ( ( 𝑔 = ℎ ∧ 𝑛 = ( 𝑘 + 1 ) ) → ( 𝜓 ↔ 𝜎 ) )
6		sdc.6	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7		sdc.7	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8		sdc.8	⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑀 } ⟶ 𝐴 ∧ 𝜏 ) )
9		sdc.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) → ∃ ℎ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑔 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
10		eqid	⊢ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } = { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) }
11		eqid	⊢ 𝑍 = 𝑍
12		oveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑘 ) )
13	12	feq2d	⊢ ( 𝑛 = 𝑘 → ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ↔ 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ) )
14	13 4	anbi12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) ) )
15	14	cbvrexvw	⊢ ( ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) )
16	15	abbii	⊢ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } = { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) }
17		eqid	⊢ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) }
18	11 16 17	mpoeq123i	⊢ ( 𝑗 ∈ 𝑍 , 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) = ( 𝑗 ∈ 𝑍 , 𝑓 ∈ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
19		eqidd	⊢ ( 𝑗 = 𝑦 → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
20		eqeq1	⊢ ( 𝑓 = 𝑥 → ( 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ↔ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ) )
21	20	3anbi2d	⊢ ( 𝑓 = 𝑥 → ( ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
22	21	rexbidv	⊢ ( 𝑓 = 𝑥 → ( ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ↔ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) ) )
23	22	abbidv	⊢ ( 𝑓 = 𝑥 → { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } = { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
24	19 23	cbvmpov	⊢ ( 𝑗 ∈ 𝑍 , 𝑓 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) = ( 𝑦 ∈ 𝑍 , 𝑥 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
25	18 24	eqtr3i	⊢ ( 𝑗 ∈ 𝑍 , 𝑓 ∈ { 𝑔 ∣ ∃ 𝑘 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑘 ) ⟶ 𝐴 ∧ 𝜃 ) } ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑓 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } ) = ( 𝑦 ∈ 𝑍 , 𝑥 ∈ { 𝑔 ∣ ∃ 𝑛 ∈ 𝑍 ( 𝑔 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ 𝜓 ) } ↦ { ℎ ∣ ∃ 𝑘 ∈ 𝑍 ( ℎ : ( 𝑀 ... ( 𝑘 + 1 ) ) ⟶ 𝐴 ∧ 𝑥 = ( ℎ ↾ ( 𝑀 ... 𝑘 ) ) ∧ 𝜎 ) } )
26	1 2 3 4 5 6 7 8 9 10 25	sdclem1	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑍 ⟶ 𝐴 ∧ ∀ 𝑛 ∈ 𝑍 𝜒 ) )