prloc - Intuitionistic Logic Explorer

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

Theorem prloc 7113

Description: A Dedekind cut is located. (Contributed by Jim Kingdon, 23-Oct-2019.)

**Assertion**
Ref	Expression
prloc	$/\$ $\/$

Proof of Theorem prloc Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elinp 7096	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
2		simpr3 952	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
3	1, 2	sylbi 120	. . 3 $\/$
4	3	adantr 271	. 2 $/\$ $\/$
5		simpr 109	. 2 $/\$
6		ltrelnq 6987	. . . . . . 7
7	6	brel 4505	. . . . . 6 $/\$
8	7	simpld 111	. . . . 5
9	8	adantl 272	. . . 4 $/\$
10		simpr 109	. . . . . . 7 $/\$ $/\$
11	10	breq1d 3863	. . . . . 6 $/\$ $/\$
12	10	eleq1d 2157	. . . . . . 7 $/\$ $/\$
13	12	orbi1d 741	. . . . . 6 $/\$ $/\$ $\/$ $\/$
14	11, 13	imbi12d 233	. . . . 5 $/\$ $/\$ $\/$ $\/$
15	14	ralbidv 2381	. . . 4 $/\$ $/\$ $\/$ $\/$
16	9, 15	rspcdv 2728	. . 3 $/\$ $\/$ $\/$
17	7	simprd 113	. . . . 5
18	17	adantl 272	. . . 4 $/\$
19		simpr 109	. . . . . 6 $/\$ $/\$
20	19	breq2d 3865	. . . . 5 $/\$ $/\$
21	19	eleq1d 2157	. . . . . 6 $/\$ $/\$
22	21	orbi2d 740	. . . . 5 $/\$ $/\$ $\/$ $\/$
23	20, 22	imbi12d 233	. . . 4 $/\$ $/\$ $\/$ $\/$
24	18, 23	rspcdv 2728	. . 3 $/\$ $\/$ $\/$
25	16, 24	syld 45	. 2 $/\$ $\/$ $\/$
26	4, 5, 25	mp2d 47	1 $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 665 $/\$ w3a 925

wceq 1290

wcel 1439

wral 2360

wrex 2361

wss 3002

cop 3455 class class class wbr 3853

cnq 6902

cltq 6907

cnp 6913

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-13 1450 ax-14 1451 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-coll 3962 ax-sep 3965 ax-pow 4017 ax-pr 4047 ax-un 4271 ax-iinf 4418

This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-eu 1952 df-mo 1953 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-rex 2366 df-reu 2367 df-rab 2369 df-v 2624 df-sbc 2844 df-csb 2937 df-dif 3004 df-un 3006 df-in 3008 df-ss 3015 df-pw 3437 df-sn 3458 df-pr 3459 df-op 3461 df-uni 3662 df-int 3697 df-iun 3740 df-br 3854 df-opab 3908 df-mpt 3909 df-id 4131 df-iom 4421 df-xp 4460 df-rel 4461 df-cnv 4462 df-co 4463 df-dm 4464 df-rn 4465 df-res 4466 df-ima 4467 df-iota 4995 df-fun 5032 df-fn 5033 df-f 5034 df-f1 5035 df-fo 5036 df-f1o 5037 df-fv 5038 df-qs 6314 df-ni 6926 df-nqqs 6970 df-ltnqqs 6975 df-inp 7088