Metamath Proof Explorer


Theorem elovolmr

Description: Sufficient condition for elementhood in the set M . (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypotheses elovolm.1 M=y*|f2Aran.fy=supranseq1+absf*<
elovolmr.2 S=seq1+absF
Assertion elovolmr F:2Aran.FsupranS*<M

Proof

Step Hyp Ref Expression
1 elovolm.1 M=y*|f2Aran.fy=supranseq1+absf*<
2 elovolmr.2 S=seq1+absF
3 elovolmlem F2F:2
4 id f=Ff=F
5 4 eqcomd f=FF=f
6 5 coeq2d f=FabsF=absf
7 6 seqeq3d f=Fseq1+absF=seq1+absf
8 2 7 eqtrid f=FS=seq1+absf
9 8 rneqd f=FranS=ranseq1+absf
10 9 supeq1d f=FsupranS*<=supranseq1+absf*<
11 10 biantrud f=FAran.fAran.fsupranS*<=supranseq1+absf*<
12 coeq2 f=F.f=.F
13 12 rneqd f=Fran.f=ran.F
14 13 unieqd f=Fran.f=ran.F
15 14 sseq2d f=FAran.fAran.F
16 11 15 bitr3d f=FAran.fsupranS*<=supranseq1+absf*<Aran.F
17 16 rspcev F2Aran.Ff2Aran.fsupranS*<=supranseq1+absf*<
18 3 17 sylanbr F:2Aran.Ff2Aran.fsupranS*<=supranseq1+absf*<
19 1 elovolm supranS*<Mf2Aran.fsupranS*<=supranseq1+absf*<
20 18 19 sylibr F:2Aran.FsupranS*<M