This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onmindif

Description: When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003)

Ref Expression
Assertion onmindif 
|- ( ( A C_ On /\ B e. On ) -> B e. |^| ( A \ suc B ) )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( x e. ( A \ suc B ) <-> ( x e. A /\ -. x e. suc B ) )
2 ssel2 
 |-  ( ( A C_ On /\ x e. A ) -> x e. On )
3 ontri1 
 |-  ( ( x e. On /\ B e. On ) -> ( x C_ B <-> -. B e. x ) )
4 onsssuc 
 |-  ( ( x e. On /\ B e. On ) -> ( x C_ B <-> x e. suc B ) )
5 3 4 bitr3d 
 |-  ( ( x e. On /\ B e. On ) -> ( -. B e. x <-> x e. suc B ) )
6 5 con1bid 
 |-  ( ( x e. On /\ B e. On ) -> ( -. x e. suc B <-> B e. x ) )
7 2 6 sylan 
 |-  ( ( ( A C_ On /\ x e. A ) /\ B e. On ) -> ( -. x e. suc B <-> B e. x ) )
8 7 biimpd 
 |-  ( ( ( A C_ On /\ x e. A ) /\ B e. On ) -> ( -. x e. suc B -> B e. x ) )
9 8 exp31 
 |-  ( A C_ On -> ( x e. A -> ( B e. On -> ( -. x e. suc B -> B e. x ) ) ) )
10 9 com23 
 |-  ( A C_ On -> ( B e. On -> ( x e. A -> ( -. x e. suc B -> B e. x ) ) ) )
11 10 imp4b 
 |-  ( ( A C_ On /\ B e. On ) -> ( ( x e. A /\ -. x e. suc B ) -> B e. x ) )
12 1 11 biimtrid 
 |-  ( ( A C_ On /\ B e. On ) -> ( x e. ( A \ suc B ) -> B e. x ) )
13 12 ralrimiv 
 |-  ( ( A C_ On /\ B e. On ) -> A. x e. ( A \ suc B ) B e. x )
14 elintg 
 |-  ( B e. On -> ( B e. |^| ( A \ suc B ) <-> A. x e. ( A \ suc B ) B e. x ) )
15 14 adantl 
 |-  ( ( A C_ On /\ B e. On ) -> ( B e. |^| ( A \ suc B ) <-> A. x e. ( A \ suc B ) B e. x ) )
16 13 15 mpbird 
 |-  ( ( A C_ On /\ B e. On ) -> B e. |^| ( A \ suc B ) )