Description: The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | hashss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssdomg | |
|
2 | 1 | com12 | |
3 | 2 | adantl | |
4 | 3 | impcom | |
5 | ssfi | |
|
6 | 5 | adantrl | |
7 | simpl | |
|
8 | hashdom | |
|
9 | 6 7 8 | syl2anc | |
10 | 4 9 | mpbird | |
11 | 10 | ex | |
12 | hashinf | |
|
13 | ssexg | |
|
14 | 13 | ancoms | |
15 | hashxrcl | |
|
16 | pnfge | |
|
17 | 14 15 16 | 3syl | |
18 | 17 | ex | |
19 | 18 | adantl | |
20 | breq2 | |
|
21 | 20 | adantr | |
22 | 19 21 | sylibrd | |
23 | 22 | expcom | |
24 | 23 | adantr | |
25 | 12 24 | mpd | |
26 | 25 | impancom | |
27 | 26 | com12 | |
28 | 11 27 | pm2.61i | |