Metamath Proof Explorer


Theorem php2

Description: Corollary of Pigeonhole Principle. (Contributed by NM, 31-May-1998)

Ref Expression
Assertion php2
|- ( ( A e. _om /\ B C. A ) -> B ~< A )

Proof

Step Hyp Ref Expression
1 eleq1
 |-  ( x = A -> ( x e. _om <-> A e. _om ) )
2 psseq2
 |-  ( x = A -> ( B C. x <-> B C. A ) )
3 1 2 anbi12d
 |-  ( x = A -> ( ( x e. _om /\ B C. x ) <-> ( A e. _om /\ B C. A ) ) )
4 breq2
 |-  ( x = A -> ( B ~< x <-> B ~< A ) )
5 3 4 imbi12d
 |-  ( x = A -> ( ( ( x e. _om /\ B C. x ) -> B ~< x ) <-> ( ( A e. _om /\ B C. A ) -> B ~< A ) ) )
6 vex
 |-  x e. _V
7 pssss
 |-  ( B C. x -> B C_ x )
8 ssdomg
 |-  ( x e. _V -> ( B C_ x -> B ~<_ x ) )
9 6 7 8 mpsyl
 |-  ( B C. x -> B ~<_ x )
10 9 adantl
 |-  ( ( x e. _om /\ B C. x ) -> B ~<_ x )
11 php
 |-  ( ( x e. _om /\ B C. x ) -> -. x ~~ B )
12 ensym
 |-  ( B ~~ x -> x ~~ B )
13 11 12 nsyl
 |-  ( ( x e. _om /\ B C. x ) -> -. B ~~ x )
14 brsdom
 |-  ( B ~< x <-> ( B ~<_ x /\ -. B ~~ x ) )
15 10 13 14 sylanbrc
 |-  ( ( x e. _om /\ B C. x ) -> B ~< x )
16 5 15 vtoclg
 |-  ( A e. _om -> ( ( A e. _om /\ B C. A ) -> B ~< A ) )
17 16 anabsi5
 |-  ( ( A e. _om /\ B C. A ) -> B ~< A )