Metamath Proof Explorer


Theorem isfin3ds

Description: Property of a III-finite set (descending sequence version). (Contributed by Mario Carneiro, 16-May-2015)

Ref Expression
Hypothesis isfin3ds.f F=g|a𝒫gωbωasucbabranarana
Assertion isfin3ds AVAFf𝒫Aωxωfsucxfxranfranf

Proof

Step Hyp Ref Expression
1 isfin3ds.f F=g|a𝒫gωbωasucbabranarana
2 suceq b=xsucb=sucx
3 2 fveq2d b=xasucb=asucx
4 fveq2 b=xab=ax
5 3 4 sseq12d b=xasucbabasucxax
6 5 cbvralvw bωasucbabxωasucxax
7 fveq1 a=fasucx=fsucx
8 fveq1 a=fax=fx
9 7 8 sseq12d a=fasucxaxfsucxfx
10 9 ralbidv a=fxωasucxaxxωfsucxfx
11 6 10 syl5bb a=fbωasucbabxωfsucxfx
12 rneq a=frana=ranf
13 12 inteqd a=frana=ranf
14 13 12 eleq12d a=franaranaranfranf
15 11 14 imbi12d a=fbωasucbabranaranaxωfsucxfxranfranf
16 15 cbvralvw a𝒫gωbωasucbabranaranaf𝒫gωxωfsucxfxranfranf
17 pweq g=A𝒫g=𝒫A
18 17 oveq1d g=A𝒫gω=𝒫Aω
19 18 raleqdv g=Af𝒫gωxωfsucxfxranfranff𝒫Aωxωfsucxfxranfranf
20 16 19 syl5bb g=Aa𝒫gωbωasucbabranaranaf𝒫Aωxωfsucxfxranfranf
21 20 1 elab2g AVAFf𝒫Aωxωfsucxfxranfranf