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

Metamath Proof Explorer

Theorem phplem1

Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 23-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → 𝐴 ∈ ω )
2 peano2 ⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
3 enrefnn ⊢ ( suc 𝐴 ∈ ω → suc 𝐴 ≈ suc 𝐴 )
4 2 3 syl ⊢ ( 𝐴 ∈ ω → suc 𝐴 ≈ suc 𝐴 )
5 4 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → suc 𝐴 ≈ suc 𝐴 )
6 simpr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → 𝐵 ∈ suc 𝐴 )
7 dif1ennn ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝐴 ≈ suc 𝐴 ∧ 𝐵 ∈ suc 𝐴 ) → ( suc 𝐴 ∖ { 𝐵 } ) ≈ 𝐴 )
8 1 5 6 7 syl3anc ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → ( suc 𝐴 ∖ { 𝐵 } ) ≈ 𝐴 )
9 nnfi ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )
10 ensymfib ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) ↔ ( suc 𝐴 ∖ { 𝐵 } ) ≈ 𝐴 ) )
11 1 9 10 3syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → ( 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) ↔ ( suc 𝐴 ∖ { 𝐵 } ) ≈ 𝐴 ) )
12 8 11 mpbird ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) )