Theorem isbnd3 35222

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 35219	. . 3 ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋))
2		0re 10632	. . . . . 6 ⊢ 0 ∈ ℝ
3	2	ne0ii 4253	. . . . 5 ⊢ ℝ ≠ ∅
4		metf 22937	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ)
5	4	ffnd 6488	. . . . . . . . 9 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 Fn (𝑋 × 𝑋))
6	1, 5	syl 17	. . . . . . . 8 ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 Fn (𝑋 × 𝑋))
7	6	ad2antrr 725	. . . . . . 7 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀 Fn (𝑋 × 𝑋))
8	1, 4	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ)
9	8	fdmd 6497	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (Bnd‘𝑋) → dom 𝑀 = (𝑋 × 𝑋))
10		xpeq2 5540	. . . . . . . . . . . 12 ⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = (𝑋 × ∅))
11		xp0 5982	. . . . . . . . . . . 12 ⊢ (𝑋 × ∅) = ∅
12	10, 11	eqtrdi 2849	. . . . . . . . . . 11 ⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = ∅)
13	9, 12	sylan9eq 2853	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → dom 𝑀 = ∅)
14	13	adantr 484	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → dom 𝑀 = ∅)
15		dm0rn0 5759	. . . . . . . . 9 ⊢ (dom 𝑀 = ∅ ↔ ran 𝑀 = ∅)
16	14, 15	sylib 221	. . . . . . . 8 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 = ∅)
17		0ss 4304	. . . . . . . 8 ⊢ ∅ ⊆ (0[,]𝑥)
18	16, 17	eqsstrdi 3969	. . . . . . 7 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 ⊆ (0[,]𝑥))
19		df-f 6328	. . . . . . 7 ⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ran 𝑀 ⊆ (0[,]𝑥)))
20	7, 18, 19	sylanbrc 586	. . . . . 6 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
21	20	ralrimiva 3149	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
22		r19.2z 4398	. . . . 5 ⊢ ((ℝ ≠ ∅ ∧ ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
23	3, 21, 22	sylancr 590	. . . 4 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
24		isbnd2 35221	. . . . . 6 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
25	24	simprbi 500	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
26		2re 11699	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
27		simprlr 779	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ+)
28	27	rpred 12419	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ)
29		remulcl 10611	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (2 · 𝑟) ∈ ℝ)
30	26, 28, 29	sylancr 590	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → (2 · 𝑟) ∈ ℝ)
31	5	adantr 484	. . . . . . . . . . 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 22939	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝑀𝑧) ∈ ℝ)
36	32, 33, 34, 35	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ∈ ℝ)
37		metge0 22952	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → 0 ≤ (𝑥𝑀𝑧))
38	32, 33, 34, 37	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 0 ≤ (𝑥𝑀𝑧))
39	30	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (2 · 𝑟) ∈ ℝ)
40		simprll 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑦 ∈ 𝑋)
41	40	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑦 ∈ 𝑋)
42		metcl 22939	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑦𝑀𝑥) ∈ ℝ)
43	32, 41, 33, 42	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑥) ∈ ℝ)
44		metcl 22939	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ ℝ)
45	32, 41, 34, 44	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑧) ∈ ℝ)
46	43, 45	readdcld 10659	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) ∈ ℝ)
47		mettri2 22948	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)))
48	32, 41, 33, 34, 47	syl13anc 1369	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)))
49	28	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℝ)
50		simplrr 777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑋 = (𝑦(ball‘𝑀)𝑟))
51	33, 50	eleqtrd 2892	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ (𝑦(ball‘𝑀)𝑟))
52		metxmet 22941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
53	32, 52	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑀 ∈ (∞Met‘𝑋))
54		rpxr 12386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
55	54	ad2antlr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → 𝑟 ∈ ℝ*)
56	55	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℝ*)
57		elbl2 22997	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟))
58	53, 56, 41, 33, 57	syl22anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑥) < 𝑟))
59	51, 58	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑥) < 𝑟)
60	34, 50	eleqtrd 2892	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ (𝑦(ball‘𝑀)𝑟))
61		elbl2 22997	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟))
62	53, 56, 41, 34, 61	syl22anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑧 ∈ (𝑦(ball‘𝑀)𝑟) ↔ (𝑦𝑀𝑧) < 𝑟))
63	60, 62	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑧) < 𝑟)
64	43, 45, 49, 49, 59, 63	lt2addd 11252	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (𝑟 + 𝑟))
65	49	recnd 10658	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℂ)
66	65	2timesd 11868	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (2 · 𝑟) = (𝑟 + 𝑟))
67	64, 66	breqtrrd 5058	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (2 · 𝑟))
68	36, 46, 39, 48, 67	lelttrd 10787	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) < (2 · 𝑟))
69	36, 39, 68	ltled 10777	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ (2 · 𝑟))
70		elicc2 12790	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ (2 · 𝑟) ∈ ℝ) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟))))
71	2, 39, 70	sylancr 590	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)) ↔ ((𝑥𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑥𝑀𝑧) ∧ (𝑥𝑀𝑧) ≤ (2 · 𝑟))))
72	36, 38, 69, 71	mpbir3and 1339	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))
73	72	ralrimivva 3156	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))
74		ffnov 7257	. . . . . . . . . . 11 ⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟))))
75	31, 73, 74	sylanbrc 586	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)))
76		oveq2 7143	. . . . . . . . . . . 12 ⊢ (𝑥 = (2 · 𝑟) → (0[,]𝑥) = (0[,](2 · 𝑟)))
77	76	feq3d 6474	. . . . . . . . . . 11 ⊢ (𝑥 = (2 · 𝑟) → (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))))
78	77	rspcev 3571	. . . . . . . . . 10 ⊢ (((2 · 𝑟) ∈ ℝ ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
79	30, 75, 78	syl2anc 587	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
80	79	expr 460	. . . . . . . 8 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ (𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+)) → (𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
81	80	rexlimdvva 3253	. . . . . . 7 ⊢ (𝑀 ∈ (Met‘𝑋) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
82	1, 81	syl 17	. . . . . 6 ⊢ (𝑀 ∈ (Bnd‘𝑋) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
83	82	adantr 484	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → (∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
84	25, 83	mpd 15	. . . 4 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
85	23, 84	pm2.61dane 3074	. . 3 ⊢ (𝑀 ∈ (Bnd‘𝑋) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
86	1, 85	jca 515	. 2 ⊢ (𝑀 ∈ (Bnd‘𝑋) → (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))
87		simpll 766	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Met‘𝑋))
88		simpllr 775	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑥 ∈ ℝ)
89	87	adantr 484	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀 ∈ (Met‘𝑋))
90		simpr 488	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋)
91		met0 22950	. . . . . . . . 9 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) = 0)
92	89, 90, 91	syl2anc 587	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) = 0)
93		simplr 768	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
94	93, 90, 90	fovrnd 7300	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) ∈ (0[,]𝑥))
95		elicc2 12790	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥)))
96	2, 88, 95	sylancr 590	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑦) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥)))
97	94, 96	mpbid 235	. . . . . . . . 9 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑦) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑦) ∧ (𝑦𝑀𝑦) ≤ 𝑥))
98	97	simp3d 1141	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) ≤ 𝑥)
99	92, 98	eqbrtrrd 5054	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 0 ≤ 𝑥)
100	88, 99	ge0p1rpd 12449	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ+)
101		fovrn 7298	. . . . . . . . . . . . . 14 ⊢ ((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
102	101	3expa 1115	. . . . . . . . . . . . 13 ⊢ (((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
103	102	adantlll 717	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
104		elicc2 12790	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
105	2, 88, 104	sylancr 590	. . . . . . . . . . . . 13 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
106	105	adantr 484	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ (0[,]𝑥) ↔ ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥)))
107	103, 106	mpbid 235	. . . . . . . . . . 11 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → ((𝑦𝑀𝑧) ∈ ℝ ∧ 0 ≤ (𝑦𝑀𝑧) ∧ (𝑦𝑀𝑧) ≤ 𝑥))
108	107	simp1d 1139	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ ℝ)
109	88	adantr 484	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → 𝑥 ∈ ℝ)
110		peano2re 10802	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
111	88, 110	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ)
112	111	adantr 484	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ)
113	107	simp3d 1141	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ≤ 𝑥)
114	109	ltp1d 11559	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → 𝑥 < (𝑥 + 1))
115	108, 109, 112, 113, 114	lelttrd 10787	. . . . . . . . 9 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) < (𝑥 + 1))
116	115	ralrimiva 3149	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) < (𝑥 + 1))
117		rabid2 3334	. . . . . . . 8 ⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)} ↔ ∀𝑧 ∈ 𝑋 (𝑦𝑀𝑧) < (𝑥 + 1))
118	116, 117	sylibr 237	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑋 = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
119	89, 52	syl 17	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑀 ∈ (∞Met‘𝑋))
120	111	rexrd 10680	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ*)
121		blval 22993	. . . . . . . 8 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑥 + 1) ∈ ℝ*) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
122	119, 90, 120, 121	syl3anc 1368	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
123	118, 122	eqtr4d 2836	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1)))
124		oveq2 7143	. . . . . . 7 ⊢ (𝑟 = (𝑥 + 1) → (𝑦(ball‘𝑀)𝑟) = (𝑦(ball‘𝑀)(𝑥 + 1)))
125	124	rspceeqv 3586	. . . . . 6 ⊢ (((𝑥 + 1) ∈ ℝ+ ∧ 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1))) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
126	100, 123, 125	syl2anc 587	. . . . 5 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
127	126	ralrimiva 3149	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
128		isbnd 35218	. . . 4 ⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
129	87, 127, 128	sylanbrc 586	. . 3 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
130	129	r19.29an 3247	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
131	86, 130	impbii 212	1 ⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110   ⊆ wss 3881  ∅c0 4243   class class class wbr 5030   × cxp 5517  dom cdm 5519  ran crn 5520   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  ℝ^*cxr 10663   < clt 10664   ≤ cle 10665  2c2 11680  ℝ⁺crp 12377  [,]cicc 12729  ∞Metcxmet 20076  Metcmet 20077  ballcbl 20078  Bndcbnd 35205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-po 5438  df-so 5439  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-er 8272  df-ec 8274  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-2 11688  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-icc 12733  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-bnd 35217

This theorem is referenced by:  isbnd3b  35223  prdsbnd  35231