Metamath Proof Explorer


Theorem wfrlem14

Description: Lemma for well-ordered recursion. Compute the value of C . (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem13.1 R We A
wfrlem13.2 R Se A
wfrlem13.3 F = wrecs R A G
wfrlem13.4 C = F z G F Pred R A z
Assertion wfrlem14 z A dom F y dom F z C y = G C Pred R A y

Proof

Step Hyp Ref Expression
1 wfrlem13.1 R We A
2 wfrlem13.2 R Se A
3 wfrlem13.3 F = wrecs R A G
4 wfrlem13.4 C = F z G F Pred R A z
5 1 2 3 4 wfrlem13 z A dom F C Fn dom F z
6 elun y dom F z y dom F y z
7 velsn y z y = z
8 7 orbi2i y dom F y z y dom F y = z
9 6 8 bitri y dom F z y dom F y = z
10 1 2 3 wfrlem12 y dom F F y = G F Pred R A y
11 fnfun C Fn dom F z Fun C
12 ssun1 F F z G F Pred R A z
13 12 4 sseqtrri F C
14 funssfv Fun C F C y dom F C y = F y
15 3 wfrdmcl y dom F Pred R A y dom F
16 fun2ssres Fun C F C Pred R A y dom F C Pred R A y = F Pred R A y
17 15 16 syl3an3 Fun C F C y dom F C Pred R A y = F Pred R A y
18 17 fveq2d Fun C F C y dom F G C Pred R A y = G F Pred R A y
19 14 18 eqeq12d Fun C F C y dom F C y = G C Pred R A y F y = G F Pred R A y
20 13 19 mp3an2 Fun C y dom F C y = G C Pred R A y F y = G F Pred R A y
21 11 20 sylan C Fn dom F z y dom F C y = G C Pred R A y F y = G F Pred R A y
22 10 21 syl5ibr C Fn dom F z y dom F y dom F C y = G C Pred R A y
23 22 ex C Fn dom F z y dom F y dom F C y = G C Pred R A y
24 23 pm2.43d C Fn dom F z y dom F C y = G C Pred R A y
25 vsnid z z
26 elun2 z z z dom F z
27 25 26 ax-mp z dom F z
28 4 reseq1i C Pred R A z = F z G F Pred R A z Pred R A z
29 resundir F z G F Pred R A z Pred R A z = F Pred R A z z G F Pred R A z Pred R A z
30 wefr R We A R Fr A
31 1 30 ax-mp R Fr A
32 predfrirr R Fr A ¬ z Pred R A z
33 ressnop0 ¬ z Pred R A z z G F Pred R A z Pred R A z =
34 31 32 33 mp2b z G F Pred R A z Pred R A z =
35 34 uneq2i F Pred R A z z G F Pred R A z Pred R A z = F Pred R A z
36 un0 F Pred R A z = F Pred R A z
37 35 36 eqtri F Pred R A z z G F Pred R A z Pred R A z = F Pred R A z
38 28 29 37 3eqtri C Pred R A z = F Pred R A z
39 38 fveq2i G C Pred R A z = G F Pred R A z
40 39 opeq2i z G C Pred R A z = z G F Pred R A z
41 opex z G C Pred R A z V
42 41 elsn z G C Pred R A z z G F Pred R A z z G C Pred R A z = z G F Pred R A z
43 40 42 mpbir z G C Pred R A z z G F Pred R A z
44 elun2 z G C Pred R A z z G F Pred R A z z G C Pred R A z F z G F Pred R A z
45 43 44 ax-mp z G C Pred R A z F z G F Pred R A z
46 45 4 eleqtrri z G C Pred R A z C
47 fnopfvb C Fn dom F z z dom F z C z = G C Pred R A z z G C Pred R A z C
48 46 47 mpbiri C Fn dom F z z dom F z C z = G C Pred R A z
49 27 48 mpan2 C Fn dom F z C z = G C Pred R A z
50 fveq2 y = z C y = C z
51 predeq3 y = z Pred R A y = Pred R A z
52 51 reseq2d y = z C Pred R A y = C Pred R A z
53 52 fveq2d y = z G C Pred R A y = G C Pred R A z
54 50 53 eqeq12d y = z C y = G C Pred R A y C z = G C Pred R A z
55 49 54 syl5ibrcom C Fn dom F z y = z C y = G C Pred R A y
56 24 55 jaod C Fn dom F z y dom F y = z C y = G C Pred R A y
57 9 56 syl5bi C Fn dom F z y dom F z C y = G C Pred R A y
58 5 57 syl z A dom F y dom F z C y = G C Pred R A y