blssex - Intuitionistic Logic Explorer

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

Theorem blssex 12419

Description: Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)

**Assertion**
Ref	Expression
blssex	$/\$ $/\$

**Proof of Theorem blssex**
Step	Hyp	Ref	Expression
1		blss 12417	. . . . . . 7 $/\$ $/\$
2		sstr 3071	. . . . . . . . 9 $/\$
3	2	expcom 115	. . . . . . . 8
4	3	reximdv 2507	. . . . . . 7
5	1, 4	syl5com 29	. . . . . 6 $/\$ $/\$
6	5	3expa 1164	. . . . 5 $/\$ $/\$
7	6	expimpd 358	. . . 4 $/\$ $/\$
8	7	adantlr 466	. . 3 $/\$ $/\$ $/\$
9	8	rexlimdva 2523	. 2 $/\$ $/\$
10		simpll 501	. . . . 5 $/\$ $/\$ $/\$
11		simplr 502	. . . . 5 $/\$ $/\$ $/\$
12		rpxr 9350	. . . . . 6
13	12	ad2antrl 479	. . . . 5 $/\$ $/\$ $/\$
14		blelrn 12409	. . . . 5 $/\$ $/\$
15	10, 11, 13, 14	syl3anc 1199	. . . 4 $/\$ $/\$ $/\$
16		simprl 503	. . . . 5 $/\$ $/\$ $/\$
17		blcntr 12405	. . . . 5 $/\$ $/\$
18	10, 11, 16, 17	syl3anc 1199	. . . 4 $/\$ $/\$ $/\$
19		simprr 504	. . . 4 $/\$ $/\$ $/\$
20		eleq2 2178	. . . . . 6
21		sseq1 3086	. . . . . 6
22	20, 21	anbi12d 462	. . . . 5 $/\$ $/\$
23	22	rspcev 2760	. . . 4 $/\$ $/\$ $/\$
24	15, 18, 19, 23	syl12anc 1197	. . 3 $/\$ $/\$ $/\$ $/\$
25	24	rexlimdvaa 2524	. 2 $/\$ $/\$
26	9, 25	impbid 128	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $/\$ w3a 945

wceq 1314

wcel 1463

wrex 2391

wss 3037

crn 4500

cfv 5081 (class class class)co 5728

cxr 7723

crp 9343

cxmet 11992

cbl 11994

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 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-13 1474 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-pow 4058 ax-pr 4091 ax-un 4315 ax-setind 4412 ax-cnex 7636 ax-resscn 7637 ax-1cn 7638 ax-1re 7639 ax-icn 7640 ax-addcl 7641 ax-addrcl 7642 ax-mulcl 7643 ax-mulrcl 7644 ax-addcom 7645 ax-mulcom 7646 ax-addass 7647 ax-mulass 7648 ax-distr 7649 ax-i2m1 7650 ax-0lt1 7651 ax-1rid 7652 ax-0id 7653 ax-rnegex 7654 ax-precex 7655 ax-cnre 7656 ax-pre-ltirr 7657 ax-pre-ltwlin 7658 ax-pre-lttrn 7659 ax-pre-apti 7660 ax-pre-ltadd 7661 ax-pre-mulgt0 7662 ax-pre-mulext 7663 ax-arch 7664

This theorem depends on definitions: df-bi 116 df-stab 799 df-dc 803 df-3or 946 df-3an 947 df-tru 1317 df-fal 1320 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ne 2283 df-nel 2378 df-ral 2395 df-rex 2396 df-reu 2397 df-rmo 2398 df-rab 2399 df-v 2659 df-sbc 2879 df-csb 2972 df-dif 3039 df-un 3041 df-in 3043 df-ss 3050 df-if 3441 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-int 3738 df-iun 3781 df-br 3896 df-opab 3950 df-mpt 3951 df-id 4175 df-po 4178 df-iso 4179 df-xp 4505 df-rel 4506 df-cnv 4507 df-co 4508 df-dm 4509 df-rn 4510 df-res 4511 df-ima 4512 df-iota 5046 df-fun 5083 df-fn 5084 df-f 5085 df-fv 5089 df-riota 5684 df-ov 5731 df-oprab 5732 df-mpo 5733 df-1st 5992 df-2nd 5993 df-map 6498 df-pnf 7726 df-mnf 7727 df-xr 7728 df-ltxr 7729 df-le 7730 df-sub 7858 df-neg 7859 df-reap 8255 df-ap 8262 df-div 8346 df-inn 8631 df-2 8689 df-n0 8882 df-z 8959 df-uz 9229 df-q 9314 df-rp 9344 df-xneg 9452 df-xadd 9453 df-psmet 11999 df-xmet 12000 df-bl 12002

This theorem is referenced by: blbas 12422 elmopn2 12438 mopni2 12472 metss 12483 tgioo 12532