Metamath Proof Explorer


Theorem tfrlem12

Description: Lemma for transfinite recursion. Show C is an acceptable function. (Contributed by NM, 15-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 tfrlem12 recs F V C A

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 1 tfrlem8 Ord dom recs F
4 3 a1i recs F V Ord dom recs F
5 dmexg recs F V dom recs F V
6 elon2 dom recs F On Ord dom recs F dom recs F V
7 4 5 6 sylanbrc recs F V dom recs F On
8 suceloni dom recs F On suc dom recs F On
9 1 2 tfrlem10 dom recs F On C Fn suc dom recs F
10 1 2 tfrlem11 dom recs F On z suc dom recs F C z = F C z
11 10 ralrimiv dom recs F On z suc dom recs F C z = F C z
12 fveq2 z = y C z = C y
13 reseq2 z = y C z = C y
14 13 fveq2d z = y F C z = F C y
15 12 14 eqeq12d z = y C z = F C z C y = F C y
16 15 cbvralvw z suc dom recs F C z = F C z y suc dom recs F C y = F C y
17 11 16 sylib dom recs F On y suc dom recs F C y = F C y
18 fneq2 x = suc dom recs F C Fn x C Fn suc dom recs F
19 raleq x = suc dom recs F y x C y = F C y y suc dom recs F C y = F C y
20 18 19 anbi12d x = suc dom recs F C Fn x y x C y = F C y C Fn suc dom recs F y suc dom recs F C y = F C y
21 20 rspcev suc dom recs F On C Fn suc dom recs F y suc dom recs F C y = F C y x On C Fn x y x C y = F C y
22 8 9 17 21 syl12anc dom recs F On x On C Fn x y x C y = F C y
23 7 22 syl recs F V x On C Fn x y x C y = F C y
24 snex dom recs F F recs F V
25 unexg recs F V dom recs F F recs F V recs F dom recs F F recs F V
26 24 25 mpan2 recs F V recs F dom recs F F recs F V
27 2 26 eqeltrid recs F V C V
28 fneq1 f = C f Fn x C Fn x
29 fveq1 f = C f y = C y
30 reseq1 f = C f y = C y
31 30 fveq2d f = C F f y = F C y
32 29 31 eqeq12d f = C f y = F f y C y = F C y
33 32 ralbidv f = C y x f y = F f y y x C y = F C y
34 28 33 anbi12d f = C f Fn x y x f y = F f y C Fn x y x C y = F C y
35 34 rexbidv f = C x On f Fn x y x f y = F f y x On C Fn x y x C y = F C y
36 35 1 elab2g C V C A x On C Fn x y x C y = F C y
37 27 36 syl recs F V C A x On C Fn x y x C y = F C y
38 23 37 mpbird recs F V C A