Theorem 1pr 5182

Description: The positive real number 'one'.

Assertion

Ref	Expression
1pr	|- 1P e. P.

Proof of Theorem 1pr

Step	Hyp	Ref	Expression
1		elnp 5157	. 2 |- (1P e. P. <-> (((/) (. 1P /\ 1P (. Q.) /\ A.x e. 1P (A.y(y <Q x -> y e. 1P) /\ E.y e. 1P x <Q y)))
2		1lt2pq 5143	. . . . . . 7 |- 1Q <Q (1Q +Q 1Q)
3		1q 5122	. . . . . . . . . 10 |- 1Q e. Q.
4	3	elisseti 1865	. . . . . . . . 9 |- 1Q e. V
5		oprex 4041	. . . . . . . . 9 |- (1Q +Q 1Q) e. V
6	4, 5	ltrpq 5150	. . . . . . . 8 |- (1Q <Q (1Q +Q 1Q) -> (*Q` (1Q +Q 1Q)) <Q (*Q` 1Q))
7		fvex 3789	. . . . . . . . . 10 |- (*Q` 1Q) e. V
8	7, 4	mulcompq 5129	. . . . . . . . 9 |- ((*Q` 1Q) .Q 1Q) = (1Q .Q (*Q` 1Q))
9		recclpq 5137	. . . . . . . . . . 11 |- (1Q e. Q. -> (*Q` 1Q) e. Q.)
10	3, 9	ax-mp 7	. . . . . . . . . 10 |- (*Q` 1Q) e. Q.
11		mulidpq 5134	. . . . . . . . . 10 |- ((*Q` 1Q) e. Q. -> ((*Q` 1Q) .Q 1Q) = (*Q` 1Q))
12	10, 11	ax-mp 7	. . . . . . . . 9 |- ((*Q` 1Q) .Q 1Q) = (*Q` 1Q)
13		recidpq 5136	. . . . . . . . . 10 |- (1Q e. Q. -> (1Q .Q (*Q` 1Q)) = 1Q)
14	3, 13	ax-mp 7	. . . . . . . . 9 |- (1Q .Q (*Q` 1Q)) = 1Q
15	8, 12, 14	3eqtr3i 1550	. . . . . . . 8 |- (*Q` 1Q) = 1Q
16	6, 15	syl6breq 2709	. . . . . . 7 |- (1Q <Q (1Q +Q 1Q) -> (*Q` (1Q +Q 1Q)) <Q 1Q)
17	2, 16	ax-mp 7	. . . . . 6 |- (*Q` (1Q +Q 1Q)) <Q 1Q
18		fvex 3789	. . . . . . 7 |- (*Q` (1Q +Q 1Q)) e. V
19		breq1 2677	. . . . . . 7 |- (x = (*Q` (1Q +Q 1Q)) -> (x <Q 1Q <-> (*Q` (1Q +Q 1Q)) <Q 1Q))
20		df-1p 5152	. . . . . . 7 |- 1P = {x | x <Q 1Q}
21	18, 19, 20	elab2 1948	. . . . . 6 |- ((*Q` (1Q +Q 1Q)) e. 1P <-> (*Q` (1Q +Q 1Q)) <Q 1Q)
22	17, 21	mpbir 197	. . . . 5 |- (*Q` (1Q +Q 1Q)) e. 1P
23		ne0i 2337	. . . . 5 |- ((*Q` (1Q +Q 1Q)) e. 1P -> 1P =/= (/))
24	22, 23	ax-mp 7	. . . 4 |- 1P =/= (/)
25		0pss 2360	. . . 4 |- ((/) (. 1P <-> 1P =/= (/))
26	24, 25	mpbir 197	. . 3 |- (/) (. 1P
27		dfpss2 2184	. . . 4 |- (1P (. Q. <-> (1P (_ Q. /\ -. 1P = Q.))
28	20	abeq2i 1617	. . . . . 6 |- (x e. 1P <-> x <Q 1Q)
29		ltrelpq 5116	. . . . . . . 8 |- <Q (_ (Q. X. Q.)
30	4, 29	brel 3280	. . . . . . 7 |- (x <Q 1Q -> (x e. Q. /\ 1Q e. Q.))
31	30	pm3.26d 328	. . . . . 6 |- (x <Q 1Q -> x e. Q.)
32	28, 31	sylbi 206	. . . . 5 |- (x e. 1P -> x e. Q.)
33	32	ssriv 2120	. . . 4 |- 1P (_ Q.
34		ltsopq 5140	. . . . . . 7 |- <Q Or Q.
35	4, 34, 29	soirri 3499	. . . . . 6 |- -. 1Q <Q 1Q
36		breq1 2677	. . . . . . 7 |- (x = 1Q -> (x <Q 1Q <-> 1Q <Q 1Q))
37	4, 36, 20	elab2 1948	. . . . . 6 |- (1Q e. 1P <-> 1Q <Q 1Q)
38	35, 37	mtbir 199	. . . . 5 |- -. 1Q e. 1P
39		eleq2 1582	. . . . . 6 |- (1P = Q. -> (1Q e. 1P <-> 1Q e. Q.))
40	3, 39	mpbiri 201	. . . . 5 |- (1P = Q. -> 1Q e. 1P)
41	38, 40	mto 112	. . . 4 |- -. 1P = Q.
42	27, 33, 41	mpbir2an 742	. . 3 |- 1P (. Q.
43	26, 42	pm3.2i 292	. 2 |- ((/) (. 1P /\ 1P (. Q.)
44		visset 1860	. . . . . . . . 9 |- y e. V
45		visset 1860	. . . . . . . . 9 |- x e. V
46	44, 34, 29, 45, 4	sotri 3500	. . . . . . . 8 |- ((y <Q x /\ x <Q 1Q) -> y <Q 1Q)
47	46	ex 380	. . . . . . 7 |- (y <Q x -> (x <Q 1Q -> y <Q 1Q))
48		df-1p 5152	. . . . . . . 8 |- 1P = {y | y <Q 1Q}
49	48	abeq2i 1617	. . . . . . 7 |- (y e. 1P <-> y <Q 1Q)
50	47, 28, 49	3imtr4g 564	. . . . . 6 |- (y <Q x -> (x e. 1P -> y e. 1P))
51	50	com12 11	. . . . 5 |- (x e. 1P -> (y <Q x -> y e. 1P))
52	51	19.21aiv 1328	. . . 4 |- (x e. 1P -> A.y(y <Q x -> y e. 1P))
53	45, 4	ltbtwnpq 5149	. . . . . 6 |- (x <Q 1Q -> E.y(x <Q y /\ y <Q 1Q))
54	49	anbi1i 492	. . . . . . . 8 |- ((y e. 1P /\ x <Q y) <-> (y <Q 1Q /\ x <Q y))
55		ancom 446	. . . . . . . 8 |- ((y <Q 1Q /\ x <Q y) <-> (x <Q y /\ y <Q 1Q))
56	54, 55	bitri 180	. . . . . . 7 |- ((y e. 1P /\ x <Q y) <-> (x <Q y /\ y <Q 1Q))
57	56	exbii 1092	. . . . . 6 |- (E.y(y e. 1P /\ x <Q y) <-> E.y(x <Q y /\ y <Q 1Q))
58	53, 28, 57	3imtr4i 226	. . . . 5 |- (x e. 1P -> E.y(y e. 1P /\ x <Q y))
59		df-rex 1697	. . . . 5 |- (E.y e. 1P x <Q y <-> E.y(y e. 1P /\ x <Q y))
60	58, 59	sylibr 207	. . . 4 |- (x e. 1P -> E.y e. 1P x <Q y)
61	52, 60	jca 295	. . 3 |- (x e. 1P -> (A.y(y <Q x -> y e. 1P) /\ E.y e. 1P x <Q y))
62	61	rgen 1745	. 2 |- A.x e. 1P (A.y(y <Q x -> y e. 1P) /\ E.y e. 1P x <Q y)
63	1, 43, 62	mpbir2an 742	1 |- 1P e. P.

Syntax hints:  -. wn 2   -> wi 3   /\ wa 230  A.wal 995   = wceq 997   e. wcel 999  E.wex 1021   =/= wne 1632  A.wral 1692  E.wrex 1693   (_ wss 2098   (. wpss 2099  (/)c0 2331   class class class wbr 2674  ` cfv 3239  (class class class)co 4021  Q.cnq 5044  1Qc1q 5045   +Q cplq 5046   .Q cmq 5047  *Qcrq 5048   <Q cltq 5049  P.cnp 5050  1Pc1p 5051

This theorem is referenced by:  1idpr 5198  recexpr 5225  gt0srpr 5252  0r 5254  1r 5255  m1r 5256  m1p1sr 5266  m1m1sr 5267  0lt1sr 5269  0idsr 5271  1idsr 5272  00sr 5273  recexsrlem 5277  mappsrpr 5283  ltpsrpr 5284  map2psrpr 5285

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-1p 5152

Copyright terms: Public domain