Theorem acdc3 7429

Description: Dependent Choice. Axiom DC1 of [Schechter] p. 149, with the addition of an initial value C. 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
acdc3.1	|- A e. V

Assertion

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

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

Proof of Theorem acdc3

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