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 ⊢ 𝐹 = recs ( 𝐺 )
Assertion tfr3 ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → 𝐵 = 𝐹 )

Proof

Step Hyp Ref Expression
1 tfr.1 ⊢ 𝐹 = recs ( 𝐺 )
2 nfv ⊢ Ⅎ 𝑥 𝐵 Fn On
3 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) )
4 2 3 nfan ⊢ Ⅎ 𝑥 ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) )
5 nfv ⊢ Ⅎ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 )
6 4 5 nfim ⊢ Ⅎ 𝑥 ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
7 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑦 ) )
8 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) )
10 9 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
11 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) )
12 rsp ⊢ ( ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) → ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) )
13 onss ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
14 1 tfr1 ⊢ 𝐹 Fn On
15 fvreseq ⊢ ( ( ( 𝐵 Fn On ∧ 𝐹 Fn On ) ∧ 𝑥 ⊆ On ) → ( ( 𝐵 ↾ 𝑥 ) = ( 𝐹 ↾ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) )
16 14 15 mpanl2 ⊢ ( ( 𝐵 Fn On ∧ 𝑥 ⊆ On ) → ( ( 𝐵 ↾ 𝑥 ) = ( 𝐹 ↾ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) )
17 fveq2 ⊢ ( ( 𝐵 ↾ 𝑥 ) = ( 𝐹 ↾ 𝑥 ) → ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) )
18 16 17 syl6bir ⊢ ( ( 𝐵 Fn On ∧ 𝑥 ⊆ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
19 13 18 sylan2 ⊢ ( ( 𝐵 Fn On ∧ 𝑥 ∈ On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
20 19 ancoms ⊢ ( ( 𝑥 ∈ On ∧ 𝐵 Fn On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
21 20 imp ⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 Fn On ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) )
22 21 adantr ⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝐵 Fn On ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) ∧ 𝑥 ∈ On ) ) → ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) )
23 1 tfr2 ⊢ ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) )
24 23 jctr ⊢ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) ∧ ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) )
25 jcab ⊢ ( ( 𝑥 ∈ On → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) ↔ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) ∧ ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) )
26 24 25 sylibr ⊢ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) )
27 eqeq12 ⊢ ( ( ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
28 26 27 syl6 ⊢ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) )
29 28 imp ⊢ ( ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) ∧ 𝑥 ∈ On ) → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
30 29 adantl ⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝐵 Fn On ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) ∧ 𝑥 ∈ On ) ) → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) = ( 𝐺 ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
31 22 30 mpbird ⊢ ( ( ( ( 𝑥 ∈ On ∧ 𝐵 Fn On ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) ∧ 𝑥 ∈ On ) ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
32 31 exp43 ⊢ ( ( 𝑥 ∈ On ∧ 𝐵 Fn On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) )
33 32 com4t ⊢ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( ( 𝑥 ∈ On ∧ 𝐵 Fn On ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) )
34 33 exp4a ⊢ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( 𝑥 ∈ On → ( 𝐵 Fn On → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
35 34 pm2.43d ⊢ ( ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( 𝐵 Fn On → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) )
36 12 35 syl ⊢ ( ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) → ( 𝑥 ∈ On → ( 𝐵 Fn On → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) )
37 36 com3l ⊢ ( 𝑥 ∈ On → ( 𝐵 Fn On → ( ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) )
38 37 impd ⊢ ( 𝑥 ∈ On → ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
39 38 a2d ⊢ ( 𝑥 ∈ On → ( ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
40 11 39 syl5bi ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
41 6 10 40 tfis2f ⊢ ( 𝑥 ∈ On → ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
42 41 com12 ⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ( 𝑥 ∈ On → ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
43 4 42 ralrimi ⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
44 eqfnfv ⊢ ( ( 𝐵 Fn On ∧ 𝐹 Fn On ) → ( 𝐵 = 𝐹 ↔ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
45 14 44 mpan2 ⊢ ( 𝐵 Fn On → ( 𝐵 = 𝐹 ↔ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) )
46 45 biimpar ⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐵 = 𝐹 )
47 43 46 syldan ⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → 𝐵 = 𝐹 )