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	syl5bi	|- ( ( 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 ) )