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

Metamath Proof Explorer

Theorem onmindif2

Description: The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed. (Contributed by NM, 20-Nov-2003)

Ref Expression
Assertion onmindif2 
|- ( ( A C_ On /\ A =/= (/) ) -> |^| A e. |^| ( A \ { |^| A } ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( x e. ( A \ { |^| A } ) <-> ( x e. A /\ x =/= |^| A ) )
2 onnmin 
 |-  ( ( A C_ On /\ x e. A ) -> -. x e. |^| A )
3 2 adantlr 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> -. x e. |^| A )
4 oninton 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. On )
5 ssel2 
 |-  ( ( A C_ On /\ x e. A ) -> x e. On )
6 5 adantlr 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> x e. On )
7 ontri1 
 |-  ( ( |^| A e. On /\ x e. On ) -> ( |^| A C_ x <-> -. x e. |^| A ) )
8 onsseleq 
 |-  ( ( |^| A e. On /\ x e. On ) -> ( |^| A C_ x <-> ( |^| A e. x \/ |^| A = x ) ) )
9 7 8 bitr3d 
 |-  ( ( |^| A e. On /\ x e. On ) -> ( -. x e. |^| A <-> ( |^| A e. x \/ |^| A = x ) ) )
10 4 6 9 syl2an2r 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> ( -. x e. |^| A <-> ( |^| A e. x \/ |^| A = x ) ) )
11 3 10 mpbid 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> ( |^| A e. x \/ |^| A = x ) )
12 11 ord 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> ( -. |^| A e. x -> |^| A = x ) )
13 eqcom 
 |-  ( |^| A = x <-> x = |^| A )
14 12 13 imbitrdi 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> ( -. |^| A e. x -> x = |^| A ) )
15 14 necon1ad 
 |-  ( ( ( A C_ On /\ A =/= (/) ) /\ x e. A ) -> ( x =/= |^| A -> |^| A e. x ) )
16 15 expimpd 
 |-  ( ( A C_ On /\ A =/= (/) ) -> ( ( x e. A /\ x =/= |^| A ) -> |^| A e. x ) )
17 1 16 biimtrid 
 |-  ( ( A C_ On /\ A =/= (/) ) -> ( x e. ( A \ { |^| A } ) -> |^| A e. x ) )
18 17 ralrimiv 
 |-  ( ( A C_ On /\ A =/= (/) ) -> A. x e. ( A \ { |^| A } ) |^| A e. x )
19 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
20 elintg 
 |-  ( |^| A e. _V -> ( |^| A e. |^| ( A \ { |^| A } ) <-> A. x e. ( A \ { |^| A } ) |^| A e. x ) )
21 19 20 sylbi 
 |-  ( A =/= (/) -> ( |^| A e. |^| ( A \ { |^| A } ) <-> A. x e. ( A \ { |^| A } ) |^| A e. x ) )
22 21 adantl 
 |-  ( ( A C_ On /\ A =/= (/) ) -> ( |^| A e. |^| ( A \ { |^| A } ) <-> A. x e. ( A \ { |^| A } ) |^| A e. x ) )
23 18 22 mpbird 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. |^| ( A \ { |^| A } ) )