Metamath Proof Explorer

Theorem hashunsnggt

Description: The size of a set is greater than a nonnegative integer N if and only if the size of the union of that set with a disjoint singleton is greater than N + 1. (Contributed by BTernaryTau, 10-Sep-2023)

Ref Expression
Assertion hashunsnggt 
|- ( ( ( A e. V /\ B e. W /\ N e. NN0 ) /\ -. B e. A ) -> ( N < ( # ` A ) <-> ( N + 1 ) < ( # ` ( A u. { B } ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 1 rexrd 
 |-  ( N e. NN0 -> N e. RR* )
3 hashxrcl 
 |-  ( A e. V -> ( # ` A ) e. RR* )
4 1re 
 |-  1 e. RR
5 xltadd1 
 |-  ( ( N e. RR* /\ ( # ` A ) e. RR* /\ 1 e. RR ) -> ( N < ( # ` A ) <-> ( N +e 1 ) < ( ( # ` A ) +e 1 ) ) )
6 4 5 mp3an3 
 |-  ( ( N e. RR* /\ ( # ` A ) e. RR* ) -> ( N < ( # ` A ) <-> ( N +e 1 ) < ( ( # ` A ) +e 1 ) ) )
7 2 3 6 syl2an 
 |-  ( ( N e. NN0 /\ A e. V ) -> ( N < ( # ` A ) <-> ( N +e 1 ) < ( ( # ` A ) +e 1 ) ) )
8 7 ancoms 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( N < ( # ` A ) <-> ( N +e 1 ) < ( ( # ` A ) +e 1 ) ) )
9 rexadd 
 |-  ( ( N e. RR /\ 1 e. RR ) -> ( N +e 1 ) = ( N + 1 ) )
10 4 9 mpan2 
 |-  ( N e. RR -> ( N +e 1 ) = ( N + 1 ) )
11 1 10 syl 
 |-  ( N e. NN0 -> ( N +e 1 ) = ( N + 1 ) )
12 11 adantl 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( N +e 1 ) = ( N + 1 ) )
13 12 breq1d 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( ( N +e 1 ) < ( ( # ` A ) +e 1 ) <-> ( N + 1 ) < ( ( # ` A ) +e 1 ) ) )
14 8 13 bitrd 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( N < ( # ` A ) <-> ( N + 1 ) < ( ( # ` A ) +e 1 ) ) )
15 14 3adant2 
 |-  ( ( A e. V /\ B e. W /\ N e. NN0 ) -> ( N < ( # ` A ) <-> ( N + 1 ) < ( ( # ` A ) +e 1 ) ) )
16 15 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ N e. NN0 ) /\ -. B e. A ) -> ( N < ( # ` A ) <-> ( N + 1 ) < ( ( # ` A ) +e 1 ) ) )
17 hashunsngx 
 |-  ( ( A e. V /\ B e. W ) -> ( -. B e. A -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e 1 ) ) )
18 17 3impia 
 |-  ( ( A e. V /\ B e. W /\ -. B e. A ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e 1 ) )
19 18 eqcomd 
 |-  ( ( A e. V /\ B e. W /\ -. B e. A ) -> ( ( # ` A ) +e 1 ) = ( # ` ( A u. { B } ) ) )
20 19 3expa 
 |-  ( ( ( A e. V /\ B e. W ) /\ -. B e. A ) -> ( ( # ` A ) +e 1 ) = ( # ` ( A u. { B } ) ) )
21 20 3adantl3 
 |-  ( ( ( A e. V /\ B e. W /\ N e. NN0 ) /\ -. B e. A ) -> ( ( # ` A ) +e 1 ) = ( # ` ( A u. { B } ) ) )
22 21 breq2d 
 |-  ( ( ( A e. V /\ B e. W /\ N e. NN0 ) /\ -. B e. A ) -> ( ( N + 1 ) < ( ( # ` A ) +e 1 ) <-> ( N + 1 ) < ( # ` ( A u. { B } ) ) ) )
23 16 22 bitrd 
 |-  ( ( ( A e. V /\ B e. W /\ N e. NN0 ) /\ -. B e. A ) -> ( N < ( # ` A ) <-> ( N + 1 ) < ( # ` ( A u. { B } ) ) ) )