Metamath Proof Explorer

Theorem phplem2

Description: Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypotheses phplem2.1 
|- A e. _V
phplem2.2 
|- B e. _V
Assertion phplem2 
|- ( ( A e. _om /\ B e. A ) -> A ~~ ( suc A \ { B } ) )

Proof

Step Hyp Ref Expression
1 phplem2.1 
 |-  A e. _V
2 phplem2.2 
 |-  B e. _V
3 snex 
 |-  { <. B , A >. } e. _V
4 2 1 f1osn 
 |-  { <. B , A >. } : { B } -1-1-onto-> { A }
5 f1oen3g 
 |-  ( ( { <. B , A >. } e. _V /\ { <. B , A >. } : { B } -1-1-onto-> { A } ) -> { B } ~~ { A } )
6 3 4 5 mp2an 
 |-  { B } ~~ { A }
7 1 difexi 
 |-  ( A \ { B } ) e. _V
8 7 enref 
 |-  ( A \ { B } ) ~~ ( A \ { B } )
9 6 8 pm3.2i 
 |-  ( { B } ~~ { A } /\ ( A \ { B } ) ~~ ( A \ { B } ) )
10 incom 
 |-  ( { A } i^i ( A \ { B } ) ) = ( ( A \ { B } ) i^i { A } )
11 difss 
 |-  ( A \ { B } ) C_ A
12 ssrin 
 |-  ( ( A \ { B } ) C_ A -> ( ( A \ { B } ) i^i { A } ) C_ ( A i^i { A } ) )
13 11 12 ax-mp 
 |-  ( ( A \ { B } ) i^i { A } ) C_ ( A i^i { A } )
14 nnord 
 |-  ( A e. _om -> Ord A )
15 orddisj 
 |-  ( Ord A -> ( A i^i { A } ) = (/) )
16 14 15 syl 
 |-  ( A e. _om -> ( A i^i { A } ) = (/) )
17 13 16 sseqtrid 
 |-  ( A e. _om -> ( ( A \ { B } ) i^i { A } ) C_ (/) )
18 ss0 
 |-  ( ( ( A \ { B } ) i^i { A } ) C_ (/) -> ( ( A \ { B } ) i^i { A } ) = (/) )
19 17 18 syl 
 |-  ( A e. _om -> ( ( A \ { B } ) i^i { A } ) = (/) )
20 10 19 syl5eq 
 |-  ( A e. _om -> ( { A } i^i ( A \ { B } ) ) = (/) )
21 disjdif 
 |-  ( { B } i^i ( A \ { B } ) ) = (/)
22 20 21 jctil 
 |-  ( A e. _om -> ( ( { B } i^i ( A \ { B } ) ) = (/) /\ ( { A } i^i ( A \ { B } ) ) = (/) ) )
23 unen 
 |-  ( ( ( { B } ~~ { A } /\ ( A \ { B } ) ~~ ( A \ { B } ) ) /\ ( ( { B } i^i ( A \ { B } ) ) = (/) /\ ( { A } i^i ( A \ { B } ) ) = (/) ) ) -> ( { B } u. ( A \ { B } ) ) ~~ ( { A } u. ( A \ { B } ) ) )
24 9 22 23 sylancr 
 |-  ( A e. _om -> ( { B } u. ( A \ { B } ) ) ~~ ( { A } u. ( A \ { B } ) ) )
25 24 adantr 
 |-  ( ( A e. _om /\ B e. A ) -> ( { B } u. ( A \ { B } ) ) ~~ ( { A } u. ( A \ { B } ) ) )
26 uncom 
 |-  ( { B } u. ( A \ { B } ) ) = ( ( A \ { B } ) u. { B } )
27 difsnid 
 |-  ( B e. A -> ( ( A \ { B } ) u. { B } ) = A )
28 26 27 syl5eq 
 |-  ( B e. A -> ( { B } u. ( A \ { B } ) ) = A )
29 28 adantl 
 |-  ( ( A e. _om /\ B e. A ) -> ( { B } u. ( A \ { B } ) ) = A )
30 phplem1 
 |-  ( ( A e. _om /\ B e. A ) -> ( { A } u. ( A \ { B } ) ) = ( suc A \ { B } ) )
31 25 29 30 3brtr3d 
 |-  ( ( A e. _om /\ B e. A ) -> A ~~ ( suc A \ { B } ) )