HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem tfrlem5 3900
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 groups:   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
StepHypRef Expression
1 tfrlem.1 . . . . . 6 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
21tfrlem3 3898 . . . . 5 |- A = {g | E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y)))}
32abeq2i 1562 . . . 4 |- (g e. A <-> E.z e. On (g Fn z /\ A.y e. z (g` y) = (G` (g |` y))))
41tfrlem3 3898 . . . . 5 |- A = {h | E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y)))}
54abeq2i 1562 . . . 4 |- (h e. A <-> E.w e. On (h Fn w /\ A.y e. w (h` y) = (G` (h |` y))))
63, 5anbi12i 481 . . 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 1770 . . 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)))))
86, 7bitr4 176 . 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 3584 . . . . . . . . 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 3897 . . . . . . . . . 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 3587 . . . . . . . . . 10 |- (g Fn z -> (g |` (z i^i w)) Fn (z i^i w))
12 fnresin2 3588 . . . . . . . . . 10 |- (h Fn w -> (h |` (z i^i w)) Fn (z i^i w))
1310, 11, 12syl2an 454 . . . . . . . . 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))))
149, 13sylbid 203 . . . . . . . 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))))
1514com24 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))))
1615com3r 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))))
1716imp32 363 . . . . 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 2968 . . . . 5 |- ((z e. On /\ w e. On) -> (z i^i w) e. On)
19 r19.26m 1744 . . . . . . . 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 554 . . . . . . . . . . . 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 323 . . . . . . . . . . . . 13 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> y e. (z i^i w))
22 elin 2197 . . . . . . . . . . . . 13 |- (y e. (z i^i w) <-> (y e. z /\ y e. w))
2321, 22sylib 198 . . . . . . . . . . . 12 |- (((z i^i w) e. On /\ y e. (z i^i w)) -> (y e. z /\ y e. w))
2420, 23syl5 21 . . . . . . . . . . 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 2990 . . . . . . . . . . . . . 14 |- ((z i^i w) e. On -> (y e. (z i^i w) -> y (_ (z i^i w)))
2625impac 387 . . . . . . . . . . . . 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 3719 . . . . . . . . . . . . . . 15 |- (y e. (z i^i w) -> ((g |` (z i^i w))` y) = (g` y))
28 resabs1 3372 . . . . . . . . . . . . . . . 16 |- (y (_ (z i^i w) -> ((g |` (z i^i w)) |` y) = (g |` y))
2928fveq2d 3713 . . . . . . . . . . . . . . 15 |- (y (_ (z i^i w) -> (G` ((g |` (z i^i w)) |` y)) = (G` (g |` y)))
3027, 29eqeqan12rd 1483 . . . . . . . . . . . . . 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)) <-> (