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		dif1en	⊢ ( ( 𝐴 ∈ ω ∧ 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 𝐴 ∖ { 𝐵 } ) )