blbas - Intuitionistic Logic Explorer

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

Theorem blbas 12422

Description: The balls of a metric space form a basis for a topology. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 15-Jan-2014.)

**Assertion**
Ref	Expression
blbas

Proof of Theorem blbas Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		blin2 12421	. . . . . 6 $/\$ $/\$ $/\$
2		simpll 501	. . . . . . 7 $/\$ $/\$ $/\$
3		elinel1 3228	. . . . . . . . . 10
4		elunii 3707	. . . . . . . . . 10 $/\$
5	3, 4	sylan 279	. . . . . . . . 9 $/\$
6	5	ad2ant2lr 499	. . . . . . . 8 $/\$ $/\$ $/\$
7		unirnbl 12412	. . . . . . . . 9
8	7	ad2antrr 477	. . . . . . . 8 $/\$ $/\$ $/\$
9	6, 8	eleqtrd 2193	. . . . . . 7 $/\$ $/\$ $/\$
10		blssex 12419	. . . . . . 7 $/\$ $/\$
11	2, 9, 10	syl2anc 406	. . . . . 6 $/\$ $/\$ $/\$ $/\$
12	1, 11	mpbird 166	. . . . 5 $/\$ $/\$ $/\$ $/\$
13	12	ex 114	. . . 4 $/\$ $/\$ $/\$
14	13	ralrimdva 2486	. . 3 $/\$ $/\$
15	14	ralrimivv 2487	. 2 $/\$
16		blex 12376	. . 3
17		rnexg 4762	. . 3
18		isbasis2g 12055	. . 3 $/\$
19	16, 17, 18	3syl 17	. 2 $/\$
20	15, 19	mpbird 166	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1314

wcel 1463

wral 2390

wrex 2391

cvv 2657

cin 3036

wss 3037

cuni 3702

crn 4500

cfv 5081 (class class class)co 5728

crp 9343

cxmet 11992

cbl 11994

ctb 12052

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-coll 4003 ax-sep 4006 ax-nul 4014 ax-pow 4058 ax-pr 4091 ax-un 4315 ax-setind 4412 ax-iinf 4462 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 ax-caucvg 7665

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-nul 3330 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-tr 3987 df-id 4175 df-po 4178 df-iso 4179 df-iord 4248 df-on 4250 df-ilim 4251 df-suc 4253 df-iom 4465 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-f1 5086 df-fo 5087 df-f1o 5088 df-fv 5089 df-isom 5090 df-riota 5684 df-ov 5731 df-oprab 5732 df-mpo 5733 df-1st 5992 df-2nd 5993 df-recs 6156 df-frec 6242 df-map 6498 df-sup 6823 df-inf 6824 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-3 8690 df-4 8691 df-n0 8882 df-z 8959 df-uz 9229 df-q 9314 df-rp 9344 df-xneg 9452 df-xadd 9453 df-seqfrec 10112 df-exp 10186 df-cj 10507 df-re 10508 df-im 10509 df-rsqrt 10662 df-abs 10663 df-psmet 11999 df-xmet 12000 df-bl 12002 df-bases 12053

This theorem is referenced by: mopnval 12431 mopntopon 12432 elmopn 12435 blssopn 12474 metss 12483