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 
|- ( ( A e. _om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. _om /\ B e. suc A ) -> A e. _om )
2 peano2 
 |-  ( A e. _om -> suc A e. _om )
3 enrefnn 
 |-  ( suc A e. _om -> suc A ~~ suc A )
4 2 3 syl 
 |-  ( A e. _om -> suc A ~~ suc A )
5 4 adantr 
 |-  ( ( A e. _om /\ B e. suc A ) -> suc A ~~ suc A )
6 simpr 
 |-  ( ( A e. _om /\ B e. suc A ) -> B e. suc A )
7 dif1ennn 
 |-  ( ( A e. _om /\ suc A ~~ suc A /\ B e. suc A ) -> ( suc A \ { B } ) ~~ A )
8 1 5 6 7 syl3anc 
 |-  ( ( A e. _om /\ B e. suc A ) -> ( suc A \ { B } ) ~~ A )
9 nnfi 
 |-  ( A e. _om -> A e. Fin )
10 ensymfib 
 |-  ( A e. Fin -> ( A ~~ ( suc A \ { B } ) <-> ( suc A \ { B } ) ~~ A ) )
11 1 9 10 3syl 
 |-  ( ( A e. _om /\ B e. suc A ) -> ( A ~~ ( suc A \ { B } ) <-> ( suc A \ { B } ) ~~ A ) )
12 8 11 mpbird 
 |-  ( ( A e. _om /\ B e. suc A ) -> A ~~ ( suc A \ { B } ) )