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 ∈ V ∧ B ∈ W → ¬ B ∈ A → A ∪ B = A + 𝑒 1

Proof

Step Hyp Ref Expression
1 disjsn ⊢ A ∩ B = ∅ ↔ ¬ B ∈ A
2 snfi ⊢ B ∈ Fin
3 hashunx ⊢ A ∈ V ∧ B ∈ Fin ∧ A ∩ B = ∅ → A ∪ B = A + 𝑒 B
4 2 3 mp3an2 ⊢ A ∈ V ∧ A ∩ B = ∅ → A ∪ B = A + 𝑒 B
5 1 4 sylan2br ⊢ A ∈ V ∧ ¬ B ∈ A → A ∪ B = A + 𝑒 B
6 5 3adant2 ⊢ A ∈ V ∧ B ∈ W ∧ ¬ B ∈ A → A ∪ B = A + 𝑒 B
7 hashsng ⊢ B ∈ W → B = 1
8 7 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ ¬ B ∈ A → B = 1
9 8 oveq2d ⊢ A ∈ V ∧ B ∈ W ∧ ¬ B ∈ A → A + 𝑒 B = A + 𝑒 1
10 6 9 eqtrd ⊢ A ∈ V ∧ B ∈ W ∧ ¬ B ∈ A → A ∪ B = A + 𝑒 1
11 10 3expia ⊢ A ∈ V ∧ B ∈ W → ¬ B ∈ A → A ∪ B = A + 𝑒 1