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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝐵 ∈ 𝐴 → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjsn	⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )
2		snfi	⊢ { 𝐵 } ∈ Fin
3		hashunx	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝐵 } ∈ Fin ∧ ( 𝐴 ∩ { 𝐵 } ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ { 𝐵 } ) ) )
4	2 3	mp3an2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐴 ∩ { 𝐵 } ) = ∅ ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ { 𝐵 } ) ) )
5	1 4	sylan2br	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ { 𝐵 } ) ) )
6	5	3adant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ { 𝐵 } ) ) )
7		hashsng	⊢ ( 𝐵 ∈ 𝑊 → ( ♯ ‘ { 𝐵 } ) = 1 )
8	7	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ { 𝐵 } ) = 1 )
9	8	oveq2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) +𝑒 ( ♯ ‘ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) )
10	6 9	eqtrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) )
11	10	3expia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝐵 ∈ 𝐴 → ( ♯ ‘ ( 𝐴 ∪ { 𝐵 } ) ) = ( ( ♯ ‘ 𝐴 ) +𝑒 1 ) ) )