Theorem nnwoOLD 4608

Description: Well-ordering principle: any non-empty set of natural numbers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34.

Assertion

Ref	Expression
nnwoOLD	|- ((A (_ NN /\ A =/= (/)) -> E.x e. A A.y e. A x <_ y)

Distinct variable group(s):   x,y,A

Proof of Theorem nnwoOLD

Step	Hyp	Ref	Expression
1		breq1 2065	. . . . . . . . . . . 12 |- (v = 1 -> (v <_ y <-> 1 <_ y))
2	1	biraldv 1219	. . . . . . . . . . 11 |- (v = 1 -> (A.y e. A v <_ y <-> A.y e. A 1 <_ y))
3	2	imbi2d 464	. . . . . . . . . 10 |- (v = 1 -> (((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A 1 <_ y)))
4		breq1 2065	. . . . . . . . . . . 12 |- (v = z -> (v <_ y <-> z <_ y))
5	4	biraldv 1219	. . . . . . . . . . 11 |- (v = z -> (A.y e. A v <_ y <-> A.y e. A z <_ y))
6	5	imbi2d 464	. . . . . . . . . 10 |- (v = z -> (((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A z <_ y)))
7		breq1 2065	. . . . . . . . . . . 12 |- (v = (z + 1) -> (v <_ y <-> (z + 1) <_ y))
8	7	biraldv 1219	. . . . . . . . . . 11 |- (v = (z + 1) -> (A.y e. A v <_ y <-> A.y e. A (z + 1) <_ y))
9	8	imbi2d 464	. . . . . . . . . 10 |- (v = (z + 1) -> (((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A (z + 1) <_ y)))
10		breq1 2065	. . . . . . . . . . . 12 |- (v = w -> (v <_ y <-> w <_ y))
11	10	biraldv 1219	. . . . . . . . . . 11 |- (v = w -> (A.y e. A v <_ y <-> A.y e. A w <_ y))
12	11	imbi2d 464	. . . . . . . . . 10 |- (v = w -> (((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A v <_ y) <-> ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A w <_ y)))
13		ssel 1502	. . . . . . . . . . . . 13 |- (A (_ NN -> (y e. A -> y e. NN))
14		nnge1t 4439	. . . . . . . . . . . . 13 |- (y e. NN -> 1 <_ y)
15	13, 14	syl6 23	. . . . . . . . . . . 12 |- (A (_ NN -> (y e. A -> 1 <_ y))
16	15	r19.21aiv 1259	. . . . . . . . . . 11 |- (A (_ NN -> A.y e. A 1 <_ y)
17	16	adantr 306	. . . . . . . . . 10 |- ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A 1 <_ y)
18		breq1 2065	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> (x <_ y <-> z <_ y))
19	18	biraldv 1219	. . . . . . . . . . . . . . . . . . . 20 |- (x = z -> (A.y e. A x <_ y <-> A.y e. A z <_ y))
20	19	rcla4ev 1403	. . . . . . . . . . . . . . . . . . 19 |- ((z e. A /\ A.y e. A z <_ y) -> E.x e. A A.y e. A x <_ y)
21	20	exp 291	. . . . . . . . . . . . . . . . . 18 |- (z e. A -> (A.y e. A z <_ y -> E.x e. A A.y e. A x <_ y))
22	21	com12 13	. . . . . . . . . . . . . . . . 17 |- (A.y e. A z <_ y -> (z e. A -> E.x e. A A.y e. A x <_ y))
23	22	con3d 87	. . . . . . . . . . . . . . . 16 |- (A.y e. A z <_ y -> (-. E.x e. A A.y e. A x <_ y -> -. z e. A))
24	23	com12 13	. . . . . . . . . . . . . . 15 |- (-. E.x e. A A.y e. A x <_ y -> (A.y e. A z <_ y -> -. z e. A))
25		letri3t 4283	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. RR /\ y e. RR) -> (z = y <-> (z <_ y /\ y <_ z)))
26		nnret 4427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z e. NN -> z e. RR)
27		nnret 4427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y e. NN -> y e. RR)
28	25, 26, 27	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z e. NN /\ y e. NN) -> (z = y <-> (z <_ y /\ y <_ z)))
29		nnleltp1t 4448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. NN /\ z e. NN) -> (y <_ z <-> y < (z + 1)))
30	29	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((z e. NN /\ y e. NN) -> (y <_ z <-> y < (z + 1)))
31		leltt 4278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((z + 1) e. RR /\ y e. RR) -> ((z + 1) <_ y <-> -. y < (z + 1)))
32		ax1re 4064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- 1 e. RR
33		axaddrcl 4067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((z e. RR /\ 1 e. RR) -> (z + 1) e. RR)
34	32, 33	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (z e. RR -> (z + 1) e. RR)
35	31, 34	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((z e. RR /\ y e. RR) -> ((z + 1) <_ y <-> -. y < (z + 1)))
36	35	bicon2d 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((z e. RR /\ y e. RR) -> (y < (z + 1) <-> -. (z + 1) <_ y))
37	36, 26, 27	syl2an 349	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((z e. NN /\ y e. NN) -> (y < (z + 1) <-> -. (z + 1) <_ y))
38	30, 37	bitrd 406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. NN /\ y e. NN) -> (y <_ z <-> -. (z + 1) <_ y))
39	38	anbi2d 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z e. NN /\ y e. NN) -> ((z <_ y /\ y <_ z) <-> (z <_ y /\ -. (z + 1) <_ y)))
40	28, 39	bitrd 406	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z e. NN /\ y e. NN) -> (z = y <-> (z <_ y /\ -. (z + 1) <_ y)))
41		ssel2 1503	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A (_ NN /\ y e. A) -> y e. NN)
42	40, 41	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. NN /\ (A (_ NN /\ y e. A)) -> (z = y <-> (z <_ y /\ -. (z + 1) <_ y)))
43		eleq1a 1158	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. A -> (z = y -> z e. A))
44	43	ad2antrr 323	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. NN /\ (A (_ NN /\ y e. A)) -> (z = y -> z e. A))
45	42, 44	sylbird 180	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((z e. NN /\ (A (_ NN /\ y e. A)) -> ((z <_ y /\ -. (z + 1) <_ y) -> z e. A))
46	45	exp3a 292	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. NN /\ (A (_ NN /\ y e. A)) -> (z <_ y -> (-. (z + 1) <_ y -> z e. A)))
47		con1 84	. . . . . . . . . . . . . . . . . . . . . 22 |- ((-. (z + 1) <_ y -> z e. A) -> (-. z e. A -> (z + 1) <_ y))
48	46, 47	syl6 23	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. NN /\ (A (_ NN /\ y e. A)) -> (z <_ y -> (-. z e. A -> (z + 1) <_ y)))
49	48	com23 32	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. NN /\ (A (_ NN /\ y e. A)) -> (-. z e. A -> (z <_ y -> (z + 1) <_ y)))
50	49	exp32 294	. . . . . . . . . . . . . . . . . . 19 |- (z e. NN -> (A (_ NN -> (y e. A -> (-. z e. A -> (z <_ y -> (z + 1) <_ y)))))
51	50	com34 36	. . . . . . . . . . . . . . . . . 18 |- (z e. NN -> (A (_ NN -> (-. z e. A -> (y e. A -> (z <_ y -> (z + 1) <_ y)))))
52	51	imp41 286	. . . . . . . . . . . . . . . . 17 |- ((((z e. NN /\ A (_ NN) /\ -. z e. A) /\ y e. A) -> (z <_ y -> (z + 1) <_ y))
53	52	r19.20dva 1256	. . . . . . . . . . . . . . . 16 |- (((z e. NN /\ A (_ NN) /\ -. z e. A) -> (A.y e. A z <_ y -> A.y e. A (z + 1) <_ y))
54	53	exp 291	. . . . . . . . . . . . . . 15 |- ((z e. NN /\ A (_ NN) -> (-. z e. A -> (A.y e. A z <_ y -> A.y e. A (z + 1) <_ y)))
55	24, 54	sylan9r 360	. . . . . . . . . . . . . 14 |- (((z e. NN /\ A (_ NN) /\ -. E.x e. A A.y e. A x <_ y) -> (A.y e. A z <_ y -> (A.y e. A z <_ y -> A.y e. A (z + 1) <_ y)))
56	55	pm2.43d 59	. . . . . . . . . . . . 13 |- (((z e. NN /\ A (_ NN) /\ -. E.x e. A A.y e. A x <_ y) -> (A.y e. A z <_ y -> A.y e. A (z + 1) <_ y))
57	56	exp31 293	. . . . . . . . . . . 12 |- (z e. NN -> (A (_ NN -> (-. E.x e. A A.y e. A x <_ y -> (A.y e. A z <_ y -> A.y e. A (z + 1) <_ y))))
58	57	imp3a 279	. . . . . . . . . . 11 |- (z e. NN -> ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> (A.y e. A z <_ y -> A.y e. A (z + 1) <_ y)))
59	58	a2d 15	. . . . . . . . . 10 |- (z e. NN -> (((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A z <_ y) -> ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A (z + 1) <_ y)))
60	3, 6, 9, 12, 17, 59	nnind 4434	. . . . . . . . 9 |- (w e. NN -> ((A (_ NN /\ -. E.x e. A A.y e. A x <_ y) -> A.y e. A w <_ y))
61		breq1 2065	. . . . . . . . . . . . . . . 16 |- (x = w -> (x <_ y <-> w <_ y))
62	61	biraldv 1219	. . . . . . . . . . . . . . 15 |- (x = w -> (A.y e. A x <_ y <-> A.y e. A w <_ y))
63	62	rcla4ev 1403	. . . . . . . . . . . . . 14 |- ((w e. A /\ A.y e. A w <_ y) -> E.x e. A A.y e. A x <_ y)
64	63	exp 291	. . . . . . . . . . . . 13 |- (w e. A -> (A.y e. A w <_ y -> E.x e. A A.y e. A x