Theorem isbnd3 37764

Description: A metric space is bounded iff the metric function maps to some bounded real interval. (Contributed by Mario Carneiro, 13-Sep-2015.)

Assertion

Ref	Expression
isbnd3	⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))

Distinct variable groups:   𝑥,𝑀   𝑥,𝑋

Proof of Theorem isbnd3

Dummy variables 𝑟 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bndmet 37761	. . 3 ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋))
2		0re 11117	. . . . . 6 ⊢ 0 ∈ ℝ
3	2	ne0ii 4295	. . . . 5 ⊢ ℝ ≠ ∅
4		metf 24216	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ)
5	4	ffnd 6653	. . . . . . . . 9 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 Fn (𝑋 × 𝑋))
6	1, 5	syl 17	. . . . . . . 8 ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 Fn (𝑋 × 𝑋))
7	6	ad2antrr 726	. . . . . . 7 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀 Fn (𝑋 × 𝑋))
8	1, 4	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ)
9	8	fdmd 6662	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (Bnd‘𝑋) → dom 𝑀 = (𝑋 × 𝑋))
10		xpeq2 5640	. . . . . . . . . . . 12 ⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = (𝑋 × ∅))
11		xp0 6107	. . . . . . . . . . . 12 ⊢ (𝑋 × ∅) = ∅
12	10, 11	eqtrdi 2780	. . . . . . . . . . 11 ⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = ∅)
13	9, 12	sylan9eq 2784	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → dom 𝑀 = ∅)
14	13	adantr 480	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → dom 𝑀 = ∅)
15		dm0rn0 5867	. . . . . . . . 9 ⊢ (dom 𝑀 = ∅ ↔ ran 𝑀 = ∅)
16	14, 15	sylib 218	. . . . . . . 8 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 = ∅)
17		0ss 4351	. . . . . . . 8 ⊢ ∅ ⊆ (0[,]𝑥)
18	16, 17	eqsstrdi 3980	. . . . . . 7 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 ⊆ (0[,]𝑥))
19		df-f 6486	. . . . . . 7 ⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ran 𝑀 ⊆ (0[,]𝑥)))
20	7, 18, 19	sylanbrc 583	. . . . . 6 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
21	20	ralrimiva 3121	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
22		r19.2z 4446	. . . . 5 ⊢ ((ℝ ≠ ∅ ∧ ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
23	3, 21, 22	sylancr 587	. . . 4 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
24		isbnd2 37763	. . . . . 6 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
25	24	simprbi 496	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
26		2re 12202	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
27		simprlr 779	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ+)
28	27	rpred 12937	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ)
29		remulcl 11094	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (2 · 𝑟) ∈ ℝ)
30	26, 28, 29	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → (2 · 𝑟) ∈ ℝ)
31	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀 Fn (𝑋 × 𝑋))
32		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑀 ∈ (Met‘𝑋))
33		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ 𝑋)
34		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ 𝑋)
35		metcl 24218	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝑀𝑧) ∈ ℝ)
36	32, 33, 34, 35	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ∈ ℝ)
37		metge0 24231	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝑥𝑀𝑧))
38	32, 33, 34, 37	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 0 ≤ (𝑥𝑀𝑧))
39	30	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (2 · 𝑟) ∈ ℝ)
40		simprll 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑦 ∈ 𝑋)
41	40	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
42		metcl 24218	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑦𝑀𝑥) ∈ ℝ)
43	32, 41, 33, 42	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑥) ∈ ℝ)
44		metcl 24218	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ ℝ)
45	32, 41, 34, 44	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑧) ∈ ℝ)
46	43, 45	readdcld 11144	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) ∈ ℝ)
47		mettri2 24227	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)))
48	32, 41, 33, 34, 47	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)))
49	28	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℝ)
50		simplrr 777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑋 = (𝑦(ball‘𝑀)𝑟))
51	33, 50	eleqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ (𝑦(ball‘𝑀)𝑟))
52		metxmet 24220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
53	32, 52	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑀 ∈ (∞Met‘𝑋))
54		rpxr 12903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
55	54	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → 𝑟 ∈ ℝ*)
56	55	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℝ*)
57		elbl2 24276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟))
58	53, 56, 41, 33, 57	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟))
59	51, 58	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑥) < 𝑟)
60	34, 50	eleqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ (𝑦(ball‘𝑀)𝑟))
61		elbl2 24276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟))
62	53, 56, 41, 34, 61	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟))
63	60, 62	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑧) < 𝑟)
64	43, 45, 49, 49, 59, 63	lt2addd 11743	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (𝑟 + 𝑟))
65	49	recnd 11143	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℂ)
66	65	2timesd 12367	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (2 · 𝑟) = (𝑟 + 𝑟))
67	64, 66	breqtrrd 5120	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (2 · 𝑟))
68	36, 46, 39, 48, 67	lelttrd 11274	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) < (2 · 𝑟))
69	36, 39, 68	ltled 11264	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ (2 · 𝑟))
70		elicc2 13314	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (2 · 𝑟) ∈ ℝ) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟))))
71	2, 39, 70	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟))))
72	36, 38, 69, 71	mpbir3and 1343	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))
73	72	ralrimivva 3172	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))
74		ffnov 7475	. . . . . . . . . . 11 ⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟))))
75	31, 73, 74	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)))
76		oveq2 7357	. . . . . . . . . . . 12 ⊢ (𝑥 = (2 · 𝑟) → (0[,]𝑥) = (0[,](2 · 𝑟)))
77	76	feq3d 6637	. . . . . . . . . . 11 ⊢ (𝑥 = (2 · 𝑟) → (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))))
78	77	rspcev 3577	. . . . . . . . . 10 ⊢ (((2 · 𝑟) ∈ ℝ ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
79	30, 75, 78	syl2anc 584	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
80	79	expr 456	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
81	80	rexlimdvva 3186	. . . . . . 7 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
82	1, 81	syl 17	. . . . . 6 ⊢ (𝑀 ∈ (Bnd‘𝑋) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
83	82	adantr 480	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
84	25, 83	mpd 15	. . . 4 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
85	23, 84	pm2.61dane 3012	. . 3 ⊢ (𝑀 ∈ (Bnd‘𝑋) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
86	1, 85	jca 511	. 2 ⊢ (𝑀 ∈ (Bnd‘𝑋) → (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
87		simpll 766	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Met‘𝑋))
88		simpllr 775	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ ℝ)
89	87	adantr 480	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀 ∈ (Met‘𝑋))
90		simpr 484	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
91		met0 24229	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) = 0)
92	89, 90, 91	syl2anc 584	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) = 0)
93		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
94	93, 90, 90	fovcdmd 7521	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) ∈ (0[,]𝑥))
95		elicc2 13314	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥)))
96	2, 88, 95	sylancr 587	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥)))
97	94, 96	mpbid 232	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥))
98	97	simp3d 1144	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) ≤ 𝑥)
99	92, 98	eqbrtrrd 5116	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 0 ≤ 𝑥)
100	88, 99	ge0p1rpd 12967	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ+)
101		fovcdm 7519	. . . . . . . . . . . . . 14 ⊢ ((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
102	101	3expa 1118	. . . . . . . . . . . . 13 ⊢ (((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
103	102	adantlll 718	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
104		elicc2 13314	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
105	2, 88, 104	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
107	103, 106	mpbid 232	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥))
108	107	simp1d 1142	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ ℝ)
109	88	adantr 480	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → 𝑥 ∈ ℝ)
110		peano2re 11289	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
111	88, 110	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ)
112	111	adantr 480	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ)
113	107	simp3d 1144	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ≤ 𝑥)
114	109	ltp1d 12055	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → 𝑥 < (𝑥 + 1))
115	108, 109, 112, 113, 114	lelttrd 11274	. . . . . . . . 9 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) < (𝑥 + 1))
116	115	ralrimiva 3121	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) < (𝑥 + 1))
117		rabid2 3428	. . . . . . . 8 ⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)} ↔ ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) < (𝑥 + 1))
118	116, 117	sylibr 234	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑋 = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
119	89, 52	syl 17	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀 ∈ (∞Met‘𝑋))
120	111	rexrd 11165	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ*)
121		blval 24272	. . . . . . . 8 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑥 + 1) ∈ ℝ*) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
122	119, 90, 120, 121	syl3anc 1373	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
123	118, 122	eqtr4d 2767	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1)))
124		oveq2 7357	. . . . . . 7 ⊢ (𝑟 = (𝑥 + 1) → (𝑦(ball‘𝑀)𝑟) = (𝑦(ball‘𝑀)(𝑥 + 1)))
125	124	rspceeqv 3600	. . . . . 6 ⊢ (((𝑥 + 1) ∈ ℝ+ ∧ 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1))) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
126	100, 123, 125	syl2anc 584	. . . . 5 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
127	126	ralrimiva 3121	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
128		isbnd 37760	. . . 4 ⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
129	87, 127, 128	sylanbrc 583	. . 3 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
130	129	r19.29an 3133	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
131	86, 130	impbii 209	1 ⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3394   ⊆ wss 3903  ∅c0 4284   class class class wbr 5092   × cxp 5617  dom cdm 5619  ran crn 5620   Fn wfn 6477  ⟶wf 6478  ‘cfv 6482  (class class class)co 7349  ℝcr 11008  0cc0 11009  1c1 11010   + caddc 11012   · cmul 11014  ℝ^*cxr 11148   < clt 11149   ≤ cle 11150  2c2 12183  ℝ⁺crp 12893  [,]cicc 13251  ∞Metcxmet 21246  Metcmet 21247  ballcbl 21248  Bndcbnd 37747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-ec 8627  df-map 8755  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-rp 12894  df-xneg 13014  df-xadd 13015  df-xmul 13016  df-icc 13255  df-psmet 21253  df-xmet 21254  df-met 21255  df-bl 21256  df-bnd 37759

This theorem is referenced by:  isbnd3b  37765  prdsbnd  37773