Metamath Proof Explorer


Theorem uzwo

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005)

Ref Expression
Assertion uzwo SMSjSkSjk

Proof

Step Hyp Ref Expression
1 breq1 h=MhtMt
2 1 ralbidv h=MtShttSMt
3 2 imbi2d h=MSM¬jStSjttShtSM¬jStSjttSMt
4 breq1 h=mhtmt
5 4 ralbidv h=mtShttSmt
6 5 imbi2d h=mSM¬jStSjttShtSM¬jStSjttSmt
7 breq1 h=m+1htm+1t
8 7 ralbidv h=m+1tShttSm+1t
9 8 imbi2d h=m+1SM¬jStSjttShtSM¬jStSjttSm+1t
10 breq1 h=nhtnt
11 10 ralbidv h=ntShttSnt
12 11 imbi2d h=nSM¬jStSjttShtSM¬jStSjttSnt
13 ssel SMtStM
14 eluzle tMMt
15 13 14 syl6 SMtSMt
16 15 ralrimiv SMtSMt
17 16 adantr SM¬jStSjttSMt
18 uzssz M
19 sstr SMMS
20 18 19 mpan2 SMS
21 eluzelz mMm
22 breq1 j=mjtmt
23 22 ralbidv j=mtSjttSmt
24 23 rspcev mStSmtjStSjt
25 24 expcom tSmtmSjStSjt
26 25 con3rr3 ¬jStSjttSmt¬mS
27 ssel2 StSt
28 zre mm
29 zre tt
30 letri3 mtm=tmttm
31 28 29 30 syl2an mtm=tmttm
32 zleltp1 tmtmt<m+1
33 peano2re mm+1
34 28 33 syl mm+1
35 ltnle tm+1t<m+1¬m+1t
36 29 34 35 syl2an tmt<m+1¬m+1t
37 32 36 bitrd tmtm¬m+1t
38 37 ancoms mttm¬m+1t
39 38 anbi2d mtmttmmt¬m+1t
40 31 39 bitrd mtm=tmt¬m+1t
41 27 40 sylan2 mStSm=tmt¬m+1t
42 eleq1a tSm=tmS
43 42 ad2antll mStSm=tmS
44 41 43 sylbird mStSmt¬m+1tmS
45 44 expd mStSmt¬m+1tmS
46 con1 ¬m+1tmS¬mSm+1t
47 45 46 syl6 mStSmt¬mSm+1t
48 47 com23 mStS¬mSmtm+1t
49 48 exp32 mStS¬mSmtm+1t
50 49 com34 mS¬mStSmtm+1t
51 50 imp41 mS¬mStSmtm+1t
52 51 ralimdva mS¬mStSmttSm+1t
53 52 ex mS¬mStSmttSm+1t
54 26 53 sylan9r mS¬jStSjttSmttSmttSm+1t
55 54 pm2.43d mS¬jStSjttSmttSm+1t
56 55 expl mS¬jStSjttSmttSm+1t
57 21 56 syl mMS¬jStSjttSmttSm+1t
58 20 57 sylani mMSM¬jStSjttSmttSm+1t
59 58 a2d mMSM¬jStSjttSmtSM¬jStSjttSm+1t
60 3 6 9 12 17 59 uzind4i nMSM¬jStSjttSnt
61 breq1 j=njtnt
62 61 ralbidv j=ntSjttSnt
63 62 rspcev nStSntjStSjt
64 63 expcom tSntnSjStSjt
65 64 con3rr3 ¬jStSjttSnt¬nS
66 65 adantl SM¬jStSjttSnt¬nS
67 60 66 sylcom nMSM¬jStSjt¬nS
68 ssel SMnSnM
69 68 con3rr3 ¬nMSM¬nS
70 69 adantrd ¬nMSM¬jStSjt¬nS
71 67 70 pm2.61i SM¬jStSjt¬nS
72 71 ex SM¬jStSjt¬nS
73 72 alrimdv SM¬jStSjtn¬nS
74 eq0 S=n¬nS
75 73 74 syl6ibr SM¬jStSjtS=
76 75 necon1ad SMSjStSjt
77 76 imp SMSjStSjt
78 breq2 t=kjtjk
79 78 cbvralvw tSjtkSjk
80 79 rexbii jStSjtjSkSjk
81 77 80 sylib SMSjSkSjk