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

Theorem onmindif2 6658
 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 4088 . . . 4
2 onnmin 6649 . . . . . . . . . 10
32adantlr 729 . . . . . . . . 9
4 oninton 6646 . . . . . . . . . . 11
54adantr 472 . . . . . . . . . 10
6 ssel2 3413 . . . . . . . . . . 11
76adantlr 729 . . . . . . . . . 10
8 ontri1 5464 . . . . . . . . . . 11
9 onsseleq 5471 . . . . . . . . . . 11
108, 9bitr3d 263 . . . . . . . . . 10
115, 7, 10syl2anc 673 . . . . . . . . 9
123, 11mpbid 215 . . . . . . . 8
1312ord 384 . . . . . . 7
14 eqcom 2478 . . . . . . 7
1513, 14syl6ib 234 . . . . . 6
1615necon1ad 2660 . . . . 5
1716expimpd 614 . . . 4
181, 17syl5bi 225 . . 3
1918ralrimiv 2808 . 2
20 intex 4557 . . . 4
21 elintg 4234 . . . 4
2220, 21sylbi 200 . . 3