Theorem acdc2 7491

Description: A more general version of acdc 7496 that allows the function F to vary with k.

Hypothesis

Ref	Expression
acdc2.1	|- A e. V

Assertion

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

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

Proof of Theorem acdc2

Step	Hyp	Ref	Expression
1		acdc2.1	. . 3 |- A e. V
2	1	weth 4797	. 2 |- E.r r We A
3		eleq1 1537	. . . . . . . . . . . . 13 |- (a = x -> (a e. A <-> x e. A))
4		eleq1 1537	. . . . . . . . . . . . 13 |- (b = y -> (b e. NN <-> y e. NN))
5	3, 4	bi2anan9 634	. . . . . . . . . . . 12 |- ((a = x /\ b = y) -> ((a e. A /\ b e. NN) <-> (x e. A /\ y e. NN)))
6		opreq12 3976	. . . . . . . . . . . . . . . . 17 |- ((b = y /\ a = x) -> (bFa) = (yFx))
7	6	ancoms 438	. . . . . . . . . . . . . . . 16 |- ((a = x /\ b = y) -> (bFa) = (yFx))
8		rabeq 1812	. . . . . . . . . . . . . . . . 17 |- ((bFa) = (yFx) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (bFa) -. hrf})
9		raleq1 1789	. . . . . . . . . . . . . . . . . 18 |- ((bFa) = (yFx) -> (A.h e. (bFa) -. hrf <-> A.h e. (yFx) -. hrf))
10	9	rabbisdv 1810	. . . . . . . . . . . . . . . . 17 |- ((bFa) = (yFx) -> {f e. (yFx) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (yFx) -. hrf})
11	8, 10	eqtrd 1510	. . . . . . . . . . . . . . . 16 |- ((bFa) = (yFx) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (yFx) -. hrf})
12	7, 11	syl 10	. . . . . . . . . . . . . . 15 |- ((a = x /\ b = y) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (yFx) -. hrf})
13		breq2 2628	. . . . . . . . . . . . . . . . . . 19 |- (f = v -> (hrf <-> hrv))
14	13	negbid 613	. . . . . . . . . . . . . . . . . 18 |- (f = v -> (-. hrf <-> -. hrv))
15	14	ralbidv 1666	. . . . . . . . . . . . . . . . 17 |- (f = v -> (A.h e. (yFx) -. hrf <-> A.h e. (yFx) -. hrv))
16		breq1 2627	. . . . . . . . . . . . . . . . . . 19 |- (h = u -> (hrv <-> urv))
17	16	negbid 613	. . . . . . . . . . . . . . . . . 18 |- (h = u -> (-. hrv <-> -. urv))
18	17	cbvralv 1803	. . . . . . . . . . . . . . . . 17 |- (A.h e. (yFx) -. hrv <-> A.u e. (yFx) -. urv)
19	15, 18	syl6bb 538	. . . . . . . . . . . . . . . 16 |- (f = v -> (A.h e. (yFx) -. hrf <-> A.u e. (yFx) -. urv))
20	19	cbvrabv 1914	. . . . . . . . . . . . . . 15 |- {f e. (yFx) | A.h e. (yFx) -. hrf} = {v e. (yFx) | A.u e. (yFx) -. urv}
21	12, 20	syl6eq 1526	. . . . . . . . . . . . . 14 |- ((a = x /\ b = y) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {v e. (yFx) | A.u e. (yFx) -. urv})
22	21	unieqd 2516	. . . . . . . . . . . . 13 |- ((a = x /\ b = y) -> U.{f e. (bFa) | A.h e. (bFa) -. hrf} = U.{v e. (yFx) | A.u e. (yFx) -. urv})
23	22	eqeq2d 1489	. . . . . . . . . . . 12 |- ((a = x /\ b = y) -> (d = U.{f e. (bFa) | A.h e. (bFa) -. hrf} <-> d = U.{v e. (yFx) | A.u e. (yFx) -. urv}))
24	5, 23	anbi12d 630	. . . . . . . . . . 11 |- ((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})))
25	24	cbvoprab12v 4005	. . . . . . . . . 10 |- {<.<.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})}
26		eqeq1 1484	. . . . . . . . . . . 12 |- (d = z -> (d = U.{v e. (yFx) | A.u e. (yFx) -. urv} <-> z = U.{v e. (yFx) | A.u e. (yFx) -. urv}))
27	26	anbi2d 618	. . . . . . . . . . 11 |- (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})))
28	27	cbvoprab3v 4006	. . . . . . . . . 10 |- {<.<.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})}
29	25, 28	eqtr 1498	. . . . . . . . 9 |- {<.<.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})}
30		eqid 1478	. . . . . . . . 9 |- ({<.<.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}))))
31	1, 29, 30	acdc2lem2 7490	. . . . . . . 8 |- ((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.k e. NN (({<.<.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}))))` (k + 1)) e. ((k + 1)F(({<.<.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}))))` k))))
32		oprex 3989	. . . . . . . . 9 |- ({<.<.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})))) e. V
33		feq1 3626	. . . . . . . . . 10 |- (g = ({<.<.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})))) -> (g: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})))):NN-->A))
34		fveq1 3729	. . . . . . . . . . . 12 |- (g = ({<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bF