Theorem prcunqu 7501

Description: An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)

Assertion

Ref	Expression
prcunqu	|- ( ( <. L , U >. e. P. /\ C e. U ) -> ( C <Q B -> B e. U ) )

Proof of Theorem prcunqu

Dummy variables b c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelnq 7381	. . . . . 6 |- <Q C_ ( Q. X. Q. )
2	1	brel 4692	. . . . 5 |- ( C <Q B -> ( C e. Q. /\ B e. Q. ) )
3	2	simprd 114	. . . 4 |- ( C <Q B -> B e. Q. )
4	3	adantl 277	. . 3 |- ( ( ( <. L , U >. e. P. /\ C e. U ) /\ C <Q B ) -> B e. Q. )
5		breq2 4021	. . . . . . 7 |- ( b = B -> ( C <Q b <-> C <Q B ) )
6		eleq1 2251	. . . . . . 7 |- ( b = B -> ( b e. U <-> B e. U ) )
7	5, 6	imbi12d 234	. . . . . 6 |- ( b = B -> ( ( C <Q b -> b e. U ) <-> ( C <Q B -> B e. U ) ) )
8	7	imbi2d 230	. . . . 5 |- ( b = B -> ( ( ( <. L , U >. e. P. /\ C e. U ) -> ( C <Q b -> b e. U ) ) <-> ( ( <. L , U >. e. P. /\ C e. U ) -> ( C <Q B -> B e. U ) ) ) )
9	1	brel 4692	. . . . . . . 8 |- ( C <Q b -> ( C e. Q. /\ b e. Q. ) )
10		an42 587	. . . . . . . . 9 |- ( ( ( C e. Q. /\ b e. Q. ) /\ ( C e. U /\ <. L , U >. e. P. ) ) <-> ( ( C e. Q. /\ C e. U ) /\ ( <. L , U >. e. P. /\ b e. Q. ) ) )
11		breq1 4020	. . . . . . . . . . . . . . . 16 |- ( c = C -> ( c <Q b <-> C <Q b ) )
12		eleq1 2251	. . . . . . . . . . . . . . . 16 |- ( c = C -> ( c e. U <-> C e. U ) )
13	11, 12	anbi12d 473	. . . . . . . . . . . . . . 15 |- ( c = C -> ( ( c <Q b /\ c e. U ) <-> ( C <Q b /\ C e. U ) ) )
14	13	rspcev 2855	. . . . . . . . . . . . . 14 |- ( ( C e. Q. /\ ( C <Q b /\ C e. U ) ) -> E. c e. Q. ( c <Q b /\ c e. U ) )
15		elinp 7490	. . . . . . . . . . . . . . . 16 |- ( <. L , U >. e. P. <-> ( ( ( L C_ Q. /\ U C_ Q. ) /\ ( E. c e. Q. c e. L /\ E. b e. Q. b e. U ) ) /\ ( ( A. c e. Q. ( c e. L <-> E. b e. Q. ( c <Q b /\ b e. L ) ) /\ A. b e. Q. ( b e. U <-> E. c e. Q. ( c <Q b /\ c e. U ) ) ) /\ A. c e. Q. -. ( c e. L /\ c e. U ) /\ A. c e. Q. A. b e. Q. ( c <Q b -> ( c e. L \/ b e. U ) ) ) ) )
16		simpr1r 1056	. . . . . . . . . . . . . . . 16 |- ( ( ( ( L C_ Q. /\ U C_ Q. ) /\ ( E. c e. Q. c e. L /\ E. b e. Q. b e. U ) ) /\ ( ( A. c e. Q. ( c e. L <-> E. b e. Q. ( c <Q b /\ b e. L ) ) /\ A. b e. Q. ( b e. U <-> E. c e. Q. ( c <Q b /\ c e. U ) ) ) /\ A. c e. Q. -. ( c e. L /\ c e. U ) /\ A. c e. Q. A. b e. Q. ( c <Q b -> ( c e. L \/ b e. U ) ) ) ) -> A. b e. Q. ( b e. U <-> E. c e. Q. ( c <Q b /\ c e. U ) ) )
17	15, 16	sylbi 121	. . . . . . . . . . . . . . 15 |- ( <. L , U >. e. P. -> A. b e. Q. ( b e. U <-> E. c e. Q. ( c <Q b /\ c e. U ) ) )
18	17	r19.21bi 2577	. . . . . . . . . . . . . 14 |- ( ( <. L , U >. e. P. /\ b e. Q. ) -> ( b e. U <-> E. c e. Q. ( c <Q b /\ c e. U ) ) )
19	14, 18	syl5ibrcom 157	. . . . . . . . . . . . 13 |- ( ( C e. Q. /\ ( C <Q b /\ C e. U ) ) -> ( ( <. L , U >. e. P. /\ b e. Q. ) -> b e. U ) )
20	19	3impb 1200	. . . . . . . . . . . 12 |- ( ( C e. Q. /\ C <Q b /\ C e. U ) -> ( ( <. L , U >. e. P. /\ b e. Q. ) -> b e. U ) )
21	20	3com12 1208	. . . . . . . . . . 11 |- ( ( C <Q b /\ C e. Q. /\ C e. U ) -> ( ( <. L , U >. e. P. /\ b e. Q. ) -> b e. U ) )
22	21	3expib 1207	. . . . . . . . . 10 |- ( C <Q b -> ( ( C e. Q. /\ C e. U ) -> ( ( <. L , U >. e. P. /\ b e. Q. ) -> b e. U ) ) )
23	22	impd 254	. . . . . . . . 9 |- ( C <Q b -> ( ( ( C e. Q. /\ C e. U ) /\ ( <. L , U >. e. P. /\ b e. Q. ) ) -> b e. U ) )
24	10, 23	biimtrid 152	. . . . . . . 8 |- ( C <Q b -> ( ( ( C e. Q. /\ b e. Q. ) /\ ( C e. U /\ <. L , U >. e. P. ) ) -> b e. U ) )
25	9, 24	mpand 429	. . . . . . 7 |- ( C <Q b -> ( ( C e. U /\ <. L , U >. e. P. ) -> b e. U ) )
26	25	com12 30	. . . . . 6 |- ( ( C e. U /\ <. L , U >. e. P. ) -> ( C <Q b -> b e. U ) )
27	26	ancoms 268	. . . . 5 |- ( ( <. L , U >. e. P. /\ C e. U ) -> ( C <Q b -> b e. U ) )
28	8, 27	vtoclg 2811	. . . 4 |- ( B e. Q. -> ( ( <. L , U >. e. P. /\ C e. U ) -> ( C <Q B -> B e. U ) ) )
29	28	impd 254	. . 3 |- ( B e. Q. -> ( ( ( <. L , U >. e. P. /\ C e. U ) /\ C <Q B ) -> B e. U ) )
30	4, 29	mpcom 36	. 2 |- ( ( ( <. L , U >. e. P. /\ C e. U ) /\ C <Q B ) -> B e. U )
31	30	ex 115	1 |- ( ( <. L , U >. e. P. /\ C e. U ) -> ( C <Q B -> B e. U ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 709   /\ w3a 979   = wceq 1363   e. wcel 2159   A.wral 2467   E.wrex 2468   C_ wss 3143   <.cop 3609   class class class wbr 4017   Q.cnq 7296   <Q cltq 7301   P.cnp 7307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-coll 4132  ax-sep 4135  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-iinf 4601

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ral 2472  df-rex 2473  df-reu 2474  df-rab 2476  df-v 2753  df-sbc 2977  df-csb 3072  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-int 3859  df-iun 3902  df-br 4018  df-opab 4079  df-mpt 4080  df-id 4307  df-iom 4604  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-qs 6558  df-ni 7320  df-nqqs 7364  df-ltnqqs 7369  df-inp 7482

This theorem is referenced by:  prarloc  7519  prarloc2  7520  addnqprulem  7544  nqpru  7568  prmuloc2  7583  mulnqpru  7585  distrlem4pru  7601  1idpru  7607  ltexprlemm  7616  ltexprlemupu  7620  ltexprlemrl  7626  ltexprlemfu  7627  ltexprlemru  7628  aptiprlemu  7656  suplocexprlemdisj  7736  suplocexprlemub  7739