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

Theorem onfr 4655
 Description: The ordinal class is well-founded. This lemma is needed for ordon 4798 in order to eliminate the need for the Axiom of Regularity. (Contributed by NM, 17-May-1994.)
Assertion
Ref Expression
onfr

Proof of Theorem onfr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfepfr 4602 . 2
2 n0 3625 . . . 4
3 ineq2 3525 . . . . . . . . . 10
43eqeq1d 2451 . . . . . . . . 9
54rspcev 3061 . . . . . . . 8
65adantll 696 . . . . . . 7
7 inss1 3549 . . . . . . . 8
8 ssel2 3332 . . . . . . . . . . . 12
9 eloni 4626 . . . . . . . . . . . 12
108, 9syl 16 . . . . . . . . . . 11
11 ordfr 4631 . . . . . . . . . . 11
1210, 11syl 16 . . . . . . . . . 10
13 inss2 3550 . . . . . . . . . . 11
14 vex 2968 . . . . . . . . . . . . 13
1514inex1 4379 . . . . . . . . . . . 12
1615epfrc 4603 . . . . . . . . . . 11
1713, 16mp3an2 1268 . . . . . . . . . 10
1812, 17sylan 459 . . . . . . . . 9
19 inass 3539 . . . . . . . . . . . . 13
2010adantr 453 . . . . . . . . . . . . . . . 16
21 simpr 449 . . . . . . . . . . . . . . . . 17
2213, 21sseldi 3335 . . . . . . . . . . . . . . . 16
23 ordelss 4632 . . . . . . . . . . . . . . . 16
2420, 22, 23syl2anc 644 . . . . . . . . . . . . . . 15
25 dfss1 3534 . . . . . . . . . . . . . . 15
2624, 25sylib 190 . . . . . . . . . . . . . 14
2726ineq2d 3531 . . . . . . . . . . . . 13
2819, 27syl5eq 2487 . . . . . . . . . . . 12
2928eqeq1d 2451 . . . . . . . . . . 11
3029rexbidva 2729 . . . . . . . . . 10
3130adantr 453 . . . . . . . . 9
3218, 31mpbid 203 . . . . . . . 8
33 ssrexv 3397 . . . . . . . 8
347, 32, 33mpsyl 62 . . . . . . 7
356, 34pm2.61dane 2689 . . . . . 6
3635ex 425 . . . . 5
3736exlimdv 1648 . . . 4
382, 37syl5bi 210 . . 3
3938imp 420 . 2
401, 39mpgbir 1560 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360  wex 1551   wceq 1654   wcel 1728   wne 2606  wrex 2713   cin 3308   wss 3309  c0 3616   cep 4527   wfr 4573   word 4615  con0 4616 This theorem is referenced by:  ordon  4798 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pr 4438 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-opab 4298  df-tr 4334  df-eprel 4529  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620
 Copyright terms: Public domain W3C validator