Step |
Hyp |
Ref |
Expression |
0 |
|
chli |
|- ~~>v |
1 |
|
vf |
|- f |
2 |
|
vw |
|- w |
3 |
1
|
cv |
|- f |
4 |
|
cn |
|- NN |
5 |
|
chba |
|- ~H |
6 |
4 5 3
|
wf |
|- f : NN --> ~H |
7 |
2
|
cv |
|- w |
8 |
7 5
|
wcel |
|- w e. ~H |
9 |
6 8
|
wa |
|- ( f : NN --> ~H /\ w e. ~H ) |
10 |
|
vx |
|- x |
11 |
|
crp |
|- RR+ |
12 |
|
vy |
|- y |
13 |
|
vz |
|- z |
14 |
|
cuz |
|- ZZ>= |
15 |
12
|
cv |
|- y |
16 |
15 14
|
cfv |
|- ( ZZ>= ` y ) |
17 |
|
cno |
|- normh |
18 |
13
|
cv |
|- z |
19 |
18 3
|
cfv |
|- ( f ` z ) |
20 |
|
cmv |
|- -h |
21 |
19 7 20
|
co |
|- ( ( f ` z ) -h w ) |
22 |
21 17
|
cfv |
|- ( normh ` ( ( f ` z ) -h w ) ) |
23 |
|
clt |
|- < |
24 |
10
|
cv |
|- x |
25 |
22 24 23
|
wbr |
|- ( normh ` ( ( f ` z ) -h w ) ) < x |
26 |
25 13 16
|
wral |
|- A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x |
27 |
26 12 4
|
wrex |
|- E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x |
28 |
27 10 11
|
wral |
|- A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x |
29 |
9 28
|
wa |
|- ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) |
30 |
29 1 2
|
copab |
|- { <. f , w >. | ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) } |
31 |
0 30
|
wceq |
|- ~~>v = { <. f , w >. | ( ( f : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` z ) -h w ) ) < x ) } |