This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashpss

Description: The size of a proper subset is less than the size of its finite superset. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Assertion hashpss 
|- ( ( A e. Fin /\ B C. A ) -> ( # ` B ) < ( # ` A ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. Fin /\ B C. A ) -> A e. Fin )
2 simpr 
 |-  ( ( A e. Fin /\ B C. A ) -> B C. A )
3 2 pssssd 
 |-  ( ( A e. Fin /\ B C. A ) -> B C_ A )
4 1 3 ssexd 
 |-  ( ( A e. Fin /\ B C. A ) -> B e. _V )
5 hashxrcl 
 |-  ( B e. _V -> ( # ` B ) e. RR* )
6 4 5 syl 
 |-  ( ( A e. Fin /\ B C. A ) -> ( # ` B ) e. RR* )
7 hashxrcl 
 |-  ( A e. Fin -> ( # ` A ) e. RR* )
8 7 adantr 
 |-  ( ( A e. Fin /\ B C. A ) -> ( # ` A ) e. RR* )
9 hashss 
 |-  ( ( A e. Fin /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) )
10 3 9 syldan 
 |-  ( ( A e. Fin /\ B C. A ) -> ( # ` B ) <_ ( # ` A ) )
11 1 adantr 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> A e. Fin )
12 3 adantr 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> B C_ A )
13 11 12 ssfid 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> B e. Fin )
14 simpr 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> ( # ` A ) = ( # ` B ) )
15 hashen 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) = ( # ` B ) <-> A ~~ B ) )
16 15 biimpa 
 |-  ( ( ( A e. Fin /\ B e. Fin ) /\ ( # ` A ) = ( # ` B ) ) -> A ~~ B )
17 11 13 14 16 syl21anc 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> A ~~ B )
18 17 ensymd 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> B ~~ A )
19 fisseneq 
 |-  ( ( A e. Fin /\ B C_ A /\ B ~~ A ) -> B = A )
20 11 12 18 19 syl3anc 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> B = A )
21 2 adantr 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> B C. A )
22 21 pssned 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> B =/= A )
23 22 neneqd 
 |-  ( ( ( A e. Fin /\ B C. A ) /\ ( # ` A ) = ( # ` B ) ) -> -. B = A )
24 20 23 pm2.65da 
 |-  ( ( A e. Fin /\ B C. A ) -> -. ( # ` A ) = ( # ` B ) )
25 24 neqned 
 |-  ( ( A e. Fin /\ B C. A ) -> ( # ` A ) =/= ( # ` B ) )
26 xrltlen 
 |-  ( ( ( # ` B ) e. RR* /\ ( # ` A ) e. RR* ) -> ( ( # ` B ) < ( # ` A ) <-> ( ( # ` B ) <_ ( # ` A ) /\ ( # ` A ) =/= ( # ` B ) ) ) )
27 26 biimpar 
 |-  ( ( ( ( # ` B ) e. RR* /\ ( # ` A ) e. RR* ) /\ ( ( # ` B ) <_ ( # ` A ) /\ ( # ` A ) =/= ( # ` B ) ) ) -> ( # ` B ) < ( # ` A ) )
28 6 8 10 25 27 syl22anc 
 |-  ( ( A e. Fin /\ B C. A ) -> ( # ` B ) < ( # ` A ) )