Theorem nnunb 4520

Description: The set of natural numbers is unbounded above. Theorem I.28 of [Apostol] p. 26.

Assertion

Ref	Expression
nnunb	|- -. E.x e. RR A.y e. NN (y < x \/ y = x)

Distinct variable group(s):   x,y

Proof of Theorem nnunb

Step	Hyp	Ref	Expression
1		pm3.24 496	. . . . . 6 |- -. (A.y e. NN -. x < y /\ -. A.y e. NN -. x < y)
2		oprex 3018	. . . . . . . . . . . . . . 15 |- (x - 1) e. V
3		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (y = (x - 1) -> (y e. RR <-> (x - 1) e. RR))
4		breq1 2065	. . . . . . . . . . . . . . . . 17 |- (y = (x - 1) -> (y < x <-> (x - 1) < x))
5		breq1 2065	. . . . . . . . . . . . . . . . . 18 |- (y = (x - 1) -> (y < z <-> (x - 1) < z))
6	5	birexdv 1220	. . . . . . . . . . . . . . . . 17 |- (y = (x - 1) -> (E.z e. NN y < z <-> E.z e. NN (x - 1) < z))
7	4, 6	imbi12d 474	. . . . . . . . . . . . . . . 16 |- (y = (x - 1) -> ((y < x -> E.z e. NN y < z) <-> ((x - 1) < x -> E.z e. NN (x - 1) < z)))
8	3, 7	imbi12d 474	. . . . . . . . . . . . . . 15 |- (y = (x - 1) -> ((y e. RR -> (y < x -> E.z e. NN y < z)) <-> ((x - 1) e. RR -> ((x - 1) < x -> E.z e. NN (x - 1) < z))))
9	2, 8	cla4v 1400	. . . . . . . . . . . . . 14 |- (A.y(y e. RR -> (y < x -> E.z e. NN y < z)) -> ((x - 1) e. RR -> ((x - 1) < x -> E.z e. NN (x - 1) < z)))
10		ltplus1t 4383	. . . . . . . . . . . . . . 15 |- (x e. RR -> x < (x + 1))
11		ax1re 4064	. . . . . . . . . . . . . . . . 17 |- 1 e. RR
12		ltsubaddt 4353	. . . . . . . . . . . . . . . . 17 |- ((x e. RR /\ 1 e. RR /\ x e. RR) -> ((x - 1) < x <-> x < (x + 1)))
13	11, 12	mp3an2 640	. . . . . . . . . . . . . . . 16 |- ((x e. RR /\ x e. RR) -> ((x - 1) < x <-> x < (x + 1)))
14	13	anidms 332	. . . . . . . . . . . . . . 15 |- (x e. RR -> ((x - 1) < x <-> x < (x + 1)))
15	10, 14	mpbird 171	. . . . . . . . . . . . . 14 |- (x e. RR -> (x - 1) < x)
16	9, 15	syl7 24	. . . . . . . . . . . . 13 |- (A.y(y e. RR -> (y < x -> E.z e. NN y < z)) -> ((x - 1) e. RR -> (x e. RR -> E.z e. NN (x - 1) < z)))
17		resubclt 4173	. . . . . . . . . . . . . 14 |- ((x e. RR /\ 1 e. RR) -> (x - 1) e. RR)
18	11, 17	mpan2 519	. . . . . . . . . . . . 13 |- (x e. RR -> (x - 1) e. RR)
19	16, 18	syl5 22	. . . . . . . . . . . 12 |- (A.y(y e. RR -> (y < x -> E.z e. NN y < z)) -> (x e. RR -> (x e. RR -> E.z e. NN (x - 1) < z)))
20	19	pm2.43d 59	. . . . . . . . . . 11 |- (A.y(y e. RR -> (y < x -> E.z e. NN y < z)) -> (x e. RR -> E.z e. NN (x - 1) < z))
21		df-rex 1206	. . . . . . . . . . 11 |- (E.z e. NN (x - 1) < z <-> E.z(z e. NN /\ (x - 1) < z))
22	20, 21	syl6ib 185	. . . . . . . . . 10 |- (A.y(y e. RR -> (y < x -> E.z e. NN y < z)) -> (x e. RR -> E.z(z e. NN /\ (x - 1) < z)))
23	22	com12 13	. . . . . . . . 9 |- (x e. RR -> (A.y(y e. RR -> (y < x -> E.z e. NN y < z)) -> E.z(z e. NN /\ (x - 1) < z)))
24		ltsubaddt 4353	. . . . . . . . . . . . . . 15 |- ((x e. RR /\ 1 e. RR /\ z e. RR) -> ((x - 1) < z <-> x < (z + 1)))
25	11, 24	mp3an2 640	. . . . . . . . . . . . . 14 |- ((x e. RR /\ z e. RR) -> ((x - 1) < z <-> x < (z + 1)))
26		nnret 4427	. . . . . . . . . . . . . 14 |- (z e. NN -> z e. RR)
27	25, 26	sylan2 346	. . . . . . . . . . . . 13 |- ((x e. RR /\ z e. NN) -> ((x - 1) < z <-> x < (z + 1)))
28	27	exp 291	. . . . . . . . . . . 12 |- (x e. RR -> (z e. NN -> ((x - 1) < z <-> x < (z + 1))))
29	28	pm5.32d 491	. . . . . . . . . . 11 |- (x e. RR -> ((z e. NN /\ (x - 1) < z) <-> (z e. NN /\ x < (z + 1))))
30	29	biexdv 936	. . . . . . . . . 10 |- (x e. RR -> (E.z(z e. NN /\ (x - 1) < z) <-> E.z(z e. NN /\ x < (z + 1))))
31		oprex 3018	. . . . . . . . . . . . 13 |- (z + 1) e. V
32		eleq1 1149	. . . . . . . . . . . . . 14 |- (y = (z + 1) -> (y e. NN <-> (z + 1) e. NN))
33		breq2 2066	. . . . . . . . . . . . . 14 |- (y = (z + 1) -> (x < y <-> x < (z + 1)))
34	32, 33	anbi12d 476	. . . . . . . . . . . . 13 |- (y = (z + 1) -> ((y e. NN /\ x < y) <-> ((z + 1) e. NN /\ x < (z + 1))))
35	31, 34	cla4ev 1401	. . . . . . . . . . . 12 |- (((z + 1) e. NN /\ x < (z + 1)) -> E.y(y e. NN /\ x < y))
36		peano2nn 4433	. . . . . . . . . . . 12 |- (z e. NN -> (z + 1) e. NN)
37	35, 36	sylan 343	. . . . . . . . . . 11 |- ((z e. NN /\ x < (z + 1)) -> E.y(y e. NN /\ x < y))
38	37	19.23aiv 952	. . . . . . . . . 10 |- (E.z(z e. NN /\ x < (z + 1)) -> E.y(y e. NN /\ x < y))
39	30, 38	syl6bi 187	. . . . . . . . 9 |- (x e. RR -> (E.z(z e. NN /\ (x - 1) < z) -> E.y(y e. NN /\ x < y)))
40	23, 39	syld 27	. . . . . . . 8 |- (x e. RR -> (A.y(y e. RR -> (y < x -> E.z e. NN y < z)) -> E.y(y e. NN /\ x < y)))
41		df-ral 1205	. . . . . . . 8 |- (A.y e. RR (y < x -> E.z e. NN y < z) <-> A.y(y e. RR -> (y < x -> E.z e. NN y < z)))
42		df-ral 1205	. . . . . . . . . 10 |- (A.y e. NN -. x < y <-> A.y(y e. NN -> -. x < y))
43		alinexa 724	. . . . . . . . . 10 |- (A.y(y e. NN -> -. x < y) <-> -. E.y(y e. NN /\ x < y))
44	42, 43	bitr2 152	. . . . . . . . 9 |- (-. E.y(y e. NN /\ x < y) <-> A.y e. NN -. x < y)
45	44	bicon1i 193	. . . . . . . 8 |- (-. A.y e. NN -. x < y <-> E.y(y e. NN /\ x < y))
46	40, 41, 45	3imtr4g 426	. . . . . . 7 |- (x e. RR -> (A.y e. RR (y < x -> E.z e. NN y < z) -> -. A.y e. NN -. x < y))
47	46	anim2d 433	. . . . . 6 |- (x e. RR -> ((A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)) -> (A.y e. NN -. x < y /\ -. A.y e. NN -. x < y)))
48	1, 47	mtoi 94	. . . . 5 |- (x e. RR -> -. (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)))
49		imnan 207	. . . . 5 |- ((x e. RR -> -. (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z))) <-> -. (x e. RR /\ (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z))))
50	48, 49	mpbi 164	. . . 4 |- -. (x e. RR /\ (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)))
51	50	nex 779	. . 3 |- -. E.x(x e. RR /\ (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)))
52		df-rex 1206	. . 3 |- (E.x e. RR (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)) <-> E.x(x e. RR /\ (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z))))
53	51, 52	mtbir 167	. 2 |- -. E.x e. RR (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z))
54		1nn 4432	. . . . 5 |- 1 e. NN
55		n0i 1712	. . . . 5 |- (1 e. NN -> -. NN = (/))
56	54, 55	ax-mp 6	. . . 4 |- -. NN = (/)
57		df-ne 1192	. . . 4 |- (NN =/= (/) <-> -. NN = (/))
58	56, 57	mpbir 165	. . 3 |- NN =/= (/)
59		nnssre 4425	. . . 4 |- NN (_ RR
60		sup2 4510	. . . 4 |- ((NN (_ RR /\ NN =/= (/) /\ E.x e. RR A.y e. NN (y < x \/ y = x)) -> E.x e. RR (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)))
61	59, 60	mp3an1 639	. . 3 |- ((NN =/= (/) /\ E.x e. RR A.y e. NN (y < x \/ y = x)) -> E.x e. RR (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)))
62	58, 61	mpan 518	. 2 |- (E.x e. RR A.y e. NN (y < x \/ y = x) -> E.x e. RR (A.y e. NN -. x < y /\ A.y e. RR (y < x -> E.z e. NN y < z)))
63	53, 62	mto 93	1 |- -. E.x e. RR A.y e. NN (y < x \/ y = x)

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196  A.wal 672  E.wex 678   = weq 797   = wceq 1091   e. wcel 1092   =/= wne 1190  A.wral 1201  E.wrex 1202   (_ wss 1487  (/)c0 1707   class class class wbr 2054  (class class class)co 3001  RRcr 4027  1c1 4029   + caddc 4031   < clt 4033   - cmin 4089  NNcn 4093

This theorem is referen