Completing the proof using strong induction for $E = \bigcap_{n=1}^\infty E_n $

Your inductive step, or maybe your proof as a whole, can perhaps be simplified by one of the following two viewpoints:

1. A dynamical viewpoint

Consider the 10-tupling map $f:[0,1]\to [0,1]$,

$$f:x \mapsto 10x \mod 1,$$

where one multiplies $x$ by $10$ and removes the integer part (another way of writing it: $f(x) = 10x - \lfloor10x \rfloor$).

Who cares?

Why define this function? It makes most sense in digit form:

if $x = 0.d_1d_2d_3\ldots,\ $ $f(x) = 0.d_2d_3d_4\ldots$

That is, $f$ acts by shifting all the digits up by one, forgetting the first digit.

From this alone, you can very quickly verify the following points, and you only need the first.

  1. If $x\in E$, $f(x)\in E$.
  2. Moreover, $f: E \to E$ is a 2-to-1 surjection.
  3. For any $n\in \mathbb N$, $f(E_{n+1}) = E_n$. ($f(E_1) = [0,1]$.)

Regarding the second step of your induction: (EDITED.)

A consequence of property 3.:

$$ y \in \bigcap_{n=1}^{\infty} E_n \implies \ \forall\,n\geq 2,\ y \in E_n \stackrel{\text{3.}}\implies \ \forall\,n\geq 2,\ f(y) \in f(E_n) = E_{n-1} \implies f(y) \in \bigcap_{n=1}^\infty E_n. $$

I.e.,

$$ y \in \bigcap_{n=1}^{\infty} E_n \implies f(y) \in \bigcap_{n=1}^\infty E_n.\tag{1} $$

Now suppose $y = 0.d_1d_2d_3\ldots \in \bigcap_{n=1}^\infty E_n$. The digits of $f(y)$ are given by

$$f(y) = 0.e_1e_2e_3\ldots \qquad\text{where, for every }n,\ e_n = d_{n+1}.$$

By (1), we know $f(y) \in \bigcap_{n=1}^\infty E_n$ and so, by your "base case," its first digit is in $\{4,7\}$.

But this first digit, $e_1 = d_2$, is simply the second digit of $y$, so you're done: $d_2 \in \{4,7\}$.

Hopefully you can see how this can be generalised to $d_{n+1}$ (apply $f$ more than once). No inductive assumption required!

2. Aside: a fractal geometry viewpoint

$E$ is really just like the (middle-thirds) Cantor set. So any argument that works for the Cantor set should work here as well (the Cantor set can be defined in terms of base 3 [ternary], rather than base 10, expansions).

The big result you are trying to prove is a special case of one in fractal geometry.

to set this up, it is simple to see that $E$ is an attractor of the following contractions, $f_4, f_7: [0,1] \to [0,1],$

$$f_4(x) = \frac{x+4}{10},\qquad f_7(x) = \frac{x+7}{10}$$

(in digit form, these are: $f_i:0.d_1d_2d_3\ldots \; \mapsto 0.\,\underline{i}\,d_1d_2d_3),$

where attractor here means: $E$ is a compact subset of $[0,1]$ ($[0,1]$ being the domain) such that $E = f_4(E) \sqcup f_7(E)$.

From fractal geometry, it is known that attractors are 1) unique and 2) satisfy the following formula.

$$E = \bigcap_{n= 1}^\infty \;\; \bigcup_{(i_1,\ldots,i_n)\in \{4,7\}^n} \underbrace{f_{i_1}\circ f_{i_2}\circ f_{i_3}\circ \cdots \circ f_{i_n}[0,1]}_{\text{first $n$ digits are }i_1,\ i_2,\ldots i_n} $$

Furthermore, $$ E_n = \bigcup_{(i_1,\ldots,i_n)\in \{4,7\}^n} f_{i_1}\circ f_{i_2}\circ f_{i_3}\circ \cdots \circ f_{i_n}[0,1],$$

where this last equality follows by your definition of $E_n$ E.g.,

$$E_1 = f_4[0,1] \cup f_7[0,1]$$ $$E_2 = f_4\circ f_4[0,1] \cup f_4\circ f_7[0,1] \cup f_7\circ f_4[0,1] \cup f_7\circ f_7[0,1] $$

and so on.

In other words, this formula (or its proof) gives you another altenrative proof/viewpoint.

Other key words which apply: iterated function system, self-similar sets.