Theorem acdclem 7436

Description: Lemma for acdc 7437. 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 4006	. . . . 5 |- S e. V
4		nnex 5881	. . . . . 6 |- NN e. V
5		snex 2740	. . . . . 6 |- {c} e. V
6	4, 5	xpex 3250	. . . . 5 |- (NN X. {c}) e. V
7	3, 6	seq1f 6260	. . . 4 |- (((NN X. {c}):NN-->A /\ S:(A X. A)-->A) -> (S seq1 (NN X. {c})):NN-->A)
8		snssi 2457	. . . . . 6 |- (c e. A -> {c} (_ A)
9		visset 1804	. . . . . . . 8 |- c e. V
10	9	fconst 3643	. . . . . . 7 |- (NN X. {c}):NN-->{c}
11		fss 3620	. . . . . . 7 |- (((NN X. {c}):NN-->{c} /\ {c} (_ A) -> (NN X. {c}):NN-->A)
12	10, 11	mpan 693	. . . . . 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 406	. . . 4 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (NN X. {c}):NN-->A)
15		fvex 3717	. . . . . . . . . . . . 13 |- (F` s) e. V
16	15	rabex 2715	. . . . . . . . . . . 12 |- {v e. (F` s) | A.u e. (F` s) -. urv} e. V
17	16	uniex 2861	. . . . . . . . . . 11 |- U.{v e. (F` s) | A.u e. (F` s) -. urv} e. V
18		fveq2 3709	. . . . . . . . . . . . 13 |- (x = s -> (F` x) = (F` s))
19		rabeq 1800	. . . . . . . . . . . . . 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 1778	. . . . . . . . . . . . . . 15 |- ((F` x) = (F` s) -> (A.u e. (F` x) -. urv <-> A.u e. (F` s) -. urv))
21	20	rabbisdv 1798	. . . . . . . . . . . . . 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 1499	. . . . . . . . . . . . 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 2502	. . . . . . . . . . 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		eqid 1468	. . . . . . . . . . . 12 |- U.{v e. (F` s) | A.u e. (F` s) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv}
26	25	a1i 8	. . . . . . . . . . 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})
27	17, 24, 26, 2	oprabval2 4013	. . . . . . . . . 10 |- ((s e. A /\ t e. A) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
28	27	adantl 388	. . . . . . . . 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})
29		ffvelrn 3799	. . . . . . . . . . . . . . 15 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) e. (P~A \ {(/)}))
30		eldifi 2152	. . . . . . . . . . . . . . 15 |- ((F` s) e. (P~A \ {(/)}) -> (F` s) e. P~A)
31	29, 30	syl 10	. . . . . . . . . . . . . 14 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) e. P~A)
32	31	adantll 392	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) e. P~A)
33		elpwi 2396	. . . . . . . . . . . . 13 |- ((F` s) e. P~A -> (F` s) (_ A)
34	32, 33	syl 10	. . . . . . . . . . . 12 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) (_ A)
35	15	wereucl 2936	. . . . . . . . . . . . 13 |- ((r We A /\ (F` s) (_ A /\ (F` s) =/= (/)) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. (F` s))
36		simpll 412	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> r We A)
37		eldifn 2153	. . . . . . . . . . . . . . . 16 |- ((F` s) e. (P~A \ {(/)}) -> -. (F` s) e. {(/)})
38		id 59	. . . . . . . . . . . . . . . . . 18 |- ((F` s) = (/) -> (F` s) = (/))
39		0ex 2701	. . . . . . . . . . . . . . . . . . 19 |- (/) e. V
40	39	snid 2425	. . . . . . . . . . . . . . . . . 18 |- (/) e. {(/)}
41	38, 40	syl6eqel 1548	. . . . . . . . . . . . . . . . 17 |- ((F` s) = (/) -> (F` s) e. {(/)})
42	41	necon3bi 1599	. . . . . . . . . . . . . . . 16 |- (-. (F` s) e. {(/)} -> (F` s) =/= (/))
43	37, 42	syl 10	. . . . . . . . . . . . . . 15 |- ((F` s) e. (P~A \ {(/)}) -> (F` s) =/= (/))
44	29, 43	syl 10	. . . . . . . . . . . . . 14 |- ((F:A-->(P~A \ {(/)}) /\ s e. A) -> (F` s) =/= (/))
45	44	adantll 392	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> (F` s) =/= (/))
46	35, 36, 34, 45	syl3anc 856	. . . . . . . . . . . 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))
47	34, 46	sseldd 2058	. . . . . . . . . . 11 |- (((r We A /\ F:A-->(P~A \ {(/)})) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
48	47	adantlrl 398	. . . . . . . . . 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)
49	48	adantrr 395	. . . . . . . . 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)
50	28, 49	eqeltrd 1540	. . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) e. A)
51	50	ex 373	. . . . . . 7 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> ((s e. A /\ t e. A) -> (sSt) e. A))
52	51	r19.21aivv 1712	. . . . . 6 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> A.s e. A A.t e. A (sSt) e. A)
53		fvex 3717	. . . . . . . . 9 |- (F` x) e. V
54	53	rabex 2715	. . . . . . . 8 |- {v e. (F` x) | A.u e. (F` x) -. urv} e. V
55	54	uniex 2861	. . . . . . 7 |- U.{v e. (F` x) | A.u e. (F` x) -. urv} e. V
56	55, 2	fnoprab2 4106	. . . . . 6 |- S Fn (A X. A)
57	52, 56	jctil 292	. . . . 5 |- ((r We A /\ (c e. A /\ F:A-->(P~A \ {(/)}))) -> (S Fn (A X. A) /\ A.