elinp - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer	< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > elinp		Structured version Unicode version

Theorem elinp 6322

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

**Assertion**
Ref	Expression
elinp	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Distinct variable groups:

Proof of Theorem elinp Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		npsspw 6319	. . . . 5
2	1	sseli 2914	. . . 4
3		opelxp 4297	. . . 4 $/\$
4	2, 3	sylib 127	. . 3 $/\$
5		elex 2539	. . . 4
6		elex 2539	. . . 4
7	5, 6	anim12i 321	. . 3 $/\$ $/\$
8	4, 7	syl 14	. 2 $/\$
9		nqex 6216	. . . . 5
10	9	ssex 3864	. . . 4
11	9	ssex 3864	. . . 4
12	10, 11	anim12i 321	. . 3 $/\$ $/\$
13	12	ad2antrr 460	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
14		df-inp 6314	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
15	14	eleq2i 2082	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
16		sseq1 2939	. . . . . . 7
17	16	anbi1d 441	. . . . . 6 $/\$ $/\$
18		eleq2 2079	. . . . . . . 8
19	18	rexbidv 2301	. . . . . . 7
20	19	anbi1d 441	. . . . . 6 $/\$ $/\$
21	17, 20	anbi12d 445	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		eleq2 2079	. . . . . . . . . . 11
23	22	anbi2d 440	. . . . . . . . . 10 $/\$ $/\$
24	23	rexbidv 2301	. . . . . . . . 9 $/\$ $/\$
25	18, 24	bibi12d 224	. . . . . . . 8 $/\$ $/\$
26	25	ralbidv 2300	. . . . . . 7 $/\$ $/\$
27	26	anbi1d 441	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28	18	anbi1d 441	. . . . . . . 8 $/\$ $/\$
29	28	notbid 579	. . . . . . 7 $/\$ $/\$
30	29	ralbidv 2300	. . . . . 6 $/\$ $/\$
31	18	orbi1d 692	. . . . . . . 8 $\/$ $\/$
32	31	imbi2d 219	. . . . . . 7 $\/$ $\/$
33	32	2ralbidv 2322	. . . . . 6 $\/$ $\/$
34	27, 30, 33	3anbi123d 1190	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
35	21, 34	anbi12d 445	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
36		sseq1 2939	. . . . . . 7
37	36	anbi2d 440	. . . . . 6 $/\$ $/\$
38		eleq2 2079	. . . . . . . 8
39	38	rexbidv 2301	. . . . . . 7
40	39	anbi2d 440	. . . . . 6 $/\$ $/\$
41	37, 40	anbi12d 445	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		eleq2 2079	. . . . . . . . . . 11
43	42	anbi2d 440	. . . . . . . . . 10 $/\$ $/\$
44	43	rexbidv 2301	. . . . . . . . 9 $/\$ $/\$
45	38, 44	bibi12d 224	. . . . . . . 8 $/\$ $/\$
46	45	ralbidv 2300	. . . . . . 7 $/\$ $/\$
47	46	anbi2d 440	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	42	anbi2d 440	. . . . . . . 8 $/\$ $/\$
49	48	notbid 579	. . . . . . 7 $/\$ $/\$
50	49	ralbidv 2300	. . . . . 6 $/\$ $/\$
51	38	orbi2d 691	. . . . . . . 8 $\/$ $\/$
52	51	imbi2d 219	. . . . . . 7 $\/$ $\/$
53	52	2ralbidv 2322	. . . . . 6 $\/$ $\/$
54	47, 50, 53	3anbi123d 1190	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
55	41, 54	anbi12d 445	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
56	35, 55	opelopabg 3975	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
57	15, 56	syl5bb 181	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
58	8, 13, 57	pm5.21nii 607	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 97

wb 98 $\/$ wo 616 $/\$ w3a 871

wceq 1226

wcel 1370

wral 2280

wrex 2281

cvv 2531

wss 2890

cpw 3330

cop 3349 class class class wbr 3734

copab 3787

cxp 4266

cnq 6134

cltq 6139

cnp 6145

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 532 ax-in2 533 ax-io 617 ax-5 1312 ax-7 1313 ax-gen 1314 ax-ie1 1359 ax-ie2 1360 ax-8 1372 ax-10 1373 ax-11 1374 ax-i12 1375 ax-bnd 1376 ax-4 1377 ax-13 1381 ax-14 1382 ax-17 1396 ax-i9 1400 ax-ial 1405 ax-i5r 1406 ax-ext 2000 ax-coll 3842 ax-sep 3845 ax-pow 3897 ax-pr 3914 ax-un 4116 ax-iinf 4234

This theorem depends on definitions: df-bi 110 df-3an 873 df-tru 1229 df-nf 1326 df-sb 1624 df-eu 1881 df-mo 1882 df-clab 2005 df-cleq 2011 df-clel 2014 df-nfc 2145 df-ral 2285 df-rex 2286 df-reu 2287 df-rab 2289 df-v 2533 df-sbc 2738 df-csb 2826 df-dif 2893 df-un 2895 df-in 2897 df-ss 2904 df-pw 3332 df-sn 3352 df-pr 3353 df-op 3355 df-uni 3551 df-int 3586 df-iun 3629 df-br 3735 df-opab 3789 df-mpt 3790 df-id 4000 df-iom 4237 df-xp 4274 df-rel 4275 df-cnv 4276 df-co 4277 df-dm 4278 df-rn 4279 df-res 4280 df-ima 4281 df-iota 4790 df-fun 4827 df-fn 4828 df-f 4829 df-f1 4830 df-fo 4831 df-f1o 4832 df-fv 4833 df-qs 6019 df-ni 6158 df-nqqs 6201 df-inp 6314

This theorem is referenced by: elnp1st2nd 6324 prml 6325 prmu 6326 prssnql 6327 prssnqu 6328 prcdnql 6332 prcunqu 6333 prltlu 6335 prnmaxl 6336 prnminu 6337 prloc 6339 prdisj 6340 nqprlu 6395

W3C validator