Metamath Proof Explorer


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 𝐴 ∖ { 𝐵 } ) )