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