Theorem tfrlem5 2953

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains.

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
tfrlem5	|- ((g e. A /\ h e. A) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))

Distinct variable group(s):   x,y,f,g,h,A   x,v,u,F,y,f   x,G,y,f,g,h   v,g,h,u

Proof of Theorem tfrlem5

Step	Hyp	Ref	Expression
1		tfrlem.1	. . . . . 6 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
2	1	tfrlem3 2951	. . . . 5 |- A = {g | E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y)))}
3	2	cleqabi 1176	. . . 4 |- (g e. A <-> E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))))
4	1	tfrlem3 2951	. . . . 5 |- A = {h | E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))}
5	4	cleqabi 1176	. . . 4 |- (h e. A <-> E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y))))
6	3, 5	anbi12i 369	. . 3 |- ((g e. A /\ h e. A) <-> (E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))))
7		reeanv 1316	. . 3 |- (E.z e. On E.w e. On ((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))) <-> (E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))))
8	6, 7	bitr4 154	. 2 |- ((g e. A /\ h e. A) <-> E.z e. On E.w e. On ((g Fn z /\ A.y e. z (g` y) = (G` (g |` y))) /\ (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))))
9		2elresin 2733	. . . . . . . . 9 |- ((g Fn z /\ h Fn w) -> ((<.x, u>. e. g /\ <.x, v>. e. h) <-> (<.x, u>. e. (g |` (z i^i w)) /\ <.x, v>. e. (h |` (z i^i w)))))
10		tfrlem2 2950	. . . . . . . . . 10 |- (((g |` (z i^i w)) Fn (z i^i w) /\ (h |` (z i^i w)) Fn (z i^i w)) -> ((<.x, u>. e. (g |` (z i^i w)) /\ <.x, v>. e. (h |` (z i^i w))) -> ((z i^i w) e. On -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> u = v))))
11		fnresin1 2735	. . . . . . . . . 10 |- (g Fn z -> (g |` (z i^i w)) Fn (z i^i w))
12		fnresin2 2736	. . . . . . . . . 10 |- (h Fn w -> (h |` (z i^i w)) Fn (z i^i w))
13	10, 11, 12	syl2an 349	. . . . . . . . 9 |- ((g Fn z /\ h Fn w) -> ((<.x, u>. e. (g |` (z i^i w)) /\ <.x, v>. e. (h |` (z i^i w))) -> ((z i^i w) e. On -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> u = v))))
14	9, 13	sylbid 178	. . . . . . . 8 |- ((g Fn z /\ h Fn w) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> ((z i^i w) e. On -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> u = v))))
15	14	com24 37	. . . . . . 7 |- ((g Fn z /\ h Fn w) -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> ((z i^i w) e. On -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))))
16	15	com3r 35	. . . . . 6 |- ((z i^i w) e. On -> ((g Fn z /\ h Fn w) -> (A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))))
17	16	imp32 281	. . . . 5 |- (((z i^i w) e. On /\ ((g Fn z /\ h Fn w) /\ A.y((z i^i w) e. On -> (y e. (z i^i w) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) /\ ((h |` (z i^i w))` y) = (G` ((h |` (z i^i w)) |` y))))))) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))
18		onin 2229	. . . . 5 |- ((z e. On /\ w e. On) -> (z i^i w) e. On)
19		r19.26m 1291	. . . . . . . 8 |- (A.y((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) <-> (A.y e. z (g` y) = (G` (g |` y)) /\ A.y e. w (h` y) = (G` (h |` y))))
20		prth 429	. . . . . . . . . . . 12 |- (((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) -> ((y e. z /\ y e. w) -> ((g` y) = (G` (g |` y)) /\ (h` y) = (G` (h |` y)))))
21		pm3.27 260	. . . . . . . . . . . . 13 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> y e. (z i^i w))
22		elin 1635	. . . . . . . . . . . . 13 |- (y e. (z i^i w) <-> (y e. z /\ y e. w))
23	21, 22	sylib 173	. . . . . . . . . . . 12 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (y e. z /\ y e. w))
24	20, 23	syl5 22	. . . . . . . . . . 11 |- (((y e. z -> (g` y) = (G` (g |` y))) /\ (y e. w -> (h` y) = (G` (h |` y)))) -> (((z i^i w) e. On /\ y e. (z i^i w)) -> ((g` y) = (G` (g |` y)) /\ (h` y) = (G` (h |` y)))))
25		onelsst 2255	. . . . . . . . . . . . . 14 |- ((z i^i w) e. On -> (y e. (z i^i w) -> y (_ (z i^i w)))
26	25	impac 304	. . . . . . . . . . . . 13 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (y (_ (z i^i w) /\ y e. (z i^i w)))
27		fvres 2840	. . . . . . . . . . . . . . 15 |- (y e. (z i^i w) -> ((g |` (z i^i w))` y) = (g` y))
28		resabs1 2592	. . . . . . . . . . . . . . . 16 |- (y (_ (z i^i w) -> ((g |` (z i^i w)) |` y) = (g |` y))
29	28	fveq2d 2836	. . . . . . . . . . . . . . 15 |- (y (_ (z i^i w) -> (G` ((g |` (z i^i w)) |` y)) = (G` (g |` y)))
30	27, 29	cleqan12rd 1117	. . . . . . . . . . . . . 14 |- ((y (_ (z i^i w) /\ y e. (z i^i w)) -> (((g |` (z i^i w))` y) = (G` ((g |` (z i^i w)) |` y)) <-> (g` y) = (G` (g |` y))))
31		fvres 2840	. . . . . . . . . . . . . . 15 |- (y e. (z i^i w) -> ((h |` (z <