Theorem acdc5lem2 7492

Description: Lemma for acdc5 7493. 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. (yFx)-. urv, which is unique when r is a well-ordering on A.

Hypotheses

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

Assertion

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

Step	Hyp	Ref	Expression
1		acdc5lem.1	. . . . . . 7 |- A e. V
2		nnex 5933	. . . . . . 7 |- NN e. V
3		acdc5lem.2	. . . . . . 7 |- S = {<.<.x, y>., z>. | ((x e. A /\ y e. NN) /\ z = U.{v e. (yFx) | A.u e. (yFx) -. urv})}
4	1, 2, 3	oprabex2 4021	. . . . . 6 |- S e. V
5		snex 2750	. . . . . . 7 |- {<.1, c>.} e. V
6		difexg 2722	. . . . . . . . 9 |- (NN e. V -> (NN \ {1}) e. V)
7	2, 6	ax-mp 7	. . . . . . . 8 |- (NN \ {1}) e. V
8		resiexg 3396	. . . . . . . 8 |- ((NN \ {1}) e. V -> (I |` (NN \ {1})) e. V)
9	7, 8	ax-mp 7	. . . . . . 7 |- (I |` (NN \ {1})) e. V
10	5, 9	unex 2872	. . . . . 6 |- ({<.1, c>.} u. (I |` (NN \ {1}))) e. V
11	4, 10	seq1f2 6324	. . . . 5 |- (((({<.1, c>.} u. (I |` (NN \ {1})))` 1) e. A /\ (({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})):(NN \ {1})-->NN /\ S:(A X. NN)-->A) -> (S seq1 ({<.1, c>.} u. (I |` (NN \ {1})))):NN-->A)
12	11	3expa 833	. . . 4 |- ((((({<.1, c>.} u. (I |` (NN \ {1})))` 1) e. A /\ (({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})):(NN \ {1})-->NN) /\ S:(A X. NN)-->A) -> (S seq1 ({<.1, c>.} u. (I |` (NN \ {1})))):NN-->A)
13		id 59	. . . . . . 7 |- (c e. A -> c e. A)
14		1nn 5934	. . . . . . . . 9 |- 1 e. NN
15	14	elisseti 1818	. . . . . . . 8 |- 1 e. V
16		visset 1813	. . . . . . . 8 |- c e. V
17		eqid 1475	. . . . . . . 8 |- ({<.1, c>.} u. (I |` (NN \ {1}))) = ({<.1, c>.} u. (I |` (NN \ {1})))
18	15, 16, 17	fvsnun1 3795	. . . . . . 7 |- (({<.1, c>.} u. (I |` (NN \ {1})))` 1) = c
19	13, 18	syl5eqel 1552	. . . . . 6 |- (c e. A -> (({<.1, c>.} u. (I |` (NN \ {1})))` 1) e. A)
20	19	ad2antrl 406	. . . . 5 |- ((r We A /\ (c e. A /\ F:(NN X. A)-->(P~A \ {(/)}))) -> (({<.1, c>.} u. (I |` (NN \ {1})))` 1) e. A)
21		f1oi 3717	. . . . . . . 8 |- (I |` (NN \ {1})):(NN \ {1})-1-1-onto->(NN \ {1})
22		f1of 3689	. . . . . . . 8 |- ((I |` (NN \ {1})):(NN \ {1})-1-1-onto->(NN \ {1}) -> (I |` (NN \ {1})):(NN \ {1})-->(NN \ {1}))
23	21, 22	ax-mp 7	. . . . . . 7 |- (I |` (NN \ {1})):(NN \ {1})-->(NN \ {1})
24		difss 2167	. . . . . . 7 |- (NN \ {1}) (_ NN
25		fss 3635	. . . . . . 7 |- (((I |` (NN \ {1})):(NN \ {1})-->(NN \ {1}) /\ (NN \ {1}) (_ NN) -> (I |` (NN \ {1})):(NN \ {1})-->NN)
26	23, 24, 25	mp2an 697	. . . . . 6 |- (I |` (NN \ {1})):(NN \ {1})-->NN
27		resundir 3379	. . . . . . . 8 |- (({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})) = (({<.1, c>.} |` (NN \ {1})) u. ((I |` (NN \ {1})) |` (NN \ {1})))
28		difdisj 2337	. . . . . . . . . 10 |- ({1} i^i (NN \ {1})) = (/)
29	15, 16	f1osn 3719	. . . . . . . . . . . 12 |- {<.1, c>.}:{1}-1-1-onto->{c}
30		f1ofn 3690	. . . . . . . . . . . 12 |- ({<.1, c>.}:{1}-1-1-onto->{c} -> {<.1, c>.} Fn {1})
31	29, 30	ax-mp 7	. . . . . . . . . . 11 |- {<.1, c>.} Fn {1}
32		fnresdisj 3597	. . . . . . . . . . 11 |- ({<.1, c>.} Fn {1} -> (({1} i^i (NN \ {1})) = (/) <-> ({<.1, c>.} |` (NN \ {1})) = (/)))
33	31, 32	ax-mp 7	. . . . . . . . . 10 |- (({1} i^i (NN \ {1})) = (/) <-> ({<.1, c>.} |` (NN \ {1})) = (/))
34	28, 33	mpbi 189	. . . . . . . . 9 |- ({<.1, c>.} |` (NN \ {1})) = (/)
35		residm 3390	. . . . . . . . 9 |- ((I |` (NN \ {1})) |` (NN \ {1})) = (I |` (NN \ {1}))
36	34, 35	uneq12i 2182	. . . . . . . 8 |- (({<.1, c>.} |` (NN \ {1})) u. ((I |` (NN \ {1})) |` (NN \ {1}))) = ((/) u. (I |` (NN \ {1})))
37		uncom 2176	. . . . . . . . 9 |- ((I |` (NN \ {1})) u. (/)) = ((/) u. (I |` (NN \ {1})))
38		un0 2297	. . . . . . . . 9 |- ((I |` (NN \ {1})) u. (/)) = (I |` (NN \ {1}))
39	37, 38	eqtr3 1497	. . . . . . . 8 |- ((/) u. (I |` (NN \ {1}))) = (I |` (NN \ {1}))
40	27, 36, 39	3eqtr 1499	. . . . . . 7 |- (({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})) = (I |` (NN \ {1}))
41		feq1 3620	. . . . . . 7 |- ((({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})) = (I |` (NN \ {1})) -> ((({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})):(NN \ {1})-->NN <-> (I |` (NN \ {1})):(NN \ {1})-->NN))
42	40, 41	ax-mp 7	. . . . . 6 |- ((({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})):(NN \ {1})-->NN <-> (I |` (NN \ {1})):(NN \ {1})-->NN)
43	26, 42	mpbir 190	. . . . 5 |- (({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})):(NN \ {1})-->NN
44	20, 43	jctir 293	. . . 4 |- ((r We A /\ (c e. A /\ F:(NN X. A)-->(P~A \ {(/)}))) -> ((({<.1, c>.} u. (I |` (NN \ {1})))` 1) e. A /\ (({<.1, c>.} u. (I |` (NN \ {1}))) |` (NN \ {1})):(NN \ {1})-->NN))
45		acdc5lem.3	. . . . . . . . . . 11 |- G = (S seq1 ({<.1, c>.} u. (I |` (NN \ {1}))))
46	1, 3, 45	acdc5lem1 7491	. . . . . . . . . 10 |- (((r We A /\ F:(NN X. A)-->(P~A \ {(/)})) /\ (s e. A /\ t e. NN)) -> ((sSt) e. (tFs) /\ (sSt) e. A))
47	46	pm3.27d 325	. . . . . . . . 9 |- (((r We A /\ F:(NN X. A)-->(P~A \ {(/)})) /\ (s e. A /\ t e. NN)) -> (sSt) e. A)
48	47	ex 373	. . . . . . . 8 |- ((r We A /\ F:(NN X. A)-->(P~A \ {(/)})) -> ((s e. A /\ t e. NN) -> (sSt) e. A))
49	48	r19.21aivv 1720	. . . . . . 7 |- ((r We A /\ F:(NN X. A)-->(P~A \ {(/)})) -> A.s e. A A.t e. NN (sSt) e. A)
50		oprex 3983	. . . . . . . . . 10