Theorem acdc5 7493

Description: A more general version of acdc 7495 that has an initial value and where the function F depends on k.

Hypothesis

Ref	Expression
acdc5.1	|- A e. V

Assertion

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

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

Proof of Theorem acdc5

Step	Hyp	Ref	Expression
1		eqeq2 1484	. . . . . 6 |- (c = C -> ((g` 1) = c <-> (g` 1) = C))
2	1	3anbi2d 898	. . . . 5 |- (c = C -> ((g:NN-->A /\ (g` 1) = c /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) <-> (g:NN-->A /\ (g` 1) = C /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))))
3	2	exbidv 1279	. . . 4 |- (c = C -> (E.g(g:NN-->A /\ (g` 1) = c /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))) <-> E.g(g:NN-->A /\ (g` 1) = C /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))))
4	3	imbi2d 612	. . 3 |- (c = C -> ((F:(NN X. A)-->(P~A \ {(/)}) -> E.g(g:NN-->A /\ (g` 1) = c /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k)))) <-> (F:(NN X. A)-->(P~A \ {(/)}) -> E.g(g:NN-->A /\ (g` 1) = C /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))))
5		acdc5.1	. . . . 5 |- A e. V
6	5	weth 4787	. . . 4 |- E.r r We A
7		eleq1 1534	. . . . . . . . . . . 12 |- (a = x -> (a e. A <-> x e. A))
8		eleq1 1534	. . . . . . . . . . . 12 |- (b = y -> (b e. NN <-> y e. NN))
9	7, 8	bi2anan9 632	. . . . . . . . . . 11 |- ((a = x /\ b = y) -> ((a e. A /\ b e. NN) <-> (x e. A /\ y e. NN)))
10		opreq12 3970	. . . . . . . . . . . . . . . 16 |- ((b = y /\ a = x) -> (bFa) = (yFx))
11	10	ancoms 436	. . . . . . . . . . . . . . 15 |- ((a = x /\ b = y) -> (bFa) = (yFx))
12		rabeq 1809	. . . . . . . . . . . . . . . 16 |- ((bFa) = (yFx) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (bFa) -. hrf})
13		raleq1 1786	. . . . . . . . . . . . . . . . 17 |- ((bFa) = (yFx) -> (A.h e. (bFa) -. hrf <-> A.h e. (yFx) -. hrf))
14	13	rabbisdv 1807	. . . . . . . . . . . . . . . 16 |- ((bFa) = (yFx) -> {f e. (yFx) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (yFx) -. hrf})
15	12, 14	eqtrd 1507	. . . . . . . . . . . . . . 15 |- ((bFa) = (yFx) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (yFx) -. hrf})
16	11, 15	syl 10	. . . . . . . . . . . . . 14 |- ((a = x /\ b = y) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (yFx) -. hrf})
17		breq2 2623	. . . . . . . . . . . . . . . . . 18 |- (f = v -> (hrf <-> hrv))
18	17	negbid 611	. . . . . . . . . . . . . . . . 17 |- (f = v -> (-. hrf <-> -. hrv))
19	18	ralbidv 1663	. . . . . . . . . . . . . . . 16 |- (f = v -> (A.h e. (yFx) -. hrf <-> A.h e. (yFx) -. hrv))
20		breq1 2622	. . . . . . . . . . . . . . . . . 18 |- (h = u -> (hrv <-> urv))
21	20	negbid 611	. . . . . . . . . . . . . . . . 17 |- (h = u -> (-. hrv <-> -. urv))
22	21	cbvralv 1800	. . . . . . . . . . . . . . . 16 |- (A.h e. (yFx) -. hrv <-> A.u e. (yFx) -. urv)
23	19, 22	syl6bb 536	. . . . . . . . . . . . . . 15 |- (f = v -> (A.h e. (yFx) -. hrf <-> A.u e. (yFx) -. urv))
24	23	cbvrabv 1911	. . . . . . . . . . . . . 14 |- {f e. (yFx) | A.h e. (yFx) -. hrf} = {v e. (yFx) | A.u e. (yFx) -. urv}
25	16, 24	syl6eq 1523	. . . . . . . . . . . . 13 |- ((a = x /\ b = y) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {v e. (yFx) | A.u e. (yFx) -. urv})
26	25	unieqd 2512	. . . . . . . . . . . 12 |- ((a = x /\ b = y) -> U.{f e. (bFa) | A.h e. (bFa) -. hrf} = U.{v e. (yFx) | A.u e. (yFx) -. urv})
27	26	eqeq2d 1486	. . . . . . . . . . 11 |- ((a = x /\ b = y) -> (d = U.{f e. (bFa) | A.h e. (bFa) -. hrf} <-> d = U.{v e. (yFx) | A.u e. (yFx) -. urv}))
28	9, 27	anbi12d 628	. . . . . . . . . 10 |- ((a = x /\ b = y) -> (((a e. A /\ b e. NN) /\ d = U.{f e. (bFa) | A.h e. (bFa) -. hrf}) <-> ((x e. A /\ y e. NN) /\ d = U.{v e. (yFx) | A.u e. (yFx) -. urv})))
29	28	cbvoprab12v 3999	. . . . . . . . 9 |- {<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bFa) | A.h e. (bFa) -. hrf})} = {<.<.x, y>., d>. | ((x e. A /\ y e. NN) /\ d = U.{v e. (yFx) | A.u e. (yFx) -. urv})}
30		eqeq1 1481	. . . . . . . . . . 11 |- (d = z -> (d = U.{v e. (yFx) | A.u e. (yFx) -. urv} <-> z = U.{v e. (yFx) | A.u e. (yFx) -. urv}))
31	30	anbi2d 616	. . . . . . . . . 10 |- (d = z -> (((x e. A /\ y e. NN) /\ d = U.{v e. (yFx) | A.u e. (yFx) -. urv}) <-> ((x e. A /\ y e. NN) /\ z = U.{v e. (yFx) | A.u e. (yFx) -. urv})))
32	31	cbvoprab3v 4000	. . . . . . . . 9 |- {<.<.x, y>., d>. | ((x e. A /\ y e. NN) /\ d = U.{v e. (yFx) | A.u e. (yFx) -. urv})} = {<.<.x, y>., z>. | ((x e. A /\ y e. NN) /\ z = U.{v e. (yFx) | A.u e. (yFx) -. urv})}
33	29, 32	eqtr 1495	. . . . . . . 8 |- {<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bFa) | A.h e. (bFa) -. hrf})} = {<.<.x, y>., z>. | ((x e. A /\ y e. NN) /\ z = U.{v e. (yFx) | A.u e. (yFx) -. urv})}
34		eqid 1475	. . . . . . . 8 |- ({<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bFa) | A.h e. (bFa) -. hrf})} seq1 ({<.1, c>.} u. (I |` (NN \ {1})))) = ({<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bFa) | A.h e. (bFa) -. hrf})} seq1 ({<.1, c>.} u. (I |` (NN \ {1}))))
35	5, 33, 34	acdc5lem2 7492	. . . . . . 7 |- ((r We A /\ (c e. A /\ F:(NN X. A)-->(P~A \ {(/)}))) -> (({<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bFa) | A.h e. (bFa) -. hrf})} seq1 ({<.1, c>.} u. (I |` (NN \ {1})))):NN-->A /\ (({<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bFa) | A.h e. (bFa) -. hrf})} seq1 ({<.1, c>.} u. (I |` (NN \ {1}))))` 1) = c