Theorem acdc 7495

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 4787	. 2 |- E.r r We A
3		eleq1 1534	. . . . . . . . . . . . 13 |- (a = x -> (a e. A <-> x e. A))
4		eleq1 1534	. . . . . . . . . . . . 13 |- (b = y -> (b e. A <-> y e. A))
5	3, 4	bi2anan9 632	. . . . . . . . . . . 12 |- ((a = x /\ b = y) -> ((a e. A /\ b e. A) <-> (x e. A /\ y e. A)))
6		fveq2 3724	. . . . . . . . . . . . . . . . 17 |- (a = x -> (F` a) = (F` x))
7		rabeq 1809	. . . . . . . . . . . . . . . . . 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 1786	. . . . . . . . . . . . . . . . . . 19 |- ((F` a) = (F` x) -> (A.h e. (F` a) -. hrf <-> A.h e. (F` x) -. hrf))
9	8	rabbisdv 1807	. . . . . . . . . . . . . . . . . 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 1507	. . . . . . . . . . . . . . . . 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 2623	. . . . . . . . . . . . . . . . . . 19 |- (f = v -> (hrf <-> hrv))
14	13	negbid 611	. . . . . . . . . . . . . . . . . 18 |- (f = v -> (-. hrf <-> -. hrv))
15	14	ralbidv 1663	. . . . . . . . . . . . . . . . 17 |- (f = v -> (A.h e. (F` x) -. hrf <-> A.h e. (F` x) -. hrv))
16		breq1 2622	. . . . . . . . . . . . . . . . . . 19 |- (h = u -> (hrv <-> urv))
17	16	negbid 611	. . . . . . . . . . . . . . . . . 18 |- (h = u -> (-. hrv <-> -. urv))
18	17	cbvralv 1800	. . . . . . . . . . . . . . . . 17 |- (A.h e. (F` x) -. hrv <-> A.u e. (F` x) -. urv)
19	15, 18	syl6bb 536	. . . . . . . . . . . . . . . 16 |- (f = v -> (A.h e. (F` x) -. hrf <-> A.u e. (F` x) -. urv))
20	19	cbvrabv 1911	. . . . . . . . . . . . . . 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 1523	. . . . . . . . . . . . . 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 2512	. . . . . . . . . . . . 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 1486	. . . . . . . . . . . 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 628	. . . . . . . . . . 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 3999	. . . . . . . . . 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 1481	. . . . . . . . . . . 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 616	. . . . . . . . . . 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 4000	. . . . . . . . . 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 1495	. . . . . . . . 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 1475	. . . . . . . . 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 7494	. . . . . . . 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 3983	. . . . . . . . 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 3620	. . . . . . . . . 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 3723	. . . . . . . . . . . 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