elnp1st2nd - Intuitionistic Logic Explorer

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

Theorem elnp1st2nd 6602

Description: Membership in positive reals, using

and

to refer to the lower and upper cut. (Contributed by Jim Kingdon, 3-Oct-2019.)

**Assertion**
Ref	Expression
elnp1st2nd	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

**Proof of Theorem elnp1st2nd**
Step	Hyp	Ref	Expression
1		npsspw 6597	. . . . 5
2	1	sseli 2966	. . . 4
3		prop 6601	. . . . . . 7
4		elinp 6600	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
5	3, 4	sylib 131	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
6	5	simpld 109	. . . . 5 $/\$ $/\$ $/\$
7	6	simprd 111	. . . 4 $/\$
8	2, 7	jca 294	. . 3 $/\$ $/\$
9	5	simprd 111	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
10	8, 9	jca 294	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
11		1st2nd2 5826	. . . 4
12	11	ad2antrr 465	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
13		xp1st 5817	. . . . . . . 8
14	13	elpwid 3394	. . . . . . 7
15		xp2nd 5818	. . . . . . . 8
16	15	elpwid 3394	. . . . . . 7
17	14, 16	jca 294	. . . . . 6 $/\$
18	17	anim1i 327	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
19	18	anim1i 327	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
20	19, 4	sylibr 141	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
21	12, 20	eqeltrd 2128	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
22	10, 21	impbii 121	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 101

wb 102 $\/$ wo 637 $/\$ w3a 894

wceq 1257

wcel 1407

wral 2321

wrex 2322

wss 2942

cpw 3384

cop 3403 class class class wbr 3789

cxp 4368

cfv 4927

c1st 5790

c2nd 5791

cnq 6406

cltq 6411

cnp 6417

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 103 ax-ia2 104 ax-ia3 105 ax-in1 552 ax-in2 553 ax-io 638 ax-5 1350 ax-7 1351 ax-gen 1352 ax-ie1 1396 ax-ie2 1397 ax-8 1409 ax-10 1410 ax-11 1411 ax-i12 1412 ax-bndl 1413 ax-4 1414 ax-13 1418 ax-14 1419 ax-17 1433 ax-i9 1437 ax-ial 1441 ax-i5r 1442 ax-ext 2036 ax-coll 3897 ax-sep 3900 ax-pow 3952 ax-pr 3969 ax-un 4195 ax-iinf 4336

This theorem depends on definitions: df-bi 114 df-3an 896 df-tru 1260 df-nf 1364 df-sb 1660 df-eu 1917 df-mo 1918 df-clab 2041 df-cleq 2047 df-clel 2050 df-nfc 2181 df-ral 2326 df-rex 2327 df-reu 2328 df-rab 2330 df-v 2574 df-sbc 2785 df-csb 2878 df-dif 2945 df-un 2947 df-in 2949 df-ss 2956 df-pw 3386 df-sn 3406 df-pr 3407 df-op 3409 df-uni 3606 df-int 3641 df-iun 3684 df-br 3790 df-opab 3844 df-mpt 3845 df-id 4055 df-iom 4339 df-xp 4376 df-rel 4377 df-cnv 4378 df-co 4379 df-dm 4380 df-rn 4381 df-res 4382 df-ima 4383 df-iota 4892 df-fun 4929 df-fn 4930 df-f 4931 df-f1 4932 df-fo 4933 df-f1o 4934 df-fv 4935 df-1st 5792 df-2nd 5793 df-qs 6140 df-ni 6430 df-nqqs 6474 df-inp 6592

This theorem is referenced by: addclpr 6663 mulclpr 6698 ltexprlempr 6734 recexprlempr 6758 cauappcvgprlemcl 6779 caucvgprlemcl 6802 caucvgprprlemcl 6830