# Metamath Proof Explorer

## Theorem tfrlem5

Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 24-May-2019)

Ref Expression
Hypothesis tfrlem.1 ${⊢}{A}=\left\{{f}|\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={F}\left({{f}↾}_{{y}}\right)\right)\right\}$
Assertion tfrlem5 ${⊢}\left({g}\in {A}\wedge {h}\in {A}\right)\to \left(\left({x}{g}{u}\wedge {x}{h}{v}\right)\to {u}={v}\right)$

### Proof

Step Hyp Ref Expression
1 tfrlem.1 ${⊢}{A}=\left\{{f}|\exists {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({f}Fn{x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)={F}\left({{f}↾}_{{y}}\right)\right)\right\}$
2 vex ${⊢}{g}\in \mathrm{V}$
3 1 2 tfrlem3a ${⊢}{g}\in {A}↔\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)$
4 vex ${⊢}{h}\in \mathrm{V}$
5 1 4 tfrlem3a ${⊢}{h}\in {A}↔\exists {w}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)$
6 reeanv ${⊢}\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)↔\left(\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \exists {w}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)$
7 fveq2 ${⊢}{a}={x}\to {g}\left({a}\right)={g}\left({x}\right)$
8 fveq2 ${⊢}{a}={x}\to {h}\left({a}\right)={h}\left({x}\right)$
9 7 8 eqeq12d ${⊢}{a}={x}\to \left({g}\left({a}\right)={h}\left({a}\right)↔{g}\left({x}\right)={h}\left({x}\right)\right)$
10 onin ${⊢}\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\to {z}\cap {w}\in \mathrm{On}$
11 10 3ad2ant1 ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {z}\cap {w}\in \mathrm{On}$
12 simp2ll ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {g}Fn{z}$
13 fnfun ${⊢}{g}Fn{z}\to \mathrm{Fun}{g}$
14 12 13 syl ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \mathrm{Fun}{g}$
15 inss1 ${⊢}{z}\cap {w}\subseteq {z}$
16 12 fndmd ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \mathrm{dom}{g}={z}$
17 15 16 sseqtrrid ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {z}\cap {w}\subseteq \mathrm{dom}{g}$
18 14 17 jca ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \left(\mathrm{Fun}{g}\wedge {z}\cap {w}\subseteq \mathrm{dom}{g}\right)$
19 simp2rl ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {h}Fn{w}$
20 fnfun ${⊢}{h}Fn{w}\to \mathrm{Fun}{h}$
21 19 20 syl ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \mathrm{Fun}{h}$
22 inss2 ${⊢}{z}\cap {w}\subseteq {w}$
23 19 fndmd ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \mathrm{dom}{h}={w}$
24 22 23 sseqtrrid ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {z}\cap {w}\subseteq \mathrm{dom}{h}$
25 21 24 jca ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \left(\mathrm{Fun}{h}\wedge {z}\cap {w}\subseteq \mathrm{dom}{h}\right)$
26 simp2lr ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)$
27 ssralv ${⊢}{z}\cap {w}\subseteq {z}\to \left(\forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\to \forall {a}\in \left({z}\cap {w}\right)\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)$
28 15 26 27 mpsyl ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \forall {a}\in \left({z}\cap {w}\right)\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)$
29 simp2rr ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)$
30 ssralv ${⊢}{z}\cap {w}\subseteq {w}\to \left(\forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\to \forall {a}\in \left({z}\cap {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)$
31 22 29 30 mpsyl ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \forall {a}\in \left({z}\cap {w}\right)\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)$
32 11 18 25 28 31 tfrlem1 ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to \forall {a}\in \left({z}\cap {w}\right)\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={h}\left({a}\right)$
33 simp3l ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {x}{g}{u}$
34 fnbr ${⊢}\left({g}Fn{z}\wedge {x}{g}{u}\right)\to {x}\in {z}$
35 12 33 34 syl2anc ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {x}\in {z}$
36 simp3r ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {x}{h}{v}$
37 fnbr ${⊢}\left({h}Fn{w}\wedge {x}{h}{v}\right)\to {x}\in {w}$
38 19 36 37 syl2anc ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {x}\in {w}$
39 35 38 elind ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {x}\in \left({z}\cap {w}\right)$
40 9 32 39 rspcdva ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {g}\left({x}\right)={h}\left({x}\right)$
41 funbrfv ${⊢}\mathrm{Fun}{g}\to \left({x}{g}{u}\to {g}\left({x}\right)={u}\right)$
42 14 33 41 sylc ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {g}\left({x}\right)={u}$
43 funbrfv ${⊢}\mathrm{Fun}{h}\to \left({x}{h}{v}\to {h}\left({x}\right)={v}\right)$
44 21 36 43 sylc ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {h}\left({x}\right)={v}$
45 40 42 44 3eqtr3d ${⊢}\left(\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\wedge \left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\wedge \left({x}{g}{u}\wedge {x}{h}{v}\right)\right)\to {u}={v}$
46 45 3exp ${⊢}\left({z}\in \mathrm{On}\wedge {w}\in \mathrm{On}\right)\to \left(\left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\to \left(\left({x}{g}{u}\wedge {x}{h}{v}\right)\to {u}={v}\right)\right)$
47 46 rexlimivv ${⊢}\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\exists {w}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left(\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\to \left(\left({x}{g}{u}\wedge {x}{h}{v}\right)\to {u}={v}\right)$
48 6 47 sylbir ${⊢}\left(\exists {z}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({g}Fn{z}\wedge \forall {a}\in {z}\phantom{\rule{.4em}{0ex}}{g}\left({a}\right)={F}\left({{g}↾}_{{a}}\right)\right)\wedge \exists {w}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({h}Fn{w}\wedge \forall {a}\in {w}\phantom{\rule{.4em}{0ex}}{h}\left({a}\right)={F}\left({{h}↾}_{{a}}\right)\right)\right)\to \left(\left({x}{g}{u}\wedge {x}{h}{v}\right)\to {u}={v}\right)$
49 3 5 48 syl2anb ${⊢}\left({g}\in {A}\wedge {h}\in {A}\right)\to \left(\left({x}{g}{u}\wedge {x}{h}{v}\right)\to {u}={v}\right)$