elnp1st2nd - Intuitionistic Logic Explorer

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

Theorem elnp1st2nd 6798

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 6793	. . . . 5
2	1	sseli 3004	. . . 4
3		prop 6797	. . . . . . 7
4		elinp 6796	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
5	3, 4	sylib 120	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
6	5	simpld 110	. . . . 5 $/\$ $/\$ $/\$
7	6	simprd 112	. . . 4 $/\$
8	2, 7	jca 300	. . 3 $/\$ $/\$
9	5	simprd 112	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
10	8, 9	jca 300	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
11		1st2nd2 5853	. . . 4
12	11	ad2antrr 472	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
13		xp1st 5844	. . . . . . . 8
14	13	elpwid 3410	. . . . . . 7
15		xp2nd 5845	. . . . . . . 8
16	15	elpwid 3410	. . . . . . 7
17	14, 16	jca 300	. . . . . 6 $/\$
18	17	anim1i 333	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
19	18	anim1i 333	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
20	19, 4	sylibr 132	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
21	12, 20	eqeltrd 2159	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
22	10, 21	impbii 124	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 102

wb 103 $\/$ wo 662 $/\$ w3a 920

wceq 1285

wcel 1434

wral 2353

wrex 2354

wss 2982

cpw 3400

cop 3419 class class class wbr 3805

cxp 4389

cfv 4952

c1st 5817

c2nd 5818

cnq 6602

cltq 6607

cnp 6613

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-coll 3913 ax-sep 3916 ax-pow 3968 ax-pr 3992 ax-un 4216 ax-iinf 4357

This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-reu 2360 df-rab 2362 df-v 2612 df-sbc 2825 df-csb 2918 df-dif 2984 df-un 2986 df-in 2988 df-ss 2995 df-pw 3402 df-sn 3422 df-pr 3423 df-op 3425 df-uni 3622 df-int 3657 df-iun 3700 df-br 3806 df-opab 3860 df-mpt 3861 df-id 4076 df-iom 4360 df-xp 4397 df-rel 4398 df-cnv 4399 df-co 4400 df-dm 4401 df-rn 4402 df-res 4403 df-ima 4404 df-iota 4917 df-fun 4954 df-fn 4955 df-f 4956 df-f1 4957 df-fo 4958 df-f1o 4959 df-fv 4960 df-1st 5819 df-2nd 5820 df-qs 6200 df-ni 6626 df-nqqs 6670 df-inp 6788

This theorem is referenced by: addclpr 6859 mulclpr 6894 ltexprlempr 6930 recexprlempr 6954 cauappcvgprlemcl 6975 caucvgprlemcl 6998 caucvgprprlemcl 7026