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

Metamath Proof Explorer

Theorem unsnen

Description: Equinumerosity of a set with a new element added. (Contributed by NM, 7-Nov-2008)

Ref Expression
Hypotheses unsnen.1 ⊢ A ∈ V
unsnen.2 ⊢ B ∈ V
Assertion unsnen ⊢ ¬ B ∈ A → A ∪ B ≈ suc ⁡ card ⁡ A

Proof

Step Hyp Ref Expression
1 unsnen.1 ⊢ A ∈ V
2 unsnen.2 ⊢ B ∈ V
3 disjsn ⊢ A ∩ B = ∅ ↔ ¬ B ∈ A
4 cardon ⊢ card ⁡ A ∈ On
5 4 onordi ⊢ Ord ⁡ card ⁡ A
6 orddisj ⊢ Ord ⁡ card ⁡ A → card ⁡ A ∩ card ⁡ A = ∅
7 5 6 ax-mp ⊢ card ⁡ A ∩ card ⁡ A = ∅
8 1 cardid ⊢ card ⁡ A ≈ A
9 8 ensymi ⊢ A ≈ card ⁡ A
10 fvex ⊢ card ⁡ A ∈ V
11 en2sn ⊢ B ∈ V ∧ card ⁡ A ∈ V → B ≈ card ⁡ A
12 2 10 11 mp2an ⊢ B ≈ card ⁡ A
13 unen ⊢ A ≈ card ⁡ A ∧ B ≈ card ⁡ A ∧ A ∩ B = ∅ ∧ card ⁡ A ∩ card ⁡ A = ∅ → A ∪ B ≈ card ⁡ A ∪ card ⁡ A
14 9 12 13 mpanl12 ⊢ A ∩ B = ∅ ∧ card ⁡ A ∩ card ⁡ A = ∅ → A ∪ B ≈ card ⁡ A ∪ card ⁡ A
15 7 14 mpan2 ⊢ A ∩ B = ∅ → A ∪ B ≈ card ⁡ A ∪ card ⁡ A
16 3 15 sylbir ⊢ ¬ B ∈ A → A ∪ B ≈ card ⁡ A ∪ card ⁡ A
17 df-suc ⊢ suc ⁡ card ⁡ A = card ⁡ A ∪ card ⁡ A
18 16 17 breqtrrdi ⊢ ¬ B ∈ A → A ∪ B ≈ suc ⁡ card ⁡ A