Theorem axdc3 10439

Description: Dependent Choice. Axiom DC1 of [Schechter] p. 149, with the addition of an initial value 𝐶. This theorem is weaker than the Axiom of Choice but is stronger than Countable Choice. It shows the existence of a sequence whose values can only be shown to exist (but cannot be constructed explicitly) and also depend on earlier values in the sequence. (Contributed by Mario Carneiro, 27-Jan-2013.)

Hypothesis

Ref	Expression
axdc3.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
axdc3	⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Distinct variable groups:   𝐴,𝑔,𝑘   𝐶,𝑔,𝑘   𝑔,𝐹,𝑘

Proof of Theorem axdc3

Dummy variables 𝑛 𝑠 𝑡 𝑥 𝑦 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axdc3.1	. 2 ⊢ 𝐴 ∈ V
2		feq1 6685	. . . . 5 ⊢ (𝑡 = 𝑠 → (𝑡:suc 𝑛⟶𝐴 ↔ 𝑠:suc 𝑛⟶𝐴))
3		fveq1 6882	. . . . . 6 ⊢ (𝑡 = 𝑠 → (𝑡‘∅) = (𝑠‘∅))
4	3	eqeq1d 2765	. . . . 5 ⊢ (𝑡 = 𝑠 → ((𝑡‘∅) = 𝐶 ↔ (𝑠‘∅) = 𝐶))
5		fveq1 6882	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝑡‘suc 𝑗) = (𝑠‘suc 𝑗))
6		fveq1 6882	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (𝑡‘𝑗) = (𝑠‘𝑗))
7	6	fveq2d 6887	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝐹‘(𝑡‘𝑗)) = (𝐹‘(𝑠‘𝑗)))
8	5, 7	eleq12d 2857	. . . . . . 7 ⊢ (𝑡 = 𝑠 → ((𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)) ↔ (𝑠‘suc 𝑗) ∈ (𝐹‘(𝑠‘𝑗))))
9	8	ralbidv 3188	. . . . . 6 ⊢ (𝑡 = 𝑠 → (∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)) ↔ ∀𝑗 ∈ 𝑛 (𝑠‘suc 𝑗) ∈ (𝐹‘(𝑠‘𝑗))))
10		suceq 6431	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → suc 𝑗 = suc 𝑘)
11	10	fveq2d 6887	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝑠‘suc 𝑗) = (𝑠‘suc 𝑘))
12		2fveq3 6888	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (𝐹‘(𝑠‘𝑗)) = (𝐹‘(𝑠‘𝑘)))
13	11, 12	eleq12d 2857	. . . . . . 7 ⊢ (𝑗 = 𝑘 → ((𝑠‘suc 𝑗) ∈ (𝐹‘(𝑠‘𝑗)) ↔ (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
14	13	cbvralvw 3243	. . . . . 6 ⊢ (∀𝑗 ∈ 𝑛 (𝑠‘suc 𝑗) ∈ (𝐹‘(𝑠‘𝑗)) ↔ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))
15	9, 14	bitrdi 290	. . . . 5 ⊢ (𝑡 = 𝑠 → (∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)) ↔ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘))))
16	2, 4, 15	3anbi123d 1464	. . . 4 ⊢ (𝑡 = 𝑠 → ((𝑡:suc 𝑛⟶𝐴 ∧ (𝑡‘∅) = 𝐶 ∧ ∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗))) ↔ (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
17	16	rexbidv 3189	. . 3 ⊢ (𝑡 = 𝑠 → (∃𝑛 ∈ ω (𝑡:suc 𝑛⟶𝐴 ∧ (𝑡‘∅) = 𝐶 ∧ ∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗))) ↔ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))))
18	17	cbvabv 2833	. 2 ⊢ {𝑡 ∣ ∃𝑛 ∈ ω (𝑡:suc 𝑛⟶𝐴 ∧ (𝑡‘∅) = 𝐶 ∧ ∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)))} = {𝑠 ∣ ∃𝑛 ∈ ω (𝑠:suc 𝑛⟶𝐴 ∧ (𝑠‘∅) = 𝐶 ∧ ∀𝑘 ∈ 𝑛 (𝑠‘suc 𝑘) ∈ (𝐹‘(𝑠‘𝑘)))}
19		eqid 2763	. 2 ⊢ (𝑥 ∈ {𝑡 ∣ ∃𝑛 ∈ ω (𝑡:suc 𝑛⟶𝐴 ∧ (𝑡‘∅) = 𝐶 ∧ ∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)))} ↦ {𝑦 ∈ {𝑡 ∣ ∃𝑛 ∈ ω (𝑡:suc 𝑛⟶𝐴 ∧ (𝑡‘∅) = 𝐶 ∧ ∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)))} ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)}) = (𝑥 ∈ {𝑡 ∣ ∃𝑛 ∈ ω (𝑡:suc 𝑛⟶𝐴 ∧ (𝑡‘∅) = 𝐶 ∧ ∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)))} ↦ {𝑦 ∈ {𝑡 ∣ ∃𝑛 ∈ ω (𝑡:suc 𝑛⟶𝐴 ∧ (𝑡‘∅) = 𝐶 ∧ ∀𝑗 ∈ 𝑛 (𝑡‘suc 𝑗) ∈ (𝐹‘(𝑡‘𝑗)))} ∣ (dom 𝑦 = suc dom 𝑥 ∧ (𝑦 ↾ dom 𝑥) = 𝑥)})
20	1, 18, 19	axdc3lem4 10438	1 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ (𝑔‘∅) = 𝐶 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570  ∃wex 1809   ∈ wcel 2143  {cab 2741  ∀wral 3079  ∃wrex 3089  {crab 3416  Vcvv 3455   ∖ cdif 3903  ∅c0 4287  𝒫 cpw 4563  {csn 4590   ↦ cmpt 5193  dom cdm 5663   ↾ cres 5665  suc csuc 6364  ⟶wf 6534  ‘cfv 6538  ωcom 7863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-dc 10431

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-om 7864  df-1o 8454

This theorem is referenced by:  axdc4lem  10440