How to prove Y Y = Y (Y(Y))

Question

I found a prove online, but I can not fully understand it. The prove is like this:

• let Y = lambda y . (lambda x . y (x x)) (lambda x . y (x x))

• Y Y

• Expand the first Y:

  (lambda y . (lambda x . y (x x)) (lambda x . y (x x))) Y

• beta:

  (lambda x . Y (x x)) (lambda x. Y (x x))

• Alpha[x/z] the second lambda:

  (lambda x . Y (x x)) (lambda z. Y (z z))

• Beta:

  Y ((lambda z. Y (z z)) (lambda z. Y (z z)))

• Expand that Y in front and alpha[y/a][x/b]:

  (lambda a . (lambda b . a (b b)) (lambda b . a (b b))) ((lambda z. Y (z z)) (lambda z. Y (z z)))

• Beta:

  (lambda b . ((lambda z. Y (z z)) (lambda z. Y (z z))) (b b)) (lambda b . ((lambda z. Y (z z)) (lambda z. Y (z z))) (b b))

• Y (Y (Y))

What I do not understand is the last step. Since Y is

lambda y . (lambda x . y (x x)) (lambda x . y (x x))

why

(lambda b . ((lambda z. Y (z z)) (lambda z. Y (z z))) (b b)) (lambda b . ((lambda z. Y (z z)) (lambda z. Y (z z))) (b b))

is

Y (Y (Y))?

Answer 1

Using the fixed-point property that $$Y f= f (Y f)$$ for all terms $f$, one can take $f=Y$ to obtain $$Y Y = Y (Y Y ).$$