elnp1st2nd - Intuitionistic Logic Explorer

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

Theorem elnp1st2nd 7695

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 7690	. . . . 5
2	1	sseli 3223	. . . 4
3		prop 7694	. . . . . . 7
4		elinp 7693	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
5	3, 4	sylib 122	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
6	5	simpld 112	. . . . 5 $/\$ $/\$ $/\$
7	6	simprd 114	. . . 4 $/\$
8	2, 7	jca 306	. . 3 $/\$ $/\$
9	5	simprd 114	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
10	8, 9	jca 306	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
11		1st2nd2 6337	. . . 4
12	11	ad2antrr 488	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
13		xp1st 6327	. . . . . . . 8
14	13	elpwid 3663	. . . . . . 7
15		xp2nd 6328	. . . . . . . 8
16	15	elpwid 3663	. . . . . . 7
17	14, 16	jca 306	. . . . . 6 $/\$
18	17	anim1i 340	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
19	18	anim1i 340	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
20	19, 4	sylibr 134	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
21	12, 20	eqeltrd 2308	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
22	10, 21	impbii 126	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 715 $/\$ w3a 1004

wceq 1397

wcel 2202

wral 2510

wrex 2511

wss 3200

cpw 3652

cop 3672 class class class wbr 4088

cxp 4723

cfv 5326

c1st 6300

c2nd 6301

cnq 7499

cltq 7504

cnp 7510

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-iinf 4686

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-reu 2517 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-id 4390 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-1st 6302 df-2nd 6303 df-qs 6707 df-ni 7523 df-nqqs 7567 df-inp 7685

This theorem is referenced by: addclpr 7756 mulclpr 7791 ltexprlempr 7827 recexprlempr 7851 cauappcvgprlemcl 7872 caucvgprlemcl 7895 caucvgprprlemcl 7923