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 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
tfrlem.3 ⊢ C = recs ⁡ F ∪ dom ⁡ recs ⁡ F F ⁡ recs ⁡ F
Assertion tfrlem11 ⊢ dom ⁡ recs ⁡ F ∈ On → B ∈ suc ⁡ dom ⁡ recs ⁡ F → C ⁡ B = F ⁡ C ↾ B

Proof

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