Theorem uzwo 6395

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

Assertion

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

Distinct variable group:   j,k,S

Proof of Theorem uzwo

Step	Hyp	Ref	Expression
1		breq1 2617	. . . . . . . . . . . 12 |- (h = M -> (h <_ t <-> M <_ t))
2	1	ralbidv 1660	. . . . . . . . . . 11 |- (h = M -> (A.t e. S h <_ t <-> A.t e. S M <_ t))
3	2	imbi2d 611	. . . . . . . . . 10 |- (h = M -> (((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S M <_ t)))
4		breq1 2617	. . . . . . . . . . . 12 |- (h = m -> (h <_ t <-> m <_ t))
5	4	ralbidv 1660	. . . . . . . . . . 11 |- (h = m -> (A.t e. S h <_ t <-> A.t e. S m <_ t))
6	5	imbi2d 611	. . . . . . . . . 10 |- (h = m -> (((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S m <_ t)))
7		breq1 2617	. . . . . . . . . . . 12 |- (h = (m + 1) -> (h <_ t <-> (m + 1) <_ t))
8	7	ralbidv 1660	. . . . . . . . . . 11 |- (h = (m + 1) -> (A.t e. S h <_ t <-> A.t e. S (m + 1) <_ t))
9	8	imbi2d 611	. . . . . . . . . 10 |- (h = (m + 1) -> (((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S (m + 1) <_ t)))
10		breq1 2617	. . . . . . . . . . . 12 |- (h = n -> (h <_ t <-> n <_ t))
11	10	ralbidv 1660	. . . . . . . . . . 11 |- (h = n -> (A.t e. S h <_ t <-> A.t e. S n <_ t))
12	11	imbi2d 611	. . . . . . . . . 10 |- (h = n -> (((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S h <_ t) <-> ((S (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S n <_ t)))
13		ssel 2059	. . . . . . . . . . . . . 14 |- (S (_ (ZZ>` M) -> (t e. S -> t e. (ZZ>` M)))
14		eluzle 6365	. . . . . . . . . . . . . 14 |- (t e. (ZZ>` M) -> M <_ t)
15	13, 14	syl6 22	. . . . . . . . . . . . 13 |- (S (_ (ZZ>` M) -> (t e. S -> M <_ t))
16	15	r19.21aiv 1710	. . . . . . . . . . . 12 |- (S (_ (ZZ>` M) -> A.t e. S M <_ t)
17	16	adantr 389	. . . . . . . . . . 11 |- ((S (_ (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 (_ (ZZ>` M) /\ -. E.j e. S A.t e. S j <_ t) -> A.t e. S M <_ t))
19		eluzelz 6363	. . . . . . . . . . . . 13 |- (m e. (ZZ>` M) -> m e. ZZ)
20		breq1 2617	. . . . . . . . . . . . . . . . . . . . . 22 |- (j = m -> (j <_ t <-> m <_ t))
21	20	ralbidv 1660	. . . . . . . . . . . . . . . . . . . . 21 |- (j = m -> (A.t e. S j <_ t <-> A.t e. S m <_ t))
22	21	rcla4ev 1873	. . . . . . . . . . . . . . . . . . . 20 |- ((m e. S /\ A.t e. S m <_ t) -> E.j e. S A.t e. S j <_ t)
23	22	expcom 374	. . . . . . . . . . . . . . . . . . 19 |- (A.t e. S m <_ t -> (m e. S -> E.j e. S A.t e. S j <_ t))
24	23	con3d 95	. . . . . . . . . . . . . . . . . 18 |- (A.t e. S m <_ t -> (-. E.j e. S A.t e. S j <_ t -> -. m e. S))
25	24	com12 11	. . . . . . . . . . . . . . . . 17 |- (-. E.j e. S A.t e. S j <_ t -> (A.t e. S m <_ t -> -. m e. S))
26		letri3t 5498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((m e. RR /\ t e. RR) -> (m = t <-> (m <_ t /\ t <_ m)))
27		zret 6094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (m e. ZZ -> m e. RR)
28		zret 6094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (t e. ZZ -> t e. RR)
29	26, 27, 28	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((m e. ZZ /\ t e. ZZ) -> (m = t <-> (m <_ t /\ t <_ m)))
30		zleltp1t 6137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((t e. ZZ /\ m e. ZZ) -> (t <_ m <-> t < (m + 1)))
31		ltnlet 5491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((t e. RR /\ (m + 1) e. RR) -> (t < (m + 1) <-> -. (m + 1) <_ t))
32		peano2re 5416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (m e. RR -> (m + 1) e. RR)
33	27, 32	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (m e. ZZ -> (m + 1) e. RR)
34	31, 28, 33	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((t e. ZZ /\ m e. ZZ) -> (t < (m + 1) <-> -. (m + 1) <_ t))
35	30, 34	bitrd 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((t e. ZZ /\ m e. ZZ) -> (t <_ m <-> -. (m + 1) <_ t))
36	35	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((m e. ZZ /\ t e. ZZ) -> (t <_ m <-> -. (m + 1) <_ t))
37	36	anbi2d 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((m e. ZZ /\ t e. ZZ) -> ((m <_ t /\ t <_ m) <-> (m <_ t /\ -. (m + 1) <_ t)))
38	29, 37	bitrd 527	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. ZZ /\ t e. ZZ) -> (m = t <-> (m <_ t /\ -. (m + 1) <_ t)))
39		ssel2 2060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((S (_ ZZ /\ t e. S) -> t e. ZZ)
40	38, 39	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. ZZ /\ (S (_ ZZ /\ t e. S)) -> (m = t <-> (m <_ t /\ -. (m + 1) <_ t)))
41		eleq1a 1540	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t e. S -> (m = t -> m e. S))
42	41	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. ZZ /\ (S (_ ZZ /\ t e. S)) -> (m = t -> m e. S))
43	40, 42	sylbird 205	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. ZZ /\ (S (_ ZZ /\ t e. S)) -> ((m <_ t /\ -. (m + 1) <_ t) -> m e. S))
44	43	exp3a 375	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((m e. ZZ /\ (S (_ ZZ /\ t e. S)) -> (m <_ t -> (-. (m + 1) <_ t -> m e. S)))
45		con1 92	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((-. (m + 1) <_ t -> m e. S) -> (-. m e. S -> (m + 1) <_ t))
46	44, 45	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((m e. ZZ /\ (S (_ ZZ /\ t e. S)) -> (m <_ t -> (-. m e. S -> (m + 1) <_ t)))
47	46	com23 32	. . . . . . . . . . . . . . . . . . . . . 22 |- ((m e. ZZ /\ (S (_ ZZ /\ t e. S)) -> (-. m e. S -> (m <_ t -> (m + 1) <_ t)))
48	47	exp32 377	. . . . . . . . . . . . . . . . . . . . 21 |- (m e. ZZ -> (S (_ ZZ -> (t e. S -> (-. m e. S -> (m <_ t -> (m + 1) <_ t)))))
49	48	com34 36	. . . . . . . . . . . . . . . . . . . 20 |- (m e. ZZ -> (S (_ ZZ -> (-. m e. S -> (t e. S -> (m <_ t -> (m + 1) <_ t)))))
50	49	imp41 368	. . . . . . . . . . . . . . . . . . 19 |- ((((m e. ZZ /\ S (_ ZZ) /\ -. m e. S) /\ t e. S) -> (m <_ t -> (m + 1) <_ t))
51	50	r19.20dva 1706	. . . . . . . . . . . . . . . . . 18 |- (((m e. ZZ /\ S (_ ZZ) /\ -. m e. S) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t))
52	51	ex 373	. . . . . . . . . . . . . . . . 17 |- ((m e. ZZ /\ S (_ ZZ) -> (-. m e. S -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t)))
53	25, 52	sylan9r 469	. . . . . . . . . . . . . . . 16 |- (((m e. ZZ /\ S (_ 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)))
54	53	pm2.43d 65	. . . . . . . . . . . . . . 15 |- (((m e. ZZ /\ S (_ ZZ) /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t))
55	54	exp31 376	. . . . . . . . . . . . . 14 |- (m e. ZZ -> (S (_ ZZ -> (-. E.j e. S A.t e. S j <_ t -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t))))
56	55	imp3a 361	. . . . . . . . . . . . 13 |- (m e. ZZ -> ((S (_ ZZ /\ -. E.j e. S A.t e. S j <_ t) -> (A.t e. S m <_ t -> A.t e. S (m + 1) <_ t)))
57	19, 56	syl 10	. . . . . . . . . . . 12 |- (m e. (ZZ>` M) -> ((S (_ 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		uzssz 6370	. . . . . . . . . . . . 13 |- (ZZ>` M) (_ ZZ
59		sstr 2068	. . . . . . . . . . . . 13 |- ((S (_ (ZZ>` M) /\ (ZZ>` M) (_ ZZ) -> S (_ ZZ)
60	58, 59	mpan2 695	. . . . . . . . . . . 12 |- (S (_ (ZZ>` M) -> S (_ ZZ)
61	57, 60	sylani 464	. . . . . . . . . . 11 |- (m e. (ZZ>` M) -> ((S (_ (ZZ>` M) /\ -. E.j e. S A.