Metamath Proof Explorer


Theorem exrecfnlem

Description: Lemma for exrecfn . (Contributed by ML, 30-Mar-2022)

Ref Expression
Hypothesis exrecfnlem.1 F = z V z ran y z B
Assertion exrecfnlem A V y B W x A x y x B x

Proof

Step Hyp Ref Expression
1 exrecfnlem.1 F = z V z ran y z B
2 rdg0g A V rec F A = A
3 peano1 ω
4 omelon ω On
5 limom Lim ω
6 rdglimss ω On Lim ω ω rec F A rec F A ω
7 4 5 6 mpanl12 ω rec F A rec F A ω
8 3 7 ax-mp rec F A rec F A ω
9 2 8 eqsstrrdi A V A rec F A ω
10 rdglim2a ω On Lim ω rec F A ω = u ω rec F A u
11 4 5 10 mp2an rec F A ω = u ω rec F A u
12 11 eleq2i y rec F A ω y u ω rec F A u
13 eliun y u ω rec F A u u ω y rec F A u
14 12 13 bitri y rec F A ω u ω y rec F A u
15 peano2 u ω suc u ω
16 nnon u ω u On
17 eqid y rec F A u B = y rec F A u B
18 17 elrnmpt1 y rec F A u B W B ran y rec F A u B
19 elun2 B ran y rec F A u B B rec F A u ran y rec F A u B
20 18 19 syl y rec F A u B W B rec F A u ran y rec F A u B
21 fvex rec F A u V
22 nfcv _ y V
23 nfcv _ y z
24 nfmpt1 _ y y z B
25 24 nfrn _ y ran y z B
26 23 25 nfun _ y z ran y z B
27 22 26 nfmpt _ y z V z ran y z B
28 1 27 nfcxfr _ y F
29 nfcv _ y A
30 28 29 nfrdg _ y rec F A
31 nfcv _ y u
32 30 31 nffv _ y rec F A u
33 32 mptexgf rec F A u V y rec F A u B V
34 21 33 ax-mp y rec F A u B V
35 34 rnex ran y rec F A u B V
36 21 35 unex rec F A u ran y rec F A u B V
37 nfcv _ z A
38 nfcv _ z u
39 nfmpt1 _ z z V z ran y z B
40 1 39 nfcxfr _ z F
41 40 37 nfrdg _ z rec F A
42 41 38 nffv _ z rec F A u
43 nfcv _ z B
44 42 43 nfmpt _ z y rec F A u B
45 44 nfrn _ z ran y rec F A u B
46 42 45 nfun _ z rec F A u ran y rec F A u B
47 rdgeq1 F = z V z ran y z B rec F A = rec z V z ran y z B A
48 1 47 ax-mp rec F A = rec z V z ran y z B A
49 id z = rec F A u z = rec F A u
50 32 nfeq2 y z = rec F A u
51 eqidd z = rec F A u B = B
52 50 49 51 mpteq12df z = rec F A u y z B = y rec F A u B
53 52 rneqd z = rec F A u ran y z B = ran y rec F A u B
54 49 53 uneq12d z = rec F A u z ran y z B = rec F A u ran y rec F A u B
55 37 38 46 48 54 rdgsucmptf u On rec F A u ran y rec F A u B V rec F A suc u = rec F A u ran y rec F A u B
56 36 55 mpan2 u On rec F A suc u = rec F A u ran y rec F A u B
57 56 eleq2d u On B rec F A suc u B rec F A u ran y rec F A u B
58 20 57 syl5ibr u On y rec F A u B W B rec F A suc u
59 16 58 syl u ω y rec F A u B W B rec F A suc u
60 rdgellim ω On Lim ω suc u ω B rec F A suc u B rec F A ω
61 4 5 60 mpanl12 suc u ω B rec F A suc u B rec F A ω
62 15 59 61 sylsyld u ω y rec F A u B W B rec F A ω
63 62 expd u ω y rec F A u B W B rec F A ω
64 63 com3r B W u ω y rec F A u B rec F A ω
65 64 rexlimdv B W u ω y rec F A u B rec F A ω
66 14 65 syl5bi B W y rec F A ω B rec F A ω
67 66 alimi y B W y y rec F A ω B rec F A ω
68 df-ral y rec F A ω B rec F A ω y y rec F A ω B rec F A ω
69 67 68 sylibr y B W y rec F A ω B rec F A ω
70 fvex rec F A ω V
71 sseq2 x = rec F A ω A x A rec F A ω
72 nfcv _ y ω
73 30 72 nffv _ y rec F A ω
74 73 nfeq2 y x = rec F A ω
75 eleq2 x = rec F A ω y x y rec F A ω
76 eleq2 x = rec F A ω B x B rec F A ω
77 75 76 imbi12d x = rec F A ω y x B x y rec F A ω B rec F A ω
78 74 77 albid x = rec F A ω y y x B x y y rec F A ω B rec F A ω
79 df-ral y x B x y y x B x
80 78 79 68 3bitr4g x = rec F A ω y x B x y rec F A ω B rec F A ω
81 71 80 anbi12d x = rec F A ω A x y x B x A rec F A ω y rec F A ω B rec F A ω
82 70 81 spcev A rec F A ω y rec F A ω B rec F A ω x A x y x B x
83 9 69 82 syl2an A V y B W x A x y x B x