Theorem acdclem 7495

Description: Lemma for acdc 7496. Build a sequence G starting at value c, as follows. Given a previous value x of G, we construct, for the next value of G, the v such that A.u e. (F` x)-. urv, which is unique when r is a well-ordering on A.

Hypotheses

Ref	Expression
acdclem.1	|- A e. V
acdclem.2	|- S = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
acdclem.3	|- G = (S seq1 (NN X. {c}))

Assertion

Ref	Expression
acdclem	|- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (G:NN-->A /\ A.k e. NN (G` (k + 1)) e. (F` (G` k))))

Distinct variable groups:   u,k,v,x,y,z,A   k,F,u,v,x,y,z   u,G,v,x,y,z   k,c,x,y,z   k,r,u,v,x,y,z

Proof of Theorem acdclem

Step	Hyp	Ref	Expression
1		acdclem.1	. . . . . 6 |- A e. V
2		acdclem.2	. . . . . 6 |- S = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
3	1, 1, 2	oprabex2 4027	. . . . 5 |- S e. V
4		nnex 5935	. . . . . 6 |- NN e. V
5		snex 2756	. . . . . 6 |- {c} e. V
6	4, 5	xpex 3266	. . . . 5 |- (NN X. {c}) e. V
7	3, 6	seq1f 6324	. . . 4 |- (((NN X. {c}):NN-->A /\ S:(A X. A)-->A) -> (S seq1 (NN X. {c})):NN-->A)
8		snssi 2470	. . . . . 6 |- (c e. A -> {c} (_ A)
9		visset 1816	. . . . . . . 8 |- c e. V
10	9	fconst 3664	. . . . . . 7 |- (NN X. {c}):NN-->{c}
11		fss 3641	. . . . . . 7 |- (((NN X. {c}):NN-->{c} /\ {c} (_ A) -> (NN X. {c}):NN-->A)
12	10, 11	mpan 697	. . . . . 6 |- ({c} (_ A -> (NN X. {c}):NN-->A)
13	8, 12	syl 10	. . . . 5 |- (c e. A -> (NN X. {c}):NN-->A)
14	13	ad2antrl 408	. . . 4 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (NN X. {c}):NN-->A)
15		fvex 3738	. . . . . . . . . . . . 13 |- (F` s) e. V
16	15	rabex 2730	. . . . . . . . . . . 12 |- {v e. (F` s) | A.u e. (F` s) -. urv} e. V
17	16	uniex 2876	. . . . . . . . . . 11 |- U.{v e. (F` s) | A.u e. (F` s) -. urv} e. V
18		fveq2 3730	. . . . . . . . . . . . 13 |- (x = s -> (F` x) = (F` s))
19		rabeq 1812	. . . . . . . . . . . . . 14 |- ((F` x) = (F` s) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` x) -. urv})
20		raleq1 1789	. . . . . . . . . . . . . . 15 |- ((F` x) = (F` s) -> (A.u e. (F` x) -. urv <-> A.u e. (F` s) -. urv))
21	20	rabbisdv 1810	. . . . . . . . . . . . . 14 |- ((F` x) = (F` s) -> {v e. (F` s) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
22	19, 21	eqtrd 1510	. . . . . . . . . . . . 13 |- ((F` x) = (F` s) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
23	18, 22	syl 10	. . . . . . . . . . . 12 |- (x = s -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
24	23	unieqd 2516	. . . . . . . . . . 11 |- (x = s -> U.{v e. (F` x) | A.u e. (F` x) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv})
25		eqidd 1479	. . . . . . . . . . 11 |- (y = t -> U.{v e. (F` s) | A.u e. (F` s) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv})
26	17, 24, 25, 2	oprabval2 4034	. . . . . . . . . 10 |- ((s e. A /\ t e. A) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
27	26	adantl 390	. . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
28		ffvelrn 3820	. . . . . . . . . . . . . . 15 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) e. (P~A \ {(/)}))
29		eldifi 2165	. . . . . . . . . . . . . . 15 |- ((F` s) e. (P~A \ {(/)}) -> (F` s) e. P~A)
30	28, 29	syl 10	. . . . . . . . . . . . . 14 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) e. P~A)
31	30	adantll 394	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) e. P~A)
32		elpwi 2410	. . . . . . . . . . . . 13 |- ((F` s) e. P~A -> (F` s) (_ A)
33	31, 32	syl 10	. . . . . . . . . . . 12 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) (_ A)
34	15	wereucl 2952	. . . . . . . . . . . . 13 |- ((r We A /\ (F` s) (_ A /\ (F` s) =/= (/)) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. (F` s))
35		simpll 414	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> r We A)
36		eldifn 2166	. . . . . . . . . . . . . . . 16 |- ((F` s) e. (P~A \ {(/)}) -> -. (F` s) e. {(/)})
37		id 59	. . . . . . . . . . . . . . . . . 18 |- ((F` s) = (/) -> (F` s) = (/))
38		0ex 2716	. . . . . . . . . . . . . . . . . . 19 |- (/) e. V
39	38	snid 2439	. . . . . . . . . . . . . . . . . 18 |- (/) e. {(/)}
40	37, 39	syl6eqel 1559	. . . . . . . . . . . . . . . . 17 |- ((F` s) = (/) -> (F` s) e. {(/)})
41	40	necon3bi 1610	. . . . . . . . . . . . . . . 16 |- (-. (F` s) e. {(/)} -> (F` s) =/= (/))
42	36, 41	syl 10	. . . . . . . . . . . . . . 15 |- ((F` s) e. (P~A \ {(/)}) -> (F` s) =/= (/))
43	28, 42	syl 10	. . . . . . . . . . . . . 14 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) =/= (/))
44	43	adantll 394	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) =/= (/))
45	34, 35, 33, 44	syl3anc 860	. . . . . . . . . . . 12 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. (F` s))
46	33, 45	sseldd 2071	. . . . . . . . . . 11 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
47	46	adantlrl 400	. . . . . . . . . 10 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
48	47	adantrr 397	. . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
49	27, 48	eqeltrd 1551	. . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) e. A)
50	49	ex 373	. . . . . . 7 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> ((s e. A /\ t e. A) -> (sSt) e. A))
51	50	r19.21aivv 1723	. . . . . 6 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> A.s e. A A.t e. A (sSt) e. A)
52		fvex 3738	. . . . . . . . 9 |- (F` x) e. V
53	52	rabex 2730	. . . . . . . 8 |- {v e. (F` x) | A.u e. (F` x) -. urv} e. V
54	53	uniex 2876	. . . . . . 7 |- U.{v e. (F` x) | A.u e. (F` x) -. urv} e. V
55	54, 2	fnoprab2 4128	. . . . . 6 |- S Fn (A X. A)
56	51, 55	jctil 292	. . . . 5 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (S Fn (A X. A) /\ A.s e. A A.t e. A (sSt) e. A))
57		ffnoprval 4020	. . . . 5 |- (S:(A X. A)-->A <-> (S Fn (A X. A) /\ A.s e. A A.t e. A (s