Theorem phplem1

Description: Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element. (Contributed by NM, 25-May-1998)

	Ref	Expression
Assertion	phplem1	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		nnord	⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
2		nordeq	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ≠ 𝐵 )
3		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
4	2 3	syl	⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
5	1 4	sylan	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
6		undif4	⊢ ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( { 𝐴 } ∪ 𝐴 ) ∖ { 𝐵 } ) )
7		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
8	7	equncomi	⊢ suc 𝐴 = ( { 𝐴 } ∪ 𝐴 )
9	8	difeq1i	⊢ ( suc 𝐴 ∖ { 𝐵 } ) = ( ( { 𝐴 } ∪ 𝐴 ) ∖ { 𝐵 } )
10	6 9	eqtr4di	⊢ ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )
11	5 10	syl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) )