Theorem acdc2 7440

Description: A more general version of acdc 7445 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 4767	. 2 |- E.r r We A
3		eleq1 1531	. . . . . . . . . . . . 13 |- (a = x -> (a e. A <-> x e. A))
4		eleq1 1531	. . . . . . . . . . . . 13 |- (b = y -> (b e. NN <-> y e. NN))
5	3, 4	bi2anan9 631	. . . . . . . . . . . 12 |- ((a = x /\ b = y) -> ((a e. A /\ b e. NN) <-> (x e. A /\ y e. NN)))
6		opreq12 3961	. . . . . . . . . . . . . . . . 17 |- ((b = y /\ a = x) -> (bFa) = (yFx))
7	6	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((a = x /\ b = y) -> (bFa) = (yFx))
8		rabeq 1805	. . . . . . . . . . . . . . . . 17 |- ((bFa) = (yFx) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (bFa) -. hrf})
9		raleq1 1783	. . . . . . . . . . . . . . . . . 18 |- ((bFa) = (yFx) -> (A.h e. (bFa) -. hrf <-> A.h e. (yFx) -. hrf))
10	9	rabbisdv 1803	. . . . . . . . . . . . . . . . 17 |- ((bFa) = (yFx) -> {f e. (yFx) | A.h e. (bFa) -. hrf} = {f e. (yFx) | A.h e. (yFx) -. hrf})
11	8, 10	eqtrd 1504	. . . . . . . . . . . . . . . 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 2618	. . . . . . . . . . . . . . . . . . 19 |- (f = v -> (hrf <-> hrv))
14	13	negbid 610	. . . . . . . . . . . . . . . . . 18 |- (f = v -> (-. hrf <-> -. hrv))
15	14	ralbidv 1660	. . . . . . . . . . . . . . . . 17 |- (f = v -> (A.h e. (yFx) -. hrf <-> A.h e. (yFx) -. hrv))
16		breq1 2617	. . . . . . . . . . . . . . . . . . 19 |- (h = u -> (hrv <-> urv))
17	16	negbid 610	. . . . . . . . . . . . . . . . . 18 |- (h = u -> (-. hrv <-> -. urv))
18	17	cbvralv 1796	. . . . . . . . . . . . . . . . 17 |- (A.h e. (yFx) -. hrv <-> A.u e. (yFx) -. urv)
19	15, 18	syl6bb 535	. . . . . . . . . . . . . . . 16 |- (f = v -> (A.h e. (yFx) -. hrf <-> A.u e. (yFx) -. urv))
20	19	cbvrabv 1907	. . . . . . . . . . . . . . 15 |- {f e. (yFx) | A.h e. (yFx) -. hrf} = {v e. (yFx) | A.u e. (yFx) -. urv}
21	12, 20	syl6eq 1520	. . . . . . . . . . . . . 14 |- ((a = x /\ b = y) -> {f e. (bFa) | A.h e. (bFa) -. hrf} = {v e. (yFx) | A.u e. (yFx) -. urv})
22	21	unieqd 2507	. . . . . . . . . . . . 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 1483	. . . . . . . . . . . 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 627	. . . . . . . . . . 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 3990	. . . . . . . . . 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 1478	. . . . . . . . . . . 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 615	. . . . . . . . . . 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 3991	. . . . . . . . . 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 1492	. . . . . . . . 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 1473	. . . . . . . . 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 7439	. . . . . . . 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 3974	. . . . . . . . 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 3612	. . . . . . . . . 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 3714	. . . . . . . . . . . 12 |- (g = ({<.<.a, b>., d>. | ((a e. A /\ b e. NN) /\ d = U.{f e. (bFa)