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