Theorem acdc3lem 7578

Description: Lemma for acdc3 7579. 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
acdc3lem.1	|- A e. V
acdc3lem.2	|- S = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
acdc3lem.3	|- G = (S seq1 (NN X. {c}))

Assertion

Ref	Expression
acdc3lem	|- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (G:NN-->A /\ (G` 1) = c /\ 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 acdc3lem

Step	Hyp	Ref	Expression
1		acdc3lem.1	. . . . . 6 |- A e. V
2		acdc3lem.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 4079	. . . . 5 |- S e. V
4		nnex 5993	. . . . . 6 |- NN e. V
5		snex 2806	. . . . . 6 |- {c} e. V
6	4, 5	xpex 3317	. . . . 5 |- (NN X. {c}) e. V
7	3, 6	seq1f 6582	. . . 4 |- (((NN X. {c}):NN-->A /\ S:(A X. A)-->A) -> (S seq1 (NN X. {c})):NN-->A)
8		snssi 2520	. . . . . 6 |- (c e. A -> {c} (_ A)
9		visset 1860	. . . . . . . 8 |- c e. V
10	9	fconst 3715	. . . . . . 7 |- (NN X. {c}):NN-->{c}
11		fss 3692	. . . . . . 7 |- (((NN X. {c}):NN-->{c} /\ {c} (_ A) -> (NN X. {c}):NN-->A)
12	10, 11	mpan 707	. . . . . 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 415	. . . 4 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (NN X. {c}):NN-->A)
15		fvex 3789	. . . . . . . . . . . . 13 |- (F` s) e. V
16	15	rabex 2780	. . . . . . . . . . . 12 |- {v e. (F` s) | A.u e. (F` s) -. urv} e. V
17	16	uniex 2926	. . . . . . . . . . 11 |- U.{v e. (F` s) | A.u e. (F` s) -. urv} e. V
18		fveq2 3781	. . . . . . . . . . . . 13 |- (x = s -> (F` x) = (F` s))
19		rabeq 1856	. . . . . . . . . . . . . 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 1833	. . . . . . . . . . . . . . 15 |- ((F` x) = (F` s) -> (A.u e. (F` x) -. urv <-> A.u e. (F` s) -. urv))
21	20	rabbisdv 1854	. . . . . . . . . . . . . 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 1554	. . . . . . . . . . . . 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 2566	. . . . . . . . . . 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 1523	. . . . . . . . . . 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 4086	. . . . . . . . . 10 |- ((s e. A /\ t e. A) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
27	26	adantl 397	. . . . . . . . 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 3871	. . . . . . . . . . . . . . 15 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) e. (P~A \ {(/)}))
29		eldifi 2213	. . . . . . . . . . . . . . 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 401	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) e. P~A)
32		elpwi 2458	. . . . . . . . . . . . 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 3003	. . . . . . . . . . . . 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 421	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> r We A)
36		eldifn 2214	. . . . . . . . . . . . . . . 16 |- ((F` s) e. (P~A \ {(/)}) -> -. (F` s) e. {(/)})
37		id 59	. . . . . . . . . . . . . . . . . 18 |- ((F` s) = (/) -> (F` s) = (/))
38		0ex 2766	. . . . . . . . . . . . . . . . . . 19 |- (/) e. V
39	38	snid 2487	. . . . . . . . . . . . . . . . . 18 |- (/) e. {(/)}
40	37, 39	syl6eqel 1603	. . . . . . . . . . . . . . . . 17 |- ((F` s) = (/) -> (F` s) e. {(/)})
41	40	necon3bi 1654	. . . . . . . . . . . . . . . 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 401	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) =/= (/))
45	34, 35, 33, 44	syl3anc 870	. . . . . . . . . . . 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 2119	. . . . . . . . . . 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 407	. . . . . . . . . 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 404	. . . . . . . . 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 1595	. . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) e. A)
50	49	ex 380	. . . . . . 7 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> ((s e. A /\ t e. A) -> (sSt) e. A))
51	50	r19.21aivv 1767	. . . . . 6 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> A.s e. A A.t e. A (sSt) e. A)
52		fvex 3789	. . . . . . . . 9 |- (F` x) e. V
53	52	rabex 2780	. . . . . . . 8 |- {v e. (F` x) | A.u e. (F` x) -. urv} e. V
54	53	uniex 2926	. . . . . . 7 |- U.{v e. (F` x) | A.u e. (F` x) -. urv} e. V
55	54, 2	fnoprab2 4180	. . . . . 6 |- S Fn (A X. A)
56	51, 55	jctil 299	. . . . 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 4072	. . . . 5 |- (S:(A X. A)-->A <-> (S Fn (A X. A) /\ A.s