Metamath Proof Explorer


Theorem elcnfn

Description: Property defining a continuous functional. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion elcnfn TContFnT:xy+z+wnormw-x<zTwTx<y

Proof

Step Hyp Ref Expression
1 fveq1 t=Ttw=Tw
2 fveq1 t=Ttx=Tx
3 1 2 oveq12d t=Ttwtx=TwTx
4 3 fveq2d t=Ttwtx=TwTx
5 4 breq1d t=Ttwtx<yTwTx<y
6 5 imbi2d t=Tnormw-x<ztwtx<ynormw-x<zTwTx<y
7 6 rexralbidv t=Tz+wnormw-x<ztwtx<yz+wnormw-x<zTwTx<y
8 7 2ralbidv t=Txy+z+wnormw-x<ztwtx<yxy+z+wnormw-x<zTwTx<y
9 df-cnfn ContFn=t|xy+z+wnormw-x<ztwtx<y
10 8 9 elrab2 TContFnTxy+z+wnormw-x<zTwTx<y
11 cnex V
12 ax-hilex V
13 11 12 elmap TT:
14 13 anbi1i Txy+z+wnormw-x<zTwTx<yT:xy+z+wnormw-x<zTwTx<y
15 10 14 bitri TContFnT:xy+z+wnormw-x<zTwTx<y