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 ⊢ A ∈ ω ∧ B ∈ suc ⁡ A → A ≈ suc ⁡ A ∖ B

Proof

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