Metamath Proof Explorer


Theorem wfrlem15

Description: Lemma for well-ordered recursion. When z is R minimal, C is an acceptable function. This step is where the Axiom of Replacement becomes required. (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 wfrlem15 z A dom F Pred R A dom F z = C f | x f Fn x x A y x Pred R A y x y x f y = G f 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 5 adantr z A dom F Pred R A dom F z = C Fn dom F z
7 1 3 wfrlem10 z A dom F Pred R A dom F z = Pred R A z = dom F
8 eldifi z A dom F z A
9 setlikespec z A R Se A Pred R A z V
10 8 2 9 sylancl z A dom F Pred R A z V
11 10 adantr z A dom F Pred R A dom F z = Pred R A z V
12 7 11 eqeltrrd z A dom F Pred R A dom F z = dom F V
13 snex z V
14 unexg dom F V z V dom F z V
15 13 14 mpan2 dom F V dom F z V
16 fnex C Fn dom F z dom F z V C V
17 15 16 sylan2 C Fn dom F z dom F V C V
18 6 12 17 syl2anc z A dom F Pred R A dom F z = C V
19 12 13 14 sylancl z A dom F Pred R A dom F z = dom F z V
20 3 wfrdmss dom F A
21 8 snssd z A dom F z A
22 unss dom F A z A dom F z A
23 22 biimpi dom F A z A dom F z A
24 20 21 23 sylancr z A dom F dom F z A
25 24 adantr z A dom F Pred R A dom F z = dom F z A
26 elun y dom F z y dom F y z
27 velsn y z y = z
28 27 orbi2i y dom F y z y dom F y = z
29 26 28 bitri y dom F z y dom F y = z
30 3 wfrdmcl y dom F Pred R A y dom F
31 ssun3 Pred R A y dom F Pred R A y dom F z
32 30 31 syl y dom F Pred R A y dom F z
33 32 a1i z A dom F Pred R A dom F z = y dom F Pred R A y dom F z
34 ssun1 dom F dom F z
35 7 34 eqsstrdi z A dom F Pred R A dom F z = Pred R A z dom F z
36 predeq3 y = z Pred R A y = Pred R A z
37 36 sseq1d y = z Pred R A y dom F z Pred R A z dom F z
38 35 37 syl5ibrcom z A dom F Pred R A dom F z = y = z Pred R A y dom F z
39 33 38 jaod z A dom F Pred R A dom F z = y dom F y = z Pred R A y dom F z
40 29 39 syl5bi z A dom F Pred R A dom F z = y dom F z Pred R A y dom F z
41 40 ralrimiv z A dom F Pred R A dom F z = y dom F z Pred R A y dom F z
42 25 41 jca z A dom F Pred R A dom F z = dom F z A y dom F z Pred R A y dom F z
43 1 2 3 4 wfrlem14 z A dom F y dom F z C y = G C Pred R A y
44 43 ralrimiv z A dom F y dom F z C y = G C Pred R A y
45 44 adantr z A dom F Pred R A dom F z = y dom F z C y = G C Pred R A y
46 6 42 45 3jca z A dom F Pred R A dom F z = C Fn dom F z dom F z A y dom F z Pred R A y dom F z y dom F z C y = G C Pred R A y
47 fneq2 x = dom F z C Fn x C Fn dom F z
48 sseq1 x = dom F z x A dom F z A
49 sseq2 x = dom F z Pred R A y x Pred R A y dom F z
50 49 raleqbi1dv x = dom F z y x Pred R A y x y dom F z Pred R A y dom F z
51 48 50 anbi12d x = dom F z x A y x Pred R A y x dom F z A y dom F z Pred R A y dom F z
52 raleq x = dom F z y x C y = G C Pred R A y y dom F z C y = G C Pred R A y
53 47 51 52 3anbi123d x = dom F z C Fn x x A y x Pred R A y x y x C y = G C Pred R A y C Fn dom F z dom F z A y dom F z Pred R A y dom F z y dom F z C y = G C Pred R A y
54 19 46 53 spcedv z A dom F Pred R A dom F z = x C Fn x x A y x Pred R A y x y x C y = G C Pred R A y
55 fneq1 f = C f Fn x C Fn x
56 fveq1 f = C f y = C y
57 reseq1 f = C f Pred R A y = C Pred R A y
58 57 fveq2d f = C G f Pred R A y = G C Pred R A y
59 56 58 eqeq12d f = C f y = G f Pred R A y C y = G C Pred R A y
60 59 ralbidv f = C y x f y = G f Pred R A y y x C y = G C Pred R A y
61 55 60 3anbi13d f = C f Fn x x A y x Pred R A y x y x f y = G f Pred R A y C Fn x x A y x Pred R A y x y x C y = G C Pred R A y
62 61 exbidv f = C x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y x C Fn x x A y x Pred R A y x y x C y = G C Pred R A y
63 18 54 62 elabd z A dom F Pred R A dom F z = C f | x f Fn x x A y x Pred R A y x y x f y = G f Pred R A y