Metamath Proof Explorer


Theorem hashss

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 AVBABA

Proof

Step Hyp Ref Expression
1 ssdomg AFinBABA
2 1 com12 BAAFinBA
3 2 adantl AVBAAFinBA
4 3 impcom AFinAVBABA
5 ssfi AFinBABFin
6 5 adantrl AFinAVBABFin
7 simpl AFinAVBAAFin
8 hashdom BFinAFinBABA
9 6 7 8 syl2anc AFinAVBABABA
10 4 9 mpbird AFinAVBABA
11 10 ex AFinAVBABA
12 hashinf AV¬AFinA=+∞
13 ssexg BAAVBV
14 13 ancoms AVBABV
15 hashxrcl BVB*
16 pnfge B*B+∞
17 14 15 16 3syl AVBAB+∞
18 17 ex AVBAB+∞
19 18 adantl A=+∞AVBAB+∞
20 breq2 A=+∞BAB+∞
21 20 adantr A=+∞AVBAB+∞
22 19 21 sylibrd A=+∞AVBABA
23 22 expcom AVA=+∞BABA
24 23 adantr AV¬AFinA=+∞BABA
25 12 24 mpd AV¬AFinBABA
26 25 impancom AVBA¬AFinBA
27 26 com12 ¬AFinAVBABA
28 11 27 pm2.61i AVBABA