Metamath Proof Explorer


Theorem cnndvlem2

Description: Lemma for cnndv . (Contributed by Asger C. Ipsen, 26-Aug-2021)

Ref Expression
Hypotheses cnndvlem2.t T = x x + 1 2 x
cnndvlem2.f F = y n 0 1 2 n T 2 3 n y
cnndvlem2.w W = w i 0 F w i
Assertion cnndvlem2 f f : cn dom f =

Proof

Step Hyp Ref Expression
1 cnndvlem2.t T = x x + 1 2 x
2 cnndvlem2.f F = y n 0 1 2 n T 2 3 n y
3 cnndvlem2.w W = w i 0 F w i
4 1 2 3 cnndvlem1 W : cn dom W =
5 reex V
6 5 mptex w i 0 F w i V
7 3 6 eqeltri W V
8 eleq1 f = W f : cn W : cn
9 oveq2 f = W D f = D W
10 9 dmeqd f = W dom f = dom W
11 10 eqeq1d f = W dom f = dom W =
12 8 11 anbi12d f = W f : cn dom f = W : cn dom W =
13 7 12 spcev W : cn dom W = f f : cn dom f =
14 4 13 ax-mp f f : cn dom f =