Description: A subset of a III-finite set is III-finite. (Contributed by Stefan O'Rear, 4-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | isfin3ds.f | |
|
Assertion | ssfin3ds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfin3ds.f | |
|
2 | pwexg | |
|
3 | simpr | |
|
4 | 3 | sspwd | |
5 | mapss | |
|
6 | 2 4 5 | syl2an2r | |
7 | 1 | isfin3ds | |
8 | 7 | ibi | |
9 | 8 | adantr | |
10 | ssralv | |
|
11 | 6 9 10 | sylc | |
12 | ssexg | |
|
13 | 12 | ancoms | |
14 | 1 | isfin3ds | |
15 | 13 14 | syl | |
16 | 11 15 | mpbird | |