Theorem tfrlem9 3919

Description: Lemma for transfinite recursion. Here we compute the value of F (the union of all acceptable functions).

Hypotheses

Ref	Expression
tfrlem.1	|- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
tfrlem.2	|- F = U.A

Assertion

Ref	Expression
tfrlem9	|- (y e. dom F -> (F` y) = (G` (F |` y)))

Distinct variable groups:   x,y,f,A   x,F,y,f   x,G,y,f

Proof of Theorem tfrlem9

Step	Hyp	Ref	Expression
1		visset 1813	. . 3 |- y e. V
2	1	eldm2 3308	. 2 |- (y e. dom F <-> E.z<.y, z>. e. F)
3		tfrlem.2	. . . . . . 7 |- F = U.A
4		tfrlem.1	. . . . . . . 8 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
5	4	unieqi 2511	. . . . . . 7 |- U.A = U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
6	3, 5	eqtr 1495	. . . . . 6 |- F = U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
7	6	eleq2i 1538	. . . . 5 |- (<.y, z>. e. F <-> <.y, z>. e. U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))})
8		eluniab 2513	. . . . 5 |- (<.y, z>. e. U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))} <-> E.f(<.y, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))))
9	7, 8	bitr 173	. . . 4 |- (<.y, z>. e. F <-> E.f(<.y, z>. e. f /\ E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))))
10		fnop 3591	. . . . . . . . . . . . . 14 |- ((f Fn x /\ <.y, z>. e. f) -> y e. x)
11		ra4e 1695	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))))
12	4	abeq2i 1570	. . . . . . . . . . . . . . . . 17 |- (f e. A <-> E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))))
13		elssuni 2526	. . . . . . . . . . . . . . . . . 18 |- (f e. A -> f (_ U.A)
14	13, 3	syl6ssr 2108	. . . . . . . . . . . . . . . . 17 |- (f e. A -> f (_ F)
15	12, 14	sylbir 201	. . . . . . . . . . . . . . . 16 |- (E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y))) -> f (_ F)
16	11, 15	syl 10	. . . . . . . . . . . . . . 15 |- ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> f (_ F)
17		ra4 1694	. . . . . . . . . . . . . . . . . . 19 |- (A.y e. x (f` y) = (G` (f |` y)) -> (y e. x -> (f` y) = (G` (f |` y))))
18	17	com12 11	. . . . . . . . . . . . . . . . . 18 |- (y e. x -> (A.y e. x (f` y) = (G` (f |` y)) -> (f` y) = (G` (f |` y))))
19		fndm 3587	. . . . . . . . . . . . . . . . . . . . 21 |- (f Fn x -> dom f = x)
20	19	eleq2d 1541	. . . . . . . . . . . . . . . . . . . 20 |- (f Fn x -> (y e. dom f <-> y e. x))
21	4, 3	tfrlem7 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- Fun F
22		funssfv 3735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((Fun F /\ f (_ F /\ y e. dom f) -> (F` y) = (f` y))
23	21, 22	mp3an1 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f (_ F /\ y e. dom f) -> (F` y) = (f` y))
24	23	adantrl 394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f (_ F /\ ((f Fn x /\ x e. On) /\ y e. dom f)) -> (F` y) = (f` y))
25		fun2ssres 3553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((Fun F /\ f (_ F /\ y (_ dom f) -> (F |` y) = (f |` y))
26	25	fveq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((Fun F /\ f (_ F /\ y (_ dom f) -> (G` (F |` y)) = (G` (f |` y)))
27	21, 26	mp3an1 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((f (_ F /\ y (_ dom f) -> (G` (F |` y)) = (G` (f |` y)))
28	19	eleq1d 1540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (f Fn x -> (dom f e. On <-> x e. On))
29		onelsst 3000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (dom f e. On -> (y e. dom f -> y (_ dom f))
30	28, 29	syl6bir 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (f Fn x -> (x e. On -> (y e. dom f -> y (_ dom f)))
31	30	imp31 362	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((f Fn x /\ x e. On) /\ y e. dom f) -> y (_ dom f)
32	27, 31	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((f (_ F /\ ((f Fn x /\ x e. On) /\ y e. dom f)) -> (G` (F |` y)) = (G` (f |` y)))
33	24, 32	eqeq12d 1489	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((f (_ F /\ ((f Fn x /\ x e. On) /\ y e. dom f)) -> ((F` y) = (G` (F |` y)) <-> (f` y) = (G` (f |` y))))
34	33	biimprd 154	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((f (_ F /\ ((f Fn x /\ x e. On) /\ y e. dom f)) -> ((f` y) = (G` (f |` y)) -> (F` y) = (G` (F |` y))))
35	34	ex 373	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f (_ F -> (((f Fn x /\ x e. On) /\ y e. dom f) -> ((f` y) = (G` (f |` y)) -> (F` y) = (G` (F |` y)))))
36	35	com3l 34	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((f Fn x /\ x e. On) /\ y e. dom f) -> ((f` y) = (G` (f |` y)) -> (f (_ F -> (F` y) = (G` (F |` y)))))
37	36	exp31 376	. . . . . . . . . . . . . . . . . . . . . 22 |- (f Fn x -> (x e. On -> (y e. dom f -> ((f` y) = (G` (f |` y)) -> (f (_ F -> (F` y) = (G` (F |` y)))))))
38	37	com34 36	. . . . . . . . . . . . . . . . . . . . 21 |- (f Fn x -> (x e. On -> ((f` y) = (G` (f |` y)) -> (y e. dom f -> (f (_ F -> (F` y) = (G` (F |` y)))))))
39	38	com24 37	. . . . . . . . . . . . . . . . . . . 20 |- (f Fn x -> (y e. dom f -> ((f` y) = (G` (f |` y)) -> (x e. On -> (f (_ F -> (F` y) = (G` (F |` y)))))))
40	20, 39	sylbird 205	. . . . . . . . . . . . . . . . . . 19 |- (f Fn x -> (y e. x -> ((f` y) = (G` (f |` y)) -> (x e. On -> (f (_ F -> (F` y) = (G` (F |` y)))))))
41	40	com3l 34	. . . . . . . . . . . . . . . . . 18 |- (y e. x -> ((f` y) = (G` (f |` y)) -> (f Fn x -> (x e. On -> (f (_ F -> (F` y) = (G` (F |` y)))))))
42	18, 41	syld 27	. . . . . . . . . . . . . . . . 17 |- (y e. x -> (A.y e. x (f` y) = (G` (f |` y)) -> (f Fn x -> (x e. On -> (f (_ F -> (F` y) = (G` (F |` y)))))))
43	42	com24 37	. . . . . . . . . . . . . . . 16 |- (y e. x -> (x e. On -> (f Fn x -> (A.y e. x (f` y) = (G` (f |` y)) -> (f (_ F -> (F` y) = (G` (F |` y)))))))
44	43	imp4d 367	. . . . . . . . . . . . . . 15 |- (y e. x -> ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> (f (_ F -> (F` y) = (G` (F |` y)))))
45	16, 44	mpdi 48	. . . . . . . . . . . . . 14 |- (y e. x -> ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> (F` y) = (G` (F |` y))))
46	10, 45	syl 10	. . . . . . . . . . . . 13 |- ((f Fn x /\ <.y, z>. e. f) -> ((x e. On /\ (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))) -> (F` y) = (G` (F |` y))))
47	46	exp4d 381	. . . . . . . . . . . 12 |- ((f Fn x /\ <.y, z>. e. f) -> (x e. On -> (f Fn x -> (A.y e. x (f` y) = (G` (f |` y)) -> (F` y) = (G` (F |` y))))))
48	47	ex 373	. . . . . . . . . . 11 |- (f Fn x -> (<.y, z>. e. f -> (x e. On -> (f Fn x -> (A.y e. x (f` y) = (G` (f |` y)) -> (F` y) = (G` (F |` y)))))))
49	48	com4r 41	. . . . . . . . . 10 |- (f Fn x -> (f Fn x -> (<.y, z>. e.