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	$⊢ Z = ℤ_{\geq M}$
	sdc.2	$⊢ g = {f ↾}_{(M \dots n)} \to (ψ \leftrightarrow χ)$
	sdc.3	$⊢ n = M \to (ψ \leftrightarrow τ)$
	sdc.4	$⊢ n = k \to (ψ \leftrightarrow θ)$
	sdc.5	$⊢ (g = h \land n = k + 1) \to (ψ \leftrightarrow σ)$
	sdc.6	$⊢ φ \to A \in V$
	sdc.7	$⊢ φ \to M \in ℤ$
	sdc.8	$⊢ φ \to \exists g (g : \{M\} ⟶ A \land τ)$
	sdc.9	$⊢ (φ \land k \in Z) \to ((g : (M \dots k) ⟶ A \land θ) \to \exists h (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ))$
Assertion	sdc	$⊢ φ \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$

Proof

Step	Hyp	Ref	Expression
1		sdc.1	$⊢ Z = ℤ_{\geq M}$
2		sdc.2	$⊢ g = {f ↾}_{(M \dots n)} \to (ψ \leftrightarrow χ)$
3		sdc.3	$⊢ n = M \to (ψ \leftrightarrow τ)$
4		sdc.4	$⊢ n = k \to (ψ \leftrightarrow θ)$
5		sdc.5	$⊢ (g = h \land n = k + 1) \to (ψ \leftrightarrow σ)$
6		sdc.6	$⊢ φ \to A \in V$
7		sdc.7	$⊢ φ \to M \in ℤ$
8		sdc.8	$⊢ φ \to \exists g (g : \{M\} ⟶ A \land τ)$
9		sdc.9	$⊢ (φ \land k \in Z) \to ((g : (M \dots k) ⟶ A \land θ) \to \exists h (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ))$
10		eqid	$⊢ \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} = \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\}$
11		eqid	$⊢ Z = Z$
12		oveq2	$⊢ n = k \to (M \dots n) = (M \dots k)$
13	12	feq2d	$⊢ n = k \to (g : (M \dots n) ⟶ A \leftrightarrow g : (M \dots k) ⟶ A)$
14	13 4	anbi12d	$⊢ n = k \to ((g : (M \dots n) ⟶ A \land ψ) \leftrightarrow (g : (M \dots k) ⟶ A \land θ))$
15	14	cbvrexvw	$⊢ \exists n \in Z (g : (M \dots n) ⟶ A \land ψ) \leftrightarrow \exists k \in Z (g : (M \dots k) ⟶ A \land θ)$
16	15	abbii	$⊢ \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} = \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\}$
17		eqid	$⊢ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\} = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\}$
18	11 16 17	mpoeq123i	$⊢ (j \in Z, f \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\}) = (j \in Z, f \in \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\})$
19		eqidd	$⊢ j = y \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\} = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\}$
20		eqeq1	$⊢ f = x \to (f = {h ↾}_{(M \dots k)} \leftrightarrow x = {h ↾}_{(M \dots k)})$
21	20	3anbi2d	$⊢ f = x \to ((h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ))$
22	21	rexbidv	$⊢ f = x \to (\exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ))$
23	22	abbidv	$⊢ f = x \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\} = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\}$
24	19 23	cbvmpov	$⊢ (j \in Z, f \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\}) = (y \in Z, x \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\})$
25	18 24	eqtr3i	$⊢ (j \in Z, f \in \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land f = {h ↾}_{(M \dots k)} \land σ)\}) = (y \in Z, x \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\})$
26	1 2 3 4 5 6 7 8 9 10 25	sdclem1	$⊢ φ \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$

Metamath Proof Explorer

Theorem sdc

Proof