Metamath Proof Explorer


Theorem unblem2

Description: Lemma for unbnn . The value of the function F belongs to the unbounded set of natural numbers A . (Contributed by NM, 3-Dec-2003)

Ref Expression
Hypothesis unblem.2 F = rec x V A suc x A ω
Assertion unblem2 A ω w ω v A w v z ω F z A

Proof

Step Hyp Ref Expression
1 unblem.2 F = rec x V A suc x A ω
2 fveq2 z = F z = F
3 2 eleq1d z = F z A F A
4 fveq2 z = u F z = F u
5 4 eleq1d z = u F z A F u A
6 fveq2 z = suc u F z = F suc u
7 6 eleq1d z = suc u F z A F suc u A
8 omsson ω On
9 sstr A ω ω On A On
10 8 9 mpan2 A ω A On
11 peano1 ω
12 eleq1 w = w v v
13 12 rexbidv w = v A w v v A v
14 13 rspcv ω w ω v A w v v A v
15 11 14 ax-mp w ω v A w v v A v
16 df-rex v A v v v A v
17 15 16 sylib w ω v A w v v v A v
18 exsimpl v v A v v v A
19 17 18 syl w ω v A w v v v A
20 n0 A v v A
21 19 20 sylibr w ω v A w v A
22 onint A On A A A
23 10 21 22 syl2an A ω w ω v A w v A A
24 1 fveq1i F = rec x V A suc x A ω
25 fr0g A A rec x V A suc x A ω = A
26 24 25 eqtr2id A A A = F
27 26 eleq1d A A A A F A
28 27 ibi A A F A
29 23 28 syl A ω w ω v A w v F A
30 unblem1 A ω w ω v A w v F u A A suc F u A
31 suceq y = x suc y = suc x
32 31 difeq2d y = x A suc y = A suc x
33 32 inteqd y = x A suc y = A suc x
34 suceq y = F u suc y = suc F u
35 34 difeq2d y = F u A suc y = A suc F u
36 35 inteqd y = F u A suc y = A suc F u
37 1 33 36 frsucmpt2 u ω A suc F u A F suc u = A suc F u
38 37 eqcomd u ω A suc F u A A suc F u = F suc u
39 38 eleq1d u ω A suc F u A A suc F u A F suc u A
40 39 ex u ω A suc F u A A suc F u A F suc u A
41 40 ibd u ω A suc F u A F suc u A
42 30 41 syl5 u ω A ω w ω v A w v F u A F suc u A
43 42 expd u ω A ω w ω v A w v F u A F suc u A
44 3 5 7 29 43 finds2 z ω A ω w ω v A w v F z A
45 44 com12 A ω w ω v A w v z ω F z A