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∈OnfFnx∧∀y∈xf⁡y=F⁡f↾y
tfrlem.3 ⊢C=recs⁡F∪dom⁡recs⁡FF⁡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∈OnfFnx∧∀y∈xf⁡y=F⁡f↾y
2 tfrlem.3 ⊢C=recs⁡F∪dom⁡recs⁡FF⁡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→CFnsuc⁡dom⁡recs⁡F
5 fnfun ⊢CFnsuc⁡dom⁡recs⁡F→Fun⁡C
6 4 5 syl ⊢dom⁡recs⁡F∈On→Fun⁡C
7 ssun1 ⊢recs⁡F⊆recs⁡F∪dom⁡recs⁡FF⁡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 imbitrrid ⊢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 ⊢BF⁡C↾B∈V
27 26 snid ⊢BF⁡C↾B∈BF⁡C↾B
28 opeq1 ⊢B=dom⁡recs⁡F→BF⁡C↾B=dom⁡recs⁡FF⁡C↾B
29 28 adantl ⊢dom⁡recs⁡F∈On∧B=dom⁡recs⁡F→BF⁡C↾B=dom⁡recs⁡FF⁡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⁡FF⁡C↾B=dom⁡recs⁡FF⁡recs⁡F
42 29 41 eqtrd ⊢dom⁡recs⁡F∈On∧B=dom⁡recs⁡F→BF⁡C↾B=dom⁡recs⁡FF⁡recs⁡F
43 42 sneqd ⊢dom⁡recs⁡F∈On∧B=dom⁡recs⁡F→BF⁡C↾B=dom⁡recs⁡FF⁡recs⁡F
44 27 43 eleqtrid ⊢dom⁡recs⁡F∈On∧B=dom⁡recs⁡F→BF⁡C↾B∈dom⁡recs⁡FF⁡recs⁡F
45 elun2 ⊢BF⁡C↾B∈dom⁡recs⁡FF⁡recs⁡F→BF⁡C↾B∈recs⁡F∪dom⁡recs⁡FF⁡recs⁡F
46 44 45 syl ⊢dom⁡recs⁡F∈On∧B=dom⁡recs⁡F→BF⁡C↾B∈recs⁡F∪dom⁡recs⁡FF⁡recs⁡F
47 46 2 eleqtrrdi ⊢dom⁡recs⁡F∈On∧B=dom⁡recs⁡F→BF⁡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 ⊢CFnsuc⁡dom⁡recs⁡F∧B∈suc⁡dom⁡recs⁡F→C⁡B=F⁡C↾B↔BF⁡C↾B∈C
53 4 51 52 syl2an2r ⊢dom⁡recs⁡F∈On∧B=dom⁡recs⁡F→C⁡B=F⁡C↾B↔BF⁡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