blssex - Intuitionistic Logic Explorer

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

Theorem blssex 14692

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 14690	. . . . . . 7 $/\$ $/\$
2		sstr 3192	. . . . . . . . 9 $/\$
3	2	expcom 116	. . . . . . . 8
4	3	reximdv 2598	. . . . . . 7
5	1, 4	syl5com 29	. . . . . 6 $/\$ $/\$
6	5	3expa 1205	. . . . 5 $/\$ $/\$
7	6	expimpd 363	. . . 4 $/\$ $/\$
8	7	adantlr 477	. . 3 $/\$ $/\$ $/\$
9	8	rexlimdva 2614	. 2 $/\$ $/\$
10		simpll 527	. . . . 5 $/\$ $/\$ $/\$
11		simplr 528	. . . . 5 $/\$ $/\$ $/\$
12		rpxr 9739	. . . . . 6
13	12	ad2antrl 490	. . . . 5 $/\$ $/\$ $/\$
14		blelrn 14682	. . . . 5 $/\$ $/\$
15	10, 11, 13, 14	syl3anc 1249	. . . 4 $/\$ $/\$ $/\$
16		simprl 529	. . . . 5 $/\$ $/\$ $/\$
17		blcntr 14678	. . . . 5 $/\$ $/\$
18	10, 11, 16, 17	syl3anc 1249	. . . 4 $/\$ $/\$ $/\$
19		simprr 531	. . . 4 $/\$ $/\$ $/\$
20		eleq2 2260	. . . . . 6
21		sseq1 3207	. . . . . 6
22	20, 21	anbi12d 473	. . . . 5 $/\$ $/\$
23	22	rspcev 2868	. . . 4 $/\$ $/\$ $/\$
24	15, 18, 19, 23	syl12anc 1247	. . 3 $/\$ $/\$ $/\$ $/\$
25	24	rexlimdvaa 2615	. 2 $/\$ $/\$
26	9, 25	impbid 129	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 980

wceq 1364

wcel 2167

wrex 2476

wss 3157

crn 4665

cfv 5259 (class class class)co 5923

cxr 8063

crp 9731

cxmet 14118

cbl 14120

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-cnex 7973 ax-resscn 7974 ax-1cn 7975 ax-1re 7976 ax-icn 7977 ax-addcl 7978 ax-addrcl 7979 ax-mulcl 7980 ax-mulrcl 7981 ax-addcom 7982 ax-mulcom 7983 ax-addass 7984 ax-mulass 7985 ax-distr 7986 ax-i2m1 7987 ax-0lt1 7988 ax-1rid 7989 ax-0id 7990 ax-rnegex 7991 ax-precex 7992 ax-cnre 7993 ax-pre-ltirr 7994 ax-pre-ltwlin 7995 ax-pre-lttrn 7996 ax-pre-apti 7997 ax-pre-ltadd 7998 ax-pre-mulgt0 7999 ax-pre-mulext 8000 ax-arch 8001

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-id 4329 df-po 4332 df-iso 4333 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-fv 5267 df-riota 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-1st 6200 df-2nd 6201 df-map 6711 df-pnf 8066 df-mnf 8067 df-xr 8068 df-ltxr 8069 df-le 8070 df-sub 8202 df-neg 8203 df-reap 8605 df-ap 8612 df-div 8703 df-inn 8994 df-2 9052 df-n0 9253 df-z 9330 df-uz 9605 df-q 9697 df-rp 9732 df-xneg 9850 df-xadd 9851 df-psmet 14125 df-xmet 14126 df-bl 14128

This theorem is referenced by: blbas 14695 elmopn2 14711 mopni2 14745 metss 14756 tgioo 14816