Metamath Proof Explorer


Theorem ssfin3ds

Description: A subset of a III-finite set is III-finite. (Contributed by Stefan O'Rear, 4-Nov-2014)

Ref Expression
Hypothesis isfin3ds.f F=g|a𝒫gωbωasucbabranarana
Assertion ssfin3ds AFBABF

Proof

Step Hyp Ref Expression
1 isfin3ds.f F=g|a𝒫gωbωasucbabranarana
2 pwexg AF𝒫AV
3 simpr AFBABA
4 3 sspwd AFBA𝒫B𝒫A
5 mapss 𝒫AV𝒫B𝒫A𝒫Bω𝒫Aω
6 2 4 5 syl2an2r AFBA𝒫Bω𝒫Aω
7 1 isfin3ds AFAFf𝒫Aωxωfsucxfxranfranf
8 7 ibi AFf𝒫Aωxωfsucxfxranfranf
9 8 adantr AFBAf𝒫Aωxωfsucxfxranfranf
10 ssralv 𝒫Bω𝒫Aωf𝒫Aωxωfsucxfxranfranff𝒫Bωxωfsucxfxranfranf
11 6 9 10 sylc AFBAf𝒫Bωxωfsucxfxranfranf
12 ssexg BAAFBV
13 12 ancoms AFBABV
14 1 isfin3ds BVBFf𝒫Bωxωfsucxfxranfranf
15 13 14 syl AFBABFf𝒫Bωxωfsucxfxranfranf
16 11 15 mpbird AFBABF