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 )