Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  onmindif2 Structured version   Unicode version

Theorem onmindif2 4792
 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.)
Assertion
Ref Expression
onmindif2

Proof of Theorem onmindif2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eldifsn 3927 . . . 4
2 onnmin 4783 . . . . . . . . . 10
32adantlr 696 . . . . . . . . 9
4 oninton 4780 . . . . . . . . . . 11
54adantr 452 . . . . . . . . . 10
6 ssel2 3343 . . . . . . . . . . 11
76adantlr 696 . . . . . . . . . 10
8 ontri1 4615 . . . . . . . . . . 11
9 onsseleq 4622 . . . . . . . . . . 11
108, 9bitr3d 247 . . . . . . . . . 10
115, 7, 10syl2anc 643 . . . . . . . . 9
123, 11mpbid 202 . . . . . . . 8
1312ord 367 . . . . . . 7
14 eqcom 2438 . . . . . . 7
1513, 14syl6ib 218 . . . . . 6
1615necon1ad 2671 . . . . 5
1716expimpd 587 . . . 4
181, 17syl5bi 209 . . 3
1918ralrimiv 2788 . 2
20 intex 4356 . . . 4
21 elintg 4058 . . . 4
2220, 21sylbi 188 . . 3