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 ) ) )