# Metamath Proof Explorer

## Theorem tfr3

Description: Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of TakeutiZaring p. 47. Finally, we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F . (Contributed by NM, 18-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypothesis tfr.1 ${⊢}{F}=\mathrm{recs}\left({G}\right)$
Assertion tfr3 ${⊢}\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}={F}$

### Proof

Step Hyp Ref Expression
1 tfr.1 ${⊢}{F}=\mathrm{recs}\left({G}\right)$
2 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{B}Fn\mathrm{On}$
3 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)$
4 2 3 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)$
5 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)$
6 4 5 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({y}\right)={F}\left({y}\right)\right)$
7 fveq2 ${⊢}{x}={y}\to {B}\left({x}\right)={B}\left({y}\right)$
8 fveq2 ${⊢}{x}={y}\to {F}\left({x}\right)={F}\left({y}\right)$
9 7 8 eqeq12d ${⊢}{x}={y}\to \left({B}\left({x}\right)={F}\left({x}\right)↔{B}\left({y}\right)={F}\left({y}\right)\right)$
10 9 imbi2d ${⊢}{x}={y}\to \left(\left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)↔\left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({y}\right)={F}\left({y}\right)\right)\right)$
11 r19.21v ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({y}\right)={F}\left({y}\right)\right)↔\left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)$
12 rsp ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\to \left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)$
13 onss ${⊢}{x}\in \mathrm{On}\to {x}\subseteq \mathrm{On}$
14 1 tfr1 ${⊢}{F}Fn\mathrm{On}$
15 fvreseq ${⊢}\left(\left({B}Fn\mathrm{On}\wedge {F}Fn\mathrm{On}\right)\wedge {x}\subseteq \mathrm{On}\right)\to \left({{B}↾}_{{x}}={{F}↾}_{{x}}↔\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)$
16 14 15 mpanl2 ${⊢}\left({B}Fn\mathrm{On}\wedge {x}\subseteq \mathrm{On}\right)\to \left({{B}↾}_{{x}}={{F}↾}_{{x}}↔\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)$
17 fveq2 ${⊢}{{B}↾}_{{x}}={{F}↾}_{{x}}\to {G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)$
18 16 17 syl6bir ${⊢}\left({B}Fn\mathrm{On}\wedge {x}\subseteq \mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)\right)$
19 13 18 sylan2 ${⊢}\left({B}Fn\mathrm{On}\wedge {x}\in \mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)\right)$
20 19 ancoms ${⊢}\left({x}\in \mathrm{On}\wedge {B}Fn\mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)\right)$
21 20 imp ${⊢}\left(\left({x}\in \mathrm{On}\wedge {B}Fn\mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)\to {G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)$
22 21 adantr ${⊢}\left(\left(\left({x}\in \mathrm{On}\wedge {B}Fn\mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)\wedge \left(\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\wedge {x}\in \mathrm{On}\right)\right)\to {G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)$
23 1 tfr2 ${⊢}{x}\in \mathrm{On}\to {F}\left({x}\right)={G}\left({{F}↾}_{{x}}\right)$
24 23 jctr ${⊢}\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left(\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\wedge \left({x}\in \mathrm{On}\to {F}\left({x}\right)={G}\left({{F}↾}_{{x}}\right)\right)\right)$
25 jcab ${⊢}\left({x}\in \mathrm{On}\to \left({B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\wedge {F}\left({x}\right)={G}\left({{F}↾}_{{x}}\right)\right)\right)↔\left(\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\wedge \left({x}\in \mathrm{On}\to {F}\left({x}\right)={G}\left({{F}↾}_{{x}}\right)\right)\right)$
26 24 25 sylibr ${⊢}\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left({x}\in \mathrm{On}\to \left({B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\wedge {F}\left({x}\right)={G}\left({{F}↾}_{{x}}\right)\right)\right)$
27 eqeq12 ${⊢}\left({B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\wedge {F}\left({x}\right)={G}\left({{F}↾}_{{x}}\right)\right)\to \left({B}\left({x}\right)={F}\left({x}\right)↔{G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)\right)$
28 26 27 syl6 ${⊢}\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left({x}\in \mathrm{On}\to \left({B}\left({x}\right)={F}\left({x}\right)↔{G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)\right)\right)$
29 28 imp ${⊢}\left(\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\wedge {x}\in \mathrm{On}\right)\to \left({B}\left({x}\right)={F}\left({x}\right)↔{G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)\right)$
30 29 adantl ${⊢}\left(\left(\left({x}\in \mathrm{On}\wedge {B}Fn\mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)\wedge \left(\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\wedge {x}\in \mathrm{On}\right)\right)\to \left({B}\left({x}\right)={F}\left({x}\right)↔{G}\left({{B}↾}_{{x}}\right)={G}\left({{F}↾}_{{x}}\right)\right)$
31 22 30 mpbird ${⊢}\left(\left(\left({x}\in \mathrm{On}\wedge {B}Fn\mathrm{On}\right)\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)\wedge \left(\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\wedge {x}\in \mathrm{On}\right)\right)\to {B}\left({x}\right)={F}\left({x}\right)$
32 31 exp43 ${⊢}\left({x}\in \mathrm{On}\wedge {B}Fn\mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to \left(\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left({x}\in \mathrm{On}\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)\right)$
33 32 com4t ${⊢}\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left({x}\in \mathrm{On}\to \left(\left({x}\in \mathrm{On}\wedge {B}Fn\mathrm{On}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)\right)$
34 33 exp4a ${⊢}\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left({x}\in \mathrm{On}\to \left({x}\in \mathrm{On}\to \left({B}Fn\mathrm{On}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)\right)\right)$
35 34 pm2.43d ${⊢}\left({x}\in \mathrm{On}\to {B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left({x}\in \mathrm{On}\to \left({B}Fn\mathrm{On}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)\right)$
36 12 35 syl ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\to \left({x}\in \mathrm{On}\to \left({B}Fn\mathrm{On}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)\right)$
37 36 com3l ${⊢}{x}\in \mathrm{On}\to \left({B}Fn\mathrm{On}\to \left(\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)\right)$
38 37 impd ${⊢}{x}\in \mathrm{On}\to \left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)$
39 38 a2d ${⊢}{x}\in \mathrm{On}\to \left(\left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}{B}\left({y}\right)={F}\left({y}\right)\right)\to \left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)$
40 11 39 syl5bi ${⊢}{x}\in \mathrm{On}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({y}\right)={F}\left({y}\right)\right)\to \left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)\right)$
41 6 10 40 tfis2f ${⊢}{x}\in \mathrm{On}\to \left(\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}\left({x}\right)={F}\left({x}\right)\right)$
42 41 com12 ${⊢}\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \left({x}\in \mathrm{On}\to {B}\left({x}\right)={F}\left({x}\right)\right)$
43 4 42 ralrimi ${⊢}\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={F}\left({x}\right)$
44 eqfnfv ${⊢}\left({B}Fn\mathrm{On}\wedge {F}Fn\mathrm{On}\right)\to \left({B}={F}↔\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={F}\left({x}\right)\right)$
45 14 44 mpan2 ${⊢}{B}Fn\mathrm{On}\to \left({B}={F}↔\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={F}\left({x}\right)\right)$
46 45 biimpar ${⊢}\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={F}\left({x}\right)\right)\to {B}={F}$
47 43 46 syldan ${⊢}\left({B}Fn\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}{B}\left({x}\right)={G}\left({{B}↾}_{{x}}\right)\right)\to {B}={F}$