Theorem unsnen

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

	Ref	Expression
Hypotheses	unsnen.1	⊢ 𝐴 ∈ V
	unsnen.2	⊢ 𝐵 ∈ V
Assertion	unsnen	⊢ ( ¬ 𝐵 ∈ 𝐴 → ( 𝐴 ∪ { 𝐵 } ) ≈ suc ( card ‘ 𝐴 ) )

Proof

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