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 
|- ( ( A e. V /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) )

Proof

Step Hyp Ref Expression
1 ssdomg 
 |-  ( A e. Fin -> ( B C_ A -> B ~<_ A ) )
2 1 com12 
 |-  ( B C_ A -> ( A e. Fin -> B ~<_ A ) )
3 2 adantl 
 |-  ( ( A e. V /\ B C_ A ) -> ( A e. Fin -> B ~<_ A ) )
4 3 impcom 
 |-  ( ( A e. Fin /\ ( A e. V /\ B C_ A ) ) -> B ~<_ A )
5 ssfi 
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
6 5 adantrl 
 |-  ( ( A e. Fin /\ ( A e. V /\ B C_ A ) ) -> B e. Fin )
7 simpl 
 |-  ( ( A e. Fin /\ ( A e. V /\ B C_ A ) ) -> A e. Fin )
8 hashdom 
 |-  ( ( B e. Fin /\ A e. Fin ) -> ( ( # ` B ) <_ ( # ` A ) <-> B ~<_ A ) )
9 6 7 8 syl2anc 
 |-  ( ( A e. Fin /\ ( A e. V /\ B C_ A ) ) -> ( ( # ` B ) <_ ( # ` A ) <-> B ~<_ A ) )
10 4 9 mpbird 
 |-  ( ( A e. Fin /\ ( A e. V /\ B C_ A ) ) -> ( # ` B ) <_ ( # ` A ) )
11 10 ex 
 |-  ( A e. Fin -> ( ( A e. V /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) ) )
12 hashinf 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
13 ssexg 
 |-  ( ( B C_ A /\ A e. V ) -> B e. _V )
14 13 ancoms 
 |-  ( ( A e. V /\ B C_ A ) -> B e. _V )
15 hashxrcl 
 |-  ( B e. _V -> ( # ` B ) e. RR* )
16 pnfge 
 |-  ( ( # ` B ) e. RR* -> ( # ` B ) <_ +oo )
17 14 15 16 3syl 
 |-  ( ( A e. V /\ B C_ A ) -> ( # ` B ) <_ +oo )
18 17 ex 
 |-  ( A e. V -> ( B C_ A -> ( # ` B ) <_ +oo ) )
19 18 adantl 
 |-  ( ( ( # ` A ) = +oo /\ A e. V ) -> ( B C_ A -> ( # ` B ) <_ +oo ) )
20 breq2 
 |-  ( ( # ` A ) = +oo -> ( ( # ` B ) <_ ( # ` A ) <-> ( # ` B ) <_ +oo ) )
21 20 adantr 
 |-  ( ( ( # ` A ) = +oo /\ A e. V ) -> ( ( # ` B ) <_ ( # ` A ) <-> ( # ` B ) <_ +oo ) )
22 19 21 sylibrd 
 |-  ( ( ( # ` A ) = +oo /\ A e. V ) -> ( B C_ A -> ( # ` B ) <_ ( # ` A ) ) )
23 22 expcom 
 |-  ( A e. V -> ( ( # ` A ) = +oo -> ( B C_ A -> ( # ` B ) <_ ( # ` A ) ) ) )
24 23 adantr 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( ( # ` A ) = +oo -> ( B C_ A -> ( # ` B ) <_ ( # ` A ) ) ) )
25 12 24 mpd 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( B C_ A -> ( # ` B ) <_ ( # ` A ) ) )
26 25 impancom 
 |-  ( ( A e. V /\ B C_ A ) -> ( -. A e. Fin -> ( # ` B ) <_ ( # ` A ) ) )
27 26 com12 
 |-  ( -. A e. Fin -> ( ( A e. V /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) ) )
28 11 27 pm2.61i 
 |-  ( ( A e. V /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) )