Theorem acdc 7437

Description: Dependent Choice. Axiom DC1 of [Schechter] p. 149. 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.

Hypothesis

Ref	Expression
acdc.1	|- A e. V

Assertion

Ref	Expression
acdc	|- ((A =/= (/) /\ F:A-->(P~A \ {(/)})) -> E.g(g:NN-->A /\ A.k e. NN (g` (k + 1)) e. (F` (g` k))))

Distinct variable groups:   g,k,A   g,F,k

Proof of Theorem acdc

Step	Hyp	Ref	Expression
1		acdc.1	. . 3 |- A e. V
2	1	weth 4759	. 2 |- E.r r We A
3		eleq1 1526	. . . . . . . . . . . . 13 |- (a = x -> (a e. A <-> x e. A))
4		eleq1 1526	. . . . . . . . . . . . 13 |- (b = y -> (b e. A <-> y e. A))
5	3, 4	bi2anan9 630	. . . . . . . . . . . 12 |- ((a = x /\ b = y) -> ((a e. A /\ b e. A) <-> (x e. A /\ y e. A)))
6		fveq2 3709	. . . . . . . . . . . . . . . . 17 |- (a = x -> (F` a) = (F` x))
7		rabeq 1800	. . . . . . . . . . . . . . . . . 18 |- ((F` a) = (F` x) -> {f e. (F` a) | A.h e. (F` a) -. hrf} = {f e. (F` x) | A.h e. (F` a) -. hrf})
8		raleq1 1778	. . . . . . . . . . . . . . . . . . 19 |- ((F` a) = (F` x) -> (A.h e. (F` a) -. hrf <-> A.h e. (F` x) -. hrf))
9	8	rabbisdv 1798	. . . . . . . . . . . . . . . . . 18 |- ((F` a) = (F` x) -> {f e. (F` x) | A.h e. (F` a) -. hrf} = {f e. (F` x) | A.h e. (F` x) -. hrf})
10	7, 9	eqtrd 1499	. . . . . . . . . . . . . . . . 17 |- ((F` a) = (F` x) -> {f e. (F` a) | A.h e. (F` a) -. hrf} = {f e. (F` x) | A.h e. (F` x) -. hrf})
11	6, 10	syl 10	. . . . . . . . . . . . . . . 16 |- (a = x -> {f e. (F` a) | A.h e. (F` a) -. hrf} = {f e. (F` x) | A.h e. (F` x) -. hrf})
12	11	adantr 389	. . . . . . . . . . . . . . 15 |- ((a = x /\ b = y) -> {f e. (F` a) | A.h e. (F` a) -. hrf} = {f e. (F` x) | A.h e. (F` x) -. hrf})
13		breq2 2613	. . . . . . . . . . . . . . . . . . 19 |- (f = v -> (hrf <-> hrv))
14	13	negbid 609	. . . . . . . . . . . . . . . . . 18 |- (f = v -> (-. hrf <-> -. hrv))
15	14	ralbidv 1655	. . . . . . . . . . . . . . . . 17 |- (f = v -> (A.h e. (F` x) -. hrf <-> A.h e. (F` x) -. hrv))
16		breq1 2612	. . . . . . . . . . . . . . . . . . 19 |- (h = u -> (hrv <-> urv))
17	16	negbid 609	. . . . . . . . . . . . . . . . . 18 |- (h = u -> (-. hrv <-> -. urv))
18	17	cbvralv 1791	. . . . . . . . . . . . . . . . 17 |- (A.h e. (F` x) -. hrv <-> A.u e. (F` x) -. urv)
19	15, 18	syl6bb 534	. . . . . . . . . . . . . . . 16 |- (f = v -> (A.h e. (F` x) -. hrf <-> A.u e. (F` x) -. urv))
20	19	cbvrabv 1902	. . . . . . . . . . . . . . 15 |- {f e. (F` x) | A.h e. (F` x) -. hrf} = {v e. (F` x) | A.u e. (F` x) -. urv}
21	12, 20	syl6eq 1515	. . . . . . . . . . . . . 14 |- ((a = x /\ b = y) -> {f e. (F` a) | A.h e. (F` a) -. hrf} = {v e. (F` x) | A.u e. (F` x) -. urv})
22	21	unieqd 2502	. . . . . . . . . . . . 13 |- ((a = x /\ b = y) -> U.{f e. (F` a) | A.h e. (F` a) -. hrf} = U.{v e. (F` x) | A.u e. (F` x) -. urv})
23	22	eqeq2d 1478	. . . . . . . . . . . 12 |- ((a = x /\ b = y) -> (d = U.{f e. (F` a) | A.h e. (F` a) -. hrf} <-> d = U.{v e. (F` x) | A.u e. (F` x) -. urv}))
24	5, 23	anbi12d 626	. . . . . . . . . . 11 |- ((a = x /\ b = y) -> (((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf}) <-> ((x e. A /\ y e. A) /\ d = U.{v e. (F` x) | A.u e. (F` x) -. urv})))
25	24	cbvoprab12v 3984	. . . . . . . . . 10 |- {<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} = {<.<.x, y>., d>. | ((x e. A /\ y e. A) /\ d = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
26		eqeq1 1473	. . . . . . . . . . . 12 |- (d = z -> (d = U.{v e. (F` x) | A.u e. (F` x) -. urv} <-> z = U.{v e. (F` x) | A.u e. (F` x) -. urv}))
27	26	anbi2d 614	. . . . . . . . . . 11 |- (d = z -> (((x e. A /\ y e. A) /\ d = U.{v e. (F` x) | A.u e. (F` x) -. urv}) <-> ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})))
28	27	cbvoprab3v 3985	. . . . . . . . . 10 |- {<.<.x, y>., d>. | ((x e. A /\ y e. A) /\ d = U.{v e. (F` x) | A.u e. (F` x) -. urv})} = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
29	25, 28	eqtr 1487	. . . . . . . . 9 |- {<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
30		eqid 1468	. . . . . . . . 9 |- ({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c})) = ({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c}))
31	1, 29, 30	acdclem 7436	. . . . . . . 8 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c})):NN-->A /\ A.k e. NN (({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c}))` (k + 1)) e. (F` (({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c}))` k))))
32		oprex 3968	. . . . . . . . 9 |- ({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c})) e. V
33		feq1 3606	. . . . . . . . . 10 |- (g = ({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c})) -> (g:NN-->A <-> ({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c})):NN-->A))
34		fveq1 3708	. . . . . . . . . . . 12 |- (g = ({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c})) -> (g` (k + 1)) = (({<.<.a, b>., d>. | ((a e. A /\ b e. A) /\ d = U.{f e. (F` a) | A.h e. (F` a) -. hrf})} seq1 (NN X. {c}