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

Metamath Proof Explorer

Theorem hashunsngx

Description: The size of the union of a set with a disjoint singleton is the extended real addition of the size of the set and 1, analogous to hashunsng . (Contributed by BTernaryTau, 9-Sep-2023)

Ref Expression
Assertion hashunsngx 
|- ( ( A e. V /\ B e. W ) -> ( -. B e. A -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e 1 ) ) )

Proof

Step Hyp Ref Expression
1 disjsn 
 |-  ( ( A i^i { B } ) = (/) <-> -. B e. A )
2 snfi 
 |-  { B } e. Fin
3 hashunx 
 |-  ( ( A e. V /\ { B } e. Fin /\ ( A i^i { B } ) = (/) ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e ( # ` { B } ) ) )
4 2 3 mp3an2 
 |-  ( ( A e. V /\ ( A i^i { B } ) = (/) ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e ( # ` { B } ) ) )
5 1 4 sylan2br 
 |-  ( ( A e. V /\ -. B e. A ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e ( # ` { B } ) ) )
6 5 3adant2 
 |-  ( ( A e. V /\ B e. W /\ -. B e. A ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e ( # ` { B } ) ) )
7 hashsng 
 |-  ( B e. W -> ( # ` { B } ) = 1 )
8 7 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ -. B e. A ) -> ( # ` { B } ) = 1 )
9 8 oveq2d 
 |-  ( ( A e. V /\ B e. W /\ -. B e. A ) -> ( ( # ` A ) +e ( # ` { B } ) ) = ( ( # ` A ) +e 1 ) )
10 6 9 eqtrd 
 |-  ( ( A e. V /\ B e. W /\ -. B e. A ) -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e 1 ) )
11 10 3expia 
 |-  ( ( A e. V /\ B e. W ) -> ( -. B e. A -> ( # ` ( A u. { B } ) ) = ( ( # ` A ) +e 1 ) ) )