Metamath Proof Explorer

Theorem tfrlem11

Description: Lemma for transfinite recursion. Compute the value of C . (Contributed by NM, 18-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
tfrlem.3 ⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
Assertion tfrlem11 ( dom recs ( 𝐹 ) ∈ On → ( 𝐵 ∈ suc dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 tfrlem.3 ⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
3 elsuci ⊢ ( 𝐵 ∈ suc dom recs ( 𝐹 ) → ( 𝐵 ∈ dom recs ( 𝐹 ) ∨ 𝐵 = dom recs ( 𝐹 ) ) )
4 1 2 tfrlem10 ⊢ ( dom recs ( 𝐹 ) ∈ On → 𝐶 Fn suc dom recs ( 𝐹 ) )
5 fnfun ⊢ ( 𝐶 Fn suc dom recs ( 𝐹 ) → Fun 𝐶 )
6 4 5 syl ⊢ ( dom recs ( 𝐹 ) ∈ On → Fun 𝐶 )
7 ssun1 ⊢ recs ( 𝐹 ) ⊆ ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
8 7 2 sseqtrri ⊢ recs ( 𝐹 ) ⊆ 𝐶
9 1 tfrlem9 ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )
10 funssfv ⊢ ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) → ( 𝐶 ‘ 𝐵 ) = ( recs ( 𝐹 ) ‘ 𝐵 ) )
11 10 3expa ⊢ ( ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ) ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) → ( 𝐶 ‘ 𝐵 ) = ( recs ( 𝐹 ) ‘ 𝐵 ) )
12 11 adantrl ⊢ ( ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ) ∧ ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) ) → ( 𝐶 ‘ 𝐵 ) = ( recs ( 𝐹 ) ‘ 𝐵 ) )
13 onelss ⊢ ( dom recs ( 𝐹 ) ∈ On → ( 𝐵 ∈ dom recs ( 𝐹 ) → 𝐵 ⊆ dom recs ( 𝐹 ) ) )
14 13 imp ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) → 𝐵 ⊆ dom recs ( 𝐹 ) )
15 fun2ssres ⊢ ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ∧ 𝐵 ⊆ dom recs ( 𝐹 ) ) → ( 𝐶 ↾ 𝐵 ) = ( recs ( 𝐹 ) ↾ 𝐵 ) )
16 15 3expa ⊢ ( ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ) ∧ 𝐵 ⊆ dom recs ( 𝐹 ) ) → ( 𝐶 ↾ 𝐵 ) = ( recs ( 𝐹 ) ↾ 𝐵 ) )
17 16 fveq2d ⊢ ( ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ) ∧ 𝐵 ⊆ dom recs ( 𝐹 ) ) → ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )
18 14 17 sylan2 ⊢ ( ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ) ∧ ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) ) → ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )
19 12 18 eqeq12d ⊢ ( ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ) ∧ ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) ) → ( ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ↔ ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) )
20 9 19 imbitrrid ⊢ ( ( ( Fun 𝐶 ∧ recs ( 𝐹 ) ⊆ 𝐶 ) ∧ ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) ) → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )
21 8 20 mpanl2 ⊢ ( ( Fun 𝐶 ∧ ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) ) → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )
22 6 21 sylan ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 ∈ dom recs ( 𝐹 ) ) ) → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )
23 22 exp32 ⊢ ( dom recs ( 𝐹 ) ∈ On → ( dom recs ( 𝐹 ) ∈ On → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) ) ) )
24 23 pm2.43i ⊢ ( dom recs ( 𝐹 ) ∈ On → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) ) )
25 24 pm2.43d ⊢ ( dom recs ( 𝐹 ) ∈ On → ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )
26 opex ⊢ ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ V
27 26 snid ⊢ ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ { ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ }
28 opeq1 ⊢ ( 𝐵 = dom recs ( 𝐹 ) → ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ = ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ )
29 28 adantl ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ = ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ )
30 eqimss ⊢ ( 𝐵 = dom recs ( 𝐹 ) → 𝐵 ⊆ dom recs ( 𝐹 ) )
31 8 15 mp3an2 ⊢ ( ( Fun 𝐶 ∧ 𝐵 ⊆ dom recs ( 𝐹 ) ) → ( 𝐶 ↾ 𝐵 ) = ( recs ( 𝐹 ) ↾ 𝐵 ) )
32 6 30 31 syl2an ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ( 𝐶 ↾ 𝐵 ) = ( recs ( 𝐹 ) ↾ 𝐵 ) )
33 reseq2 ⊢ ( 𝐵 = dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝐵 ) = ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) )
34 1 tfrlem6 ⊢ Rel recs ( 𝐹 )
35 resdm ⊢ ( Rel recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 ) )
36 34 35 ax-mp ⊢ ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 )
37 33 36 eqtrdi ⊢ ( 𝐵 = dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝐵 ) = recs ( 𝐹 ) )
38 37 adantl ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ( recs ( 𝐹 ) ↾ 𝐵 ) = recs ( 𝐹 ) )
39 32 38 eqtrd ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ( 𝐶 ↾ 𝐵 ) = recs ( 𝐹 ) )
40 39 fveq2d ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) = ( 𝐹 ‘ recs ( 𝐹 ) ) )
41 40 opeq2d ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ = ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ )
42 29 41 eqtrd ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ = ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ )
43 42 sneqd ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → { ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ } = { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
44 27 43 eleqtrid ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
45 elun2 ⊢ ( ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } → ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
46 44 45 syl ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
47 46 2 eleqtrrdi ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ 𝐶 )
48 simpr ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → 𝐵 = dom recs ( 𝐹 ) )
49 sucidg ⊢ ( dom recs ( 𝐹 ) ∈ On → dom recs ( 𝐹 ) ∈ suc dom recs ( 𝐹 ) )
50 49 adantr ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → dom recs ( 𝐹 ) ∈ suc dom recs ( 𝐹 ) )
51 48 50 eqeltrd ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → 𝐵 ∈ suc dom recs ( 𝐹 ) )
52 fnopfvb ⊢ ( ( 𝐶 Fn suc dom recs ( 𝐹 ) ∧ 𝐵 ∈ suc dom recs ( 𝐹 ) ) → ( ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ↔ ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ 𝐶 ) )
53 4 51 52 syl2an2r ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ( ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ↔ ⟨ 𝐵 , ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ⟩ ∈ 𝐶 ) )
54 47 53 mpbird ⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ 𝐵 = dom recs ( 𝐹 ) ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) )
55 54 ex ⊢ ( dom recs ( 𝐹 ) ∈ On → ( 𝐵 = dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )
56 25 55 jaod ⊢ ( dom recs ( 𝐹 ) ∈ On → ( ( 𝐵 ∈ dom recs ( 𝐹 ) ∨ 𝐵 = dom recs ( 𝐹 ) ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )
57 3 56 syl5 ⊢ ( dom recs ( 𝐹 ) ∈ On → ( 𝐵 ∈ suc dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝐵 ) ) ) )