bdmopn - Intuitionistic Logic Explorer

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

Theorem bdmopn 12493

Description: The standard bounded metric corresponding to 𝐶 generates the same topology as 𝐶. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)

**Hypotheses**
Ref	Expression
stdbdmet.1	⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ^*, < ))
stdbdmopn.2	⊢ 𝐽 = (MetOpen‘𝐶)

**Assertion**
Ref	Expression
bdmopn	⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) → 𝐽 = (MetOpen‘𝐷))

Distinct variable groups: 𝑥,𝑦,𝐶 𝑥,𝑅,𝑦 𝑥,𝑋,𝑦 Allowed substitution hints: 𝐷(𝑥,𝑦) 𝐽(𝑥,𝑦)

Proof of Theorem bdmopn Dummy variables 𝑟 𝑠 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpxr 9350	. . . . . . . 8 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
2	1	ad2antll 480	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 𝑟 ∈ ℝ^*)
3		simpl2 968	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 𝑅 ∈ ℝ^*)
4		xrmincl 10927	. . . . . . 7 ⊢ ((𝑟 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^) → inf({𝑟, 𝑅}, ℝ^, < ) ∈ ℝ^*)
5	2, 3, 4	syl2anc 406	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → inf({𝑟, 𝑅}, ℝ^, < ) ∈ ℝ^)
6		rpre 9349	. . . . . . 7 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ)
7	6	ad2antll 480	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 𝑟 ∈ ℝ)
8		0xr 7736	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
9	8	a1i 9	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 0 ∈ ℝ^*)
10		rpgt0 9354	. . . . . . . . 9 ⊢ (𝑟 ∈ ℝ⁺ → 0 < 𝑟)
11	10	ad2antll 480	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 0 < 𝑟)
12		simpl3 969	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 0 < 𝑅)
13		xrltmininf 10931	. . . . . . . . 9 ⊢ ((0 ∈ ℝ^* ∧ 𝑟 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^) → (0 < inf({𝑟, 𝑅}, ℝ^, < ) ↔ (0 < 𝑟 ∧ 0 < 𝑅)))
14	8, 2, 3, 13	mp3an2i 1303	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → (0 < inf({𝑟, 𝑅}, ℝ^*, < ) ↔ (0 < 𝑟 ∧ 0 < 𝑅)))
15	11, 12, 14	mpbir2and 911	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 0 < inf({𝑟, 𝑅}, ℝ^*, < ))
16	9, 5, 15	xrltled 9478	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 0 ≤ inf({𝑟, 𝑅}, ℝ^*, < ))
17		xrmin1inf 10928	. . . . . . 7 ⊢ ((𝑟 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^) → inf({𝑟, 𝑅}, ℝ^, < ) ≤ 𝑟)
18	2, 3, 17	syl2anc 406	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → inf({𝑟, 𝑅}, ℝ^*, < ) ≤ 𝑟)
19		xrrege0 9501	. . . . . 6 ⊢ (((inf({𝑟, 𝑅}, ℝ^, < ) ∈ ℝ^ ∧ 𝑟 ∈ ℝ) ∧ (0 ≤ inf({𝑟, 𝑅}, ℝ^, < ) ∧ inf({𝑟, 𝑅}, ℝ^, < ) ≤ 𝑟)) → inf({𝑟, 𝑅}, ℝ^*, < ) ∈ ℝ)
20	5, 7, 16, 18, 19	syl22anc 1200	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → inf({𝑟, 𝑅}, ℝ^*, < ) ∈ ℝ)
21	20, 15	elrpd 9380	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → inf({𝑟, 𝑅}, ℝ^*, < ) ∈ ℝ⁺)
22		simprl 503	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → 𝑧 ∈ 𝑋)
23		xrmin2inf 10929	. . . . . . . 8 ⊢ ((𝑟 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^) → inf({𝑟, 𝑅}, ℝ^, < ) ≤ 𝑅)
24	2, 3, 23	syl2anc 406	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → inf({𝑟, 𝑅}, ℝ^*, < ) ≤ 𝑅)
25	22, 5, 24	3jca 1144	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → (𝑧 ∈ 𝑋 ∧ inf({𝑟, 𝑅}, ℝ^, < ) ∈ ℝ^ ∧ inf({𝑟, 𝑅}, ℝ^*, < ) ≤ 𝑅))
26		stdbdmet.1	. . . . . . 7 ⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ^*, < ))
27	26	bdbl 12492	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ inf({𝑟, 𝑅}, ℝ^, < ) ∈ ℝ^ ∧ inf({𝑟, 𝑅}, ℝ^, < ) ≤ 𝑅)) → (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ^, < )) = (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ^*, < )))
28	25, 27	syldan 278	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ^, < )) = (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ^, < )))
29	28	eqcomd 2120	. . . 4 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ^, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ^, < )))
30		breq1 3898	. . . . . 6 ⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ^, < ) → (𝑠 ≤ 𝑟 ↔ inf({𝑟, 𝑅}, ℝ^, < ) ≤ 𝑟))
31		oveq2 5736	. . . . . . 7 ⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ^, < ) → (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ^, < )))
32		oveq2 5736	. . . . . . 7 ⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ^, < ) → (𝑧(ball‘𝐷)𝑠) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ^, < )))
33	31, 32	eqeq12d 2129	. . . . . 6 ⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ^, < ) → ((𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠) ↔ (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ^, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ^*, < ))))
34	30, 33	anbi12d 462	. . . . 5 ⊢ (𝑠 = inf({𝑟, 𝑅}, ℝ^, < ) → ((𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) ↔ (inf({𝑟, 𝑅}, ℝ^, < ) ≤ 𝑟 ∧ (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ^, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ^, < )))))
35	34	rspcev 2760	. . . 4 ⊢ ((inf({𝑟, 𝑅}, ℝ^, < ) ∈ ℝ⁺ ∧ (inf({𝑟, 𝑅}, ℝ^, < ) ≤ 𝑟 ∧ (𝑧(ball‘𝐶)inf({𝑟, 𝑅}, ℝ^, < )) = (𝑧(ball‘𝐷)inf({𝑟, 𝑅}, ℝ^, < )))) → ∃𝑠 ∈ ℝ⁺ (𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)))
36	21, 18, 29, 35	syl12anc 1197	. . 3 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) ∧ (𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺)) → ∃𝑠 ∈ ℝ⁺ (𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)))
37	36	ralrimivva 2488	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) → ∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ (𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)))
38		simp1 964	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) → 𝐶 ∈ (∞Met‘𝑋))
39	26	bdxmet 12490	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) → 𝐷 ∈ (∞Met‘𝑋))
40		stdbdmopn.2	. . . 4 ⊢ 𝐽 = (MetOpen‘𝐶)
41		eqid 2115	. . . 4 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
42	40, 41	metequiv2 12485	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ (𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) → 𝐽 = (MetOpen‘𝐷)))
43	38, 39, 42	syl2anc 406	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) → (∀𝑧 ∈ 𝑋 ∀𝑟 ∈ ℝ⁺ ∃𝑠 ∈ ℝ⁺ (𝑠 ≤ 𝑟 ∧ (𝑧(ball‘𝐶)𝑠) = (𝑧(ball‘𝐷)𝑠)) → 𝐽 = (MetOpen‘𝐷)))
44	37, 43	mpd 13	1 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅) → 𝐽 = (MetOpen‘𝐷))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 945 = wceq 1314 ∈ wcel 1463 ∀wral 2390 ∃wrex 2391 {cpr 3494 class class class wbr 3895 ‘cfv 5081 (class class class)co 5728 ∈ cmpo 5730 infcinf 6822 ℝcr 7546 0cc0 7547 ℝ^*cxr 7723 < clt 7724 ≤ cle 7725 ℝ⁺crp 9343 ∞Metcxmet 11992 ballcbl 11994 MetOpencmopn 11997

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-icc 9571 df-seqfrec 10112 df-exp 10186 df-cj 10507 df-re 10508 df-im 10509 df-rsqrt 10662 df-abs 10663 df-topgen 11984 df-psmet 11999 df-xmet 12000 df-bl 12002 df-mopn 12003 df-top 12008 df-bases 12053

This theorem is referenced by: mopnex 12494

W3C validator