Theorem elinp 6457

Description: Membership in positive reals. (Contributed by Jim Kingdon, 27-Sep-2019.)

Assertion

Ref	Expression
elinp	|- ( <. L , U >. e. P. <-> ((( L C_ Q. /\ U C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. U)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))) /\ A. q e. Q. -. ( q e. L /\ q e. U) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U)))))

Distinct variable groups:   r, q, L   U, q, r

Proof of Theorem elinp

Dummy variables u l are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		npsspw 6454	. . . . 5 |- P. C_ ( ~P Q. X. ~P Q.)
2	1	sseli 2935	. . . 4 |- ( <. L , U >. e. P. -> <. L , U >. e. ( ~P Q. X. ~P Q.))
3		opelxp 4317	. . . 4 |- ( <. L , U >. e. ( ~P Q. X. ~P Q.) <-> ( L e. ~P Q. /\ U e. ~P Q.))
4	2, 3	sylib 127	. . 3 |- ( <. L , U >. e. P. -> ( L e. ~P Q. /\ U e. ~P Q.))
5		elex 2560	. . . 4 |- ( L e. ~P Q. -> L e. _V)
6		elex 2560	. . . 4 |- ( U e. ~P Q. -> U e. _V)
7	5, 6	anim12i 321	. . 3 |- (( L e. ~P Q. /\ U e. ~P Q.) -> ( L e. _V /\ U e. _V))
8	4, 7	syl 14	. 2 |- ( <. L , U >. e. P. -> ( L e. _V /\ U e. _V))
9		nqex 6347	. . . . 5 |- Q. e. _V
10	9	ssex 3885	. . . 4 |- ( L C_ Q. -> L e. _V)
11	9	ssex 3885	. . . 4 |- ( U C_ Q. -> U e. _V)
12	10, 11	anim12i 321	. . 3 |- (( L C_ Q. /\ U C_ Q.) -> ( L e. _V /\ U e. _V))
13	12	ad2antrr 457	. 2 |- (((( L C_ Q. /\ U C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. U)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))) /\ A. q e. Q. -. ( q e. L /\ q e. U) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U)))) -> ( L e. _V /\ U e. _V))
14		df-inp 6449	. . . 4 |- P. = { <. l , u >. | ((( l C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. l /\ E. r e. Q. r e. u)) /\ ((A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. l /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u)))) }
15	14	eleq2i 2101	. . 3 |- ( <. L , U >. e. P. <-> <. L , U >. e. { <. l , u >. | ((( l C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. l /\ E. r e. Q. r e. u)) /\ ((A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. l /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u)))) })
16		sseq1 2960	. . . . . . 7 |- ( l = L -> ( l C_ Q. <-> L C_ Q.))
17	16	anbi1d 438	. . . . . 6 |- ( l = L -> (( l C_ Q. /\ u C_ Q.) <-> ( L C_ Q. /\ u C_ Q.)))
18		eleq2 2098	. . . . . . . 8 |- ( l = L -> ( q e. l <-> q e. L))
19	18	rexbidv 2321	. . . . . . 7 |- ( l = L -> (E. q e. Q. q e. l <-> E. q e. Q. q e. L))
20	19	anbi1d 438	. . . . . 6 |- ( l = L -> ((E. q e. Q. q e. l /\ E. r e. Q. r e. u) <-> (E. q e. Q. q e. L /\ E. r e. Q. r e. u)))
21	17, 20	anbi12d 442	. . . . 5 |- ( l = L -> ((( l C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. l /\ E. r e. Q. r e. u)) <-> (( L C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. u))))
22		eleq2 2098	. . . . . . . . . . 11 |- ( l = L -> ( r e. l <-> r e. L))
23	22	anbi2d 437	. . . . . . . . . 10 |- ( l = L -> (( q <Q r /\ r e. l) <-> ( q <Q r /\ r e. L)))
24	23	rexbidv 2321	. . . . . . . . 9 |- ( l = L -> (E. r e. Q. ( q <Q r /\ r e. l) <-> E. r e. Q. ( q <Q r /\ r e. L)))
25	18, 24	bibi12d 224	. . . . . . . 8 |- ( l = L -> (( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) <-> ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L))))
26	25	ralbidv 2320	. . . . . . 7 |- ( l = L -> (A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) <-> A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L))))
27	26	anbi1d 438	. . . . . 6 |- ( l = L -> ((A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) <-> (A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u)))))
28	18	anbi1d 438	. . . . . . . 8 |- ( l = L -> (( q e. l /\ q e. u) <-> ( q e. L /\ q e. u)))
29	28	notbid 591	. . . . . . 7 |- ( l = L -> (-. ( q e. l /\ q e. u) <-> -. ( q e. L /\ q e. u)))
30	29	ralbidv 2320	. . . . . 6 |- ( l = L -> (A. q e. Q. -. ( q e. l /\ q e. u) <-> A. q e. Q. -. ( q e. L /\ q e. u)))
31	18	orbi1d 704	. . . . . . . 8 |- ( l = L -> (( q e. l \/ r e. u) <-> ( q e. L \/ r e. u)))
32	31	imbi2d 219	. . . . . . 7 |- ( l = L -> (( q <Q r -> ( q e. l \/ r e. u)) <-> ( q <Q r -> ( q e. L \/ r e. u))))
33	32	2ralbidv 2342	. . . . . 6 |- ( l = L -> (A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u)) <-> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. u))))
34	27, 30, 33	3anbi123d 1206	. . . . 5 |- ( l = L -> (((A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. l /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u))) <-> ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. L /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. u)))))
35	21, 34	anbi12d 442	. . . 4 |- ( l = L -> (((( l C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. l /\ E. r e. Q. r e. u)) /\ ((A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. l /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u)))) <-> ((( L C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. u)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. L /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. u))))))
36		sseq1 2960	. . . . . . 7 |- (u = U -> (u C_ Q. <-> U C_ Q.))
37	36	anbi2d 437	. . . . . 6 |- (u = U -> (( L C_ Q. /\ u C_ Q.) <-> ( L C_ Q. /\ U C_ Q.)))
38		eleq2 2098	. . . . . . . 8 |- (u = U -> ( r e. u <-> r e. U))
39	38	rexbidv 2321	. . . . . . 7 |- (u = U -> (E. r e. Q. r e. u <-> E. r e. Q. r e. U))
40	39	anbi2d 437	. . . . . 6 |- (u = U -> ((E. q e. Q. q e. L /\ E. r e. Q. r e. u) <-> (E. q e. Q. q e. L /\ E. r e. Q. r e. U)))
41	37, 40	anbi12d 442	. . . . 5 |- (u = U -> ((( L C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. u)) <-> (( L C_ Q. /\ U C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. U))))
42		eleq2 2098	. . . . . . . . . . 11 |- (u = U -> ( q e. u <-> q e. U))
43	42	anbi2d 437	. . . . . . . . . 10 |- (u = U -> (( q <Q r /\ q e. u) <-> ( q <Q r /\ q e. U)))
44	43	rexbidv 2321	. . . . . . . . 9 |- (u = U -> (E. q e. Q. ( q <Q r /\ q e. u) <-> E. q e. Q. ( q <Q r /\ q e. U)))
45	38, 44	bibi12d 224	. . . . . . . 8 |- (u = U -> (( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u)) <-> ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))))
46	45	ralbidv 2320	. . . . . . 7 |- (u = U -> (A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u)) <-> A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))))
47	46	anbi2d 437	. . . . . 6 |- (u = U -> ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) <-> (A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U)))))
48	42	anbi2d 437	. . . . . . . 8 |- (u = U -> (( q e. L /\ q e. u) <-> ( q e. L /\ q e. U)))
49	48	notbid 591	. . . . . . 7 |- (u = U -> (-. ( q e. L /\ q e. u) <-> -. ( q e. L /\ q e. U)))
50	49	ralbidv 2320	. . . . . 6 |- (u = U -> (A. q e. Q. -. ( q e. L /\ q e. u) <-> A. q e. Q. -. ( q e. L /\ q e. U)))
51	38	orbi2d 703	. . . . . . . 8 |- (u = U -> (( q e. L \/ r e. u) <-> ( q e. L \/ r e. U)))
52	51	imbi2d 219	. . . . . . 7 |- (u = U -> (( q <Q r -> ( q e. L \/ r e. u)) <-> ( q <Q r -> ( q e. L \/ r e. U))))
53	52	2ralbidv 2342	. . . . . 6 |- (u = U -> (A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. u)) <-> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U))))
54	47, 50, 53	3anbi123d 1206	. . . . 5 |- (u = U -> (((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. L /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. u))) <-> ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))) /\ A. q e. Q. -. ( q e. L /\ q e. U) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U)))))
55	41, 54	anbi12d 442	. . . 4 |- (u = U -> (((( L C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. u)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. L /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. u)))) <-> ((( L C_ Q. /\ U C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. U)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))) /\ A. q e. Q. -. ( q e. L /\ q e. U) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U))))))
56	35, 55	opelopabg 3996	. . 3 |- (( L e. _V /\ U e. _V) -> ( <. L , U >. e. { <. l , u >. | ((( l C_ Q. /\ u C_ Q.) /\ (E. q e. Q. q e. l /\ E. r e. Q. r e. u)) /\ ((A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l)) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u))) /\ A. q e. Q. -. ( q e. l /\ q e. u) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u)))) } <-> ((( L C_ Q. /\ U C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. U)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))) /\ A. q e. Q. -. ( q e. L /\ q e. U) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U))))))
57	15, 56	syl5bb 181	. 2 |- (( L e. _V /\ U e. _V) -> ( <. L , U >. e. P. <-> ((( L C_ Q. /\ U C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. U)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))) /\ A. q e. Q. -. ( q e. L /\ q e. U) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U))))))
58	8, 13, 57	pm5.21nii 619	1 |- ( <. L , U >. e. P. <-> ((( L C_ Q. /\ U C_ Q.) /\ (E. q e. Q. q e. L /\ E. r e. Q. r e. U)) /\ ((A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L)) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U))) /\ A. q e. Q. -. ( q e. L /\ q e. U) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U)))))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628   /\ w3a 884   = wceq 1242   e. wcel 1390  A.wral 2300  E.wrex 2301   _Vcvv 2551   C_ wss 2911   ~Pcpw 3351   <.cop 3370   class class class wbr 3755   {copab 3808   X. cxp 4286   Q.cnq 6264   <Q cltq 6269   P.cnp 6275

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-qs 6048  df-ni 6288  df-nqqs 6332  df-inp 6449

This theorem is referenced by:  elnp1st2nd  6459  prml  6460  prmu  6461  prssnql  6462  prssnqu  6463  prcdnql  6467  prcunqu  6468  prltlu  6470  prnmaxl  6471  prnminu  6472  prloc  6474  prdisj  6475  nqprxx  6529