Theorem uzwoOLD 8086

Description: Well-ordering principle: any non-empty subset of the upper integers has a least element.

Assertion

Ref	Expression
uzwoOLD	|- ((S C_ (ZZ>=` M) /\ -. S = (/)) -> E.j e. S A.k e. S j <_ k)

Distinct variable group:   j,k,S

Proof of Theorem uzwoOLD

Step	Hyp	Ref	Expression
1		breq1 3542	. . . . . . . . . . . 12 |- (h = M -> (h <_ t <-> M <_ t))
2	1	ralbidv 2403	. . . . . . . . . . 11 |- (h = M -> (A.t e. S h <_ t <-> A.t e. S M <_ t))
3	2	imbi2d 380	. . . . . . . . . 10 |- (h = M -> (((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S M <_ t)))
4		breq1 3542	. . . . . . . . . . . 12 |- (h = m -> (h <_ t <-> m <_ t))
5	4	ralbidv 2403	. . . . . . . . . . 11 |- (h = m -> (A.t e. S h <_ t <-> A.t e. S m <_ t))
6	5	imbi2d 380	. . . . . . . . . 10 |- (h = m -> (((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S m <_ t)))
7		breq1 3542	. . . . . . . . . . . 12 |- (h = (m + 1) -> (h <_ t <-> (m + 1) <_ t))
8	7	ralbidv 2403	. . . . . . . . . . 11 |- (h = (m + 1) -> (A.t e. S h <_ t <-> A.t e. S (m + 1) <_ t))
9	8	imbi2d 380	. . . . . . . . . 10 |- (h = (m + 1) -> (((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S (m + 1) <_ t)))
10		breq1 3542	. . . . . . . . . . . 12 |- (h = n -> (h <_ t <-> n <_ t))
11	10	ralbidv 2403	. . . . . . . . . . 11 |- (h = n -> (A.t e. S h <_ t <-> A.t e. S n <_ t))
12	11	imbi2d 380	. . . . . . . . . 10 |- (h = n -> (((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S n <_ t)))
13		ssel 2878	. . . . . . . . . . . . . 14 |- (S C_ (ZZ>=` M) -> (t e. S -> t e. (ZZ>=` M)))
14		eluzle 8053	. . . . . . . . . . . . . 14 |- (t e. (ZZ>=` M) -> M <_ t)
15	13, 14	syl6 39	. . . . . . . . . . . . 13 |- (S C_ (ZZ>=` M) -> (t e. S -> M <_ t))
16	15	r19.21aiv 2455	. . . . . . . . . . . 12 |- (S C_ (ZZ>=` M) -> A.t e. S M <_ t)
17	16	adantr 543	. . . . . . . . . . 11 |- ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S M <_ t)
18	17	a1i 8	. . . . . . . . . 10 |- (M e. ZZ -> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S M <_ t))
19		uzssz 8058	. . . . . . . . . . . . 13 |- (ZZ>=` M) C_ ZZ
20		sstr 2887	. . . . . . . . . . . . 13 |- ((S C_ (ZZ>=` M) /\ (ZZ>=` M) C_ ZZ) -> S C_ ZZ)
21	19, 20	mpan2 775	. . . . . . . . . . . 12 |- (S C_ (ZZ>=` M) -> S C_ ZZ)
22		eluzelz 8051	. . . . . . . . . . . . 13 |- (m e. (ZZ>=` M) -> m e. ZZ)
23		breq1 3542	. . . . . . . . . . . . . . . . . . . . 21 |- (j = m -> (j <_ t <-> m <_ t))
24	23	ralbidv 2403	. . . . . . . . . . . . . . . . . . . 20 |- (j = m -> (A.t e. S j <_ t <-> A.t e. S m <_ t))
25	24	rcla4ev 2651	. . . . . . . . . . . . . . . . . . 19 |- ((m e. S /\ A.t e. S m <_ t) -> E.j e. S A.t e. S j <_ t)
26	25	expcom 495	. . . . . . . . . . . . . . . . . 18 |- (A.t e. S m <_ t -> (m e. S -> E.j e. S A.t e. S j <_ t))
27	26	con3d 157	. . . . . . . . . . . . . . . . 17 |- (A.t e. S m <_ t -> (-. E.j e. S A.t e. S j <_ t -> -. m e. S))
28	27	com12 26	. . . . . . . . . . . . . . . 16 |- (-. E.j e. S A.t e. S j <_ t -> (A.t e. S m <_ t -> -. m e. S))
29		ssel2 2879	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((S C_ ZZ /\ t e. S) -> t e. ZZ)
30		zre 7801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (m e. ZZ -> m e. RR)
31		zre 7801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t e. ZZ -> t e. RR)
32		letri3 6978	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((m e. RR /\ t e. RR) -> (m = t <-> (m <_ t /\ t <_ m)))
33	30, 31, 32	syl2an 699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. ZZ /\ t e. ZZ) -> (m = t <-> (m <_ t /\ t <_ m)))
34		zleltp1 7845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((t e. ZZ /\ m e. ZZ) -> (t <_ m <-> t < (m + 1)))
35		peano2re 7069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (m e. RR -> (m + 1) e. RR)
36	30, 35	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (m e. ZZ -> (m + 1) e. RR)
37		ltnle 6972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((t e. RR /\ (m + 1) e. RR) -> (t < (m + 1) <-> -. (m + 1) <_ t))
38	31, 36, 37	syl2an 699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((t e. ZZ /\ m e. ZZ) -> (t < (m + 1) <-> -. (m + 1) <_ t))
39	34, 38	bitrd 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((t e. ZZ /\ m e. ZZ) -> (t <_ m <-> -. (m + 1) <_ t))
40	39	ancoms 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((m e. ZZ /\ t e. ZZ) -> (t <_ m <-> -. (m + 1) <_ t))
41	40	anbi2d 814	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. ZZ /\ t e. ZZ) -> ((m <_ t /\ t <_ m) <-> (m <_ t /\ -. (m + 1) <_ t)))
42	33, 41	bitrd 311	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. ZZ /\ t e. ZZ) -> (m = t <-> (m <_ t /\ -. (m + 1) <_ t)))
43	29, 42	sylan2 696	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. ZZ /\ (S C_ ZZ /\ t e. S)) -> (m = t <-> (m <_ t /\ -. (m + 1) <_ t)))
44		eleq1a 2242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (t e. S -> (m = t -> m e. S))
45	44	ad2antll 862	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. ZZ /\ (S C_ ZZ /\ t e. S)) -> (m = t -> m e. S))
46	43, 45	sylbird 269	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((m e. ZZ /\ (S C_ ZZ /\ t e. S)) -> ((m <_ t /\ -. (m + 1) <_ t) -> m e. S))
47	46	exp3a 496	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((m e. ZZ /\ (S C_ ZZ /\ t e. S)) -> (m <_ t -> (-. (m + 1) <_ t -> m e. S)))
48		con1 153	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((-. (m + 1) <_ t -> m e. S) -> (-. m e. S -> (m + 1) <_ t))
49	47, 48	syl6 39	. . . . . . . . . . . . . . . . . . . . . 22 |- ((m e. ZZ /\ (S C_ ZZ /\ t e. S)) -> (m <_ t -> (-. m e. S -> (m + 1) <_ t)))
50	49	com23 68	. . . . . . . . . . . . . . . . . . . . 21 |- ((m e. ZZ /\ (S C_ ZZ /\ t e. S)) -> (-. m e. S -> (m <_ t -> (m + 1) <_ t)))
51	50	exp32 674	. . . . . . . . . . . . . . . . . . . 20 |- (m e. ZZ -> (S C_ ZZ -> (t e. S -> (-. m e. S -> (m <_ t -> (m + 1) <_ t)))))
52	51	com34 78	. . . . . . . . . . . . . . . . . . 19 |- (m e. ZZ -> (S C_ ZZ -> (-. m e. S -> (t e. S -> (m <_ t -> (m + 1) <_ t)))))
53	52	imp41 665	. . . . . . . . . . . . . . . . . 18 |- ((((m e. ZZ /\ S C_ ZZ) /\ -. m e. S) /\ t e. S) -> (m <_ t -> (m + 1) <_ t))
54	53	ralimdva 2451	. . . . . . . . . . . . . . . . 17 |- (((m e. ZZ /\ S C_ ZZ) /\ -. m e. S) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t))
55	54	ex 494	. . . . . . . . . . . . . . . 16 |- ((m e. ZZ /\ S C_ ZZ) -> (-. m e. S -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t)))
56	28, 55	sylan9r 752	. . . . . . . . . . . . . . 15 |- (((m e. ZZ /\ S C_ ZZ) /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S m <_ t -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t)))
57	56	pm2.43d 113	. . . . . . . . . . . . . 14 |- (((m e. ZZ /\ S C_ ZZ) /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t))
58	57	expl 687	. . . . . . . . . . . . 13 |- (m e. ZZ -> ((S C_ ZZ /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t)))
59	22, 58	syl 13	. . . . . . . . . . . 12 |- (m e. (ZZ>=` M) -> ((S C_ ZZ /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t)))
60	21, 59	sylani 745	. . . . . . . . . . 11 |- (m e. (ZZ>=` M) -> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t)))
61	60	a2d 19	. . . . . . . . . 10 |- (m e. (ZZ>=` M) -> (((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S m <_ t) -> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S (m + 1) <_ t)))
62	3, 6, 9, 12, 18, 61	uzind4 8080	. . . . . . . . 9 |- (n e. (ZZ>=` M) -> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S n <_ t))
63		breq1 3542	. . . . . . . . . . . . . . 15 |- (j = n -> (j <_ t <-> n <_ t))
64	63	ralbidv 2403	. . . . . . . . . . . . . 14 |- (j = n -> (A.t e. S j <_ t <-> A.t e. S n <_ t))
65	64	rcla4ev 2651	. . . . . . . . . . . . 13 |- ((n e. S /\ A.t e. S n <_ t) -> E.j e. S A.t e. S j <_ t)
66	65	expcom 495	. . . . . . . . . . . 12 |- (A.t e. S n <_ t -> (n e. S -> E.j e. S A.t e. S j <_ t))
67	66	con3d 157	. . . . . . . . . . 11 |- (A.t e. S n <_ t -> (-. E.j e. S A.t e. S j <_ t -> -. n e. S))
68	67	com12 26	. . . . . . . . . 10 |- (-. E.j e. S A.t e. S j <_ t -> (A.t e. S n <_ t -> -. n e. S))
69	68	adantl 544	. . . . . . . . 9 |- ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S n <_ t -> -. n e. S))
70	62, 69	sylcom 23	. . . . . . . 8 |- (n e. (ZZ>=` M) -> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> -. n e. S))
71		ssel 2878	. . . . . . . . . . 11 |- (S C_ (ZZ>=` M) -> (n e. S -> n e. (ZZ>=` M)))
72	71	con3d 157	. . . . . . . . . 10 |- (S C_ (ZZ>=` M) -> (-. n e. (ZZ>=` M) -> -. n e. S))
73	72	com12 26	. . . . . . . . 9 |- (-. n e. (ZZ>=` M) -> (S C_ (ZZ>=` M) -> -. n e. S))
74	73	adantrd 548	. . . . . . . 8 |- (-. n e. (ZZ>=` M) -> ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> -. n e. S))
75	70, 74	pm2.61i 201	. . . . . . 7 |- ((S C_ (ZZ>=` M) /\ -. E.j e. S A.t e. S j <_ t) -> -. n e. S)
76	75	ex 494	. . . . . 6 |- (S C_ (ZZ>=` M) -> (-. E.j e. S A.t e. S j <_ t -> -. n e. S))
77	76	19.21adv 1964	. . . . 5 |- (S C_ (ZZ>=` M) -> (-. E.j e. S A.t e. S j <_ t -> A.n -. n e. S))
78		eq0 3128	. . . . 5 |- (S = (/) <-> A.n -. n e. S)
79	77, 78	syl6ibr 283	. . . 4 |- (S C_ (ZZ>=` M) -> (-. E.j e. S A.t e. S j <_ t -> S = (/)))
80	79	con1d 152	. . 3 |- (S C_ (ZZ>=` M) -> (-. S = (/) -> E.j e. S A.t e. S j <_ t))
81	80	imp 489	. 2 |- ((S C_ (ZZ>=` M) /\ -. S = (/)) -> E.j e. S A.t e. S j <_ t)
82		breq2 3543	. . . 4 |- (t = k -> (j <_ t <-> j <_ k))
83	82	cbvralv 2557	. . 3 |- (A.t e. S j <_ t <-> A.k e. S j <_ k)
84	83	rexbii 2408	. 2 |- (E.j e. S A.t e. S j <_ t <-> E.j e. S A.k e. S j <_ k)
85	81, 84	sylib 263	1 |- ((S C_ (ZZ>=` M) /\ -. S = (/)) -> E.j e. S A.k e. S j <_ k)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 231   /\ wa 433  A.wal 1613   = wceq 1615   e. wcel 1617  A.wral 2385  E.wrex 2386   C_ wss 2859  (/)c0 3114   class class class wbr 3539  ` cfv 4163  (class class class)co 5020  RRcr 6828  1c1 6830   + caddc 6832   <_ cle 6943   < clt 6947  ZZcz 7096  ZZ>=cuz 8045

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-int 3433  df-br 3540  df-opab 3598  df-id 3779  df-po 3784  df-so 3796  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-iota 5259  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-n 7543  df-n0 7761  df-z 7798  df-uz 8046

Copyright terms: Public domain