elinp - Intuitionistic Logic Explorer

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

Theorem elinp 6457

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

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 97

wb 98 $\/$ wo 628 $/\$ w3a 884

wceq 1242

wcel 1390

wral 2300

wrex 2301

cvv 2551

wss 2911

cpw 3351

cop 3370 class class class wbr 3755

copab 3808

cxp 4286

cnq 6264

cltq 6269

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

W3C validator