Theorem isbnd3 37824

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 37821	. . 3 ⊢ (𝑀 ∈ (Bnd‘𝑋) → 𝑀 ∈ (Met‘𝑋))
2		0re 11109	. . . . . 6 ⊢ 0 ∈ ℝ
3	2	ne0ii 4289	. . . . 5 ⊢ ℝ ≠ ∅
4		metf 24240	. . . . . . . . . 10 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ)
5	4	ffnd 6647	. . . . . . . . 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 6656	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (Bnd‘𝑋) → dom 𝑀 = (𝑋 × 𝑋))
10		xpeq2 5632	. . . . . . . . . . . 12 ⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = (𝑋 × ∅))
11		xp0 6100	. . . . . . . . . . . 12 ⊢ (𝑋 × ∅) = ∅
12	10, 11	eqtrdi 2782	. . . . . . . . . . 11 ⊢ (𝑋 = ∅ → (𝑋 × 𝑋) = ∅)
13	9, 12	sylan9eq 2786	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → dom 𝑀 = ∅)
14	13	adantr 480	. . . . . . . . 9 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → dom 𝑀 = ∅)
15		dm0rn0 5859	. . . . . . . . 9 ⊢ (dom 𝑀 = ∅ ↔ ran 𝑀 = ∅)
16	14, 15	sylib 218	. . . . . . . 8 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 = ∅)
17		0ss 4345	. . . . . . . 8 ⊢ ∅ ⊆ (0[,]𝑥)
18	16, 17	eqsstrdi 3974	. . . . . . 7 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → ran 𝑀 ⊆ (0[,]𝑥))
19		df-f 6480	. . . . . . 7 ⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ran 𝑀 ⊆ (0[,]𝑥)))
20	7, 18, 19	sylanbrc 583	. . . . . 6 ⊢ (((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) ∧ 𝑥 ∈ ℝ) → 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
21	20	ralrimiva 3124	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
22		r19.2z 4440	. . . . 5 ⊢ ((ℝ ≠ ∅ ∧ ∀𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
23	3, 21, 22	sylancr 587	. . . 4 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 = ∅) → ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥))
24		isbnd2 37823	. . . . . 6 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) ↔ (𝑀 ∈ (∞Met‘𝑋) ∧ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
25	24	simprbi 496	. . . . 5 ⊢ ((𝑀 ∈ (Bnd‘𝑋) ∧ 𝑋 ≠ ∅) → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
26		2re 12194	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
27		simprlr 779	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ+)
28	27	rpred 12929	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑟 ∈ ℝ)
29		remulcl 11086	. . . . . . . . . . 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 24242	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑥𝑀𝑧) ∈ ℝ)
36	32, 33, 34, 35	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ∈ ℝ)
37		metge0 24255	. . . . . . . . . . . . . 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 24242	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑦𝑀𝑥) ∈ ℝ)
43	32, 41, 33, 42	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑥) ∈ ℝ)
44		metcl 24242	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ ℝ)
45	32, 41, 34, 44	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦𝑀𝑧) ∈ ℝ)
46	43, 45	readdcld 11136	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) ∈ ℝ)
47		mettri2 24251	. . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑥 ∈ (𝑦(ball‘𝑀)𝑟))
52		metxmet 24244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (Met‘𝑋) → 𝑀 ∈ (∞Met‘𝑋))
53	32, 52	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑀 ∈ (∞Met‘𝑋))
54		rpxr 12895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
55	54	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟)) → 𝑟 ∈ ℝ*)
56	55	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℝ*)
57		elbl2 24300	. . . . . . . . . . . . . . . . . . 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 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑧 ∈ (𝑦(ball‘𝑀)𝑟))
61		elbl2 24300	. . . . . . . . . . . . . . . . . . 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 11735	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (𝑟 + 𝑟))
65	49	recnd 11135	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → 𝑟 ∈ ℂ)
66	65	2timesd 12359	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (2 · 𝑟) = (𝑟 + 𝑟))
67	64, 66	breqtrrd 5114	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((𝑦𝑀𝑥) + (𝑦𝑀𝑧)) < (2 · 𝑟))
68	36, 46, 39, 48, 67	lelttrd 11266	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) < (2 · 𝑟))
69	36, 39, 68	ltled 11256	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥𝑀𝑧) ≤ (2 · 𝑟))
70		elicc2 13306	. . . . . . . . . . . . . 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 3175	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟)))
74		ffnov 7467	. . . . . . . . . . 11 ⊢ (𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)) ↔ (𝑀 Fn (𝑋 × 𝑋) ∧ ∀𝑥 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑥𝑀𝑧) ∈ (0[,](2 · 𝑟))))
75	31, 73, 74	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ((𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ 𝑋 = (𝑦(ball‘𝑀)𝑟))) → 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟)))
76		oveq2 7349	. . . . . . . . . . . 12 ⊢ (𝑥 = (2 · 𝑟) → (0[,]𝑥) = (0[,](2 · 𝑟)))
77	76	feq3d 6631	. . . . . . . . . . 11 ⊢ (𝑥 = (2 · 𝑟) → (𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ↔ 𝑀:(𝑋 × 𝑋)⟶(0[,](2 · 𝑟))))
78	77	rspcev 3572	. . . . . . . . . 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 3189	. . . . . . 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 3015	. . 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 24253	. . . . . . . . 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 7513	. . . . . . . . . 10 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦𝑀𝑦) ∈ (0[,]𝑥))
95		elicc2 13306	. . . . . . . . . . 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 5110	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 0 ≤ 𝑥)
100	88, 99	ge0p1rpd 12959	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ+)
101		fovcdm 7511	. . . . . . . . . . . . . 14 ⊢ ((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
102	101	3expa 1118	. . . . . . . . . . . . 13 ⊢ (((𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
103	102	adantlll 718	. . . . . . . . . . . 12 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) ∈ (0[,]𝑥))
104		elicc2 13306	. . . . . . . . . . . . . 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 11281	. . . . . . . . . . . 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 12047	. . . . . . . . . 10 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → 𝑥 < (𝑥 + 1))
115	108, 109, 112, 113, 114	lelttrd 11266	. . . . . . . . 9 ⊢ (((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ 𝑋) → (𝑦𝑀𝑧) < (𝑥 + 1))
116	115	ralrimiva 3124	. . . . . . . 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 11157	. . . . . . . 8 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑥 + 1) ∈ ℝ*)
121		blval 24296	. . . . . . . 8 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑥 + 1) ∈ ℝ*) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
122	119, 90, 120, 121	syl3anc 1373	. . . . . . 7 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → (𝑦(ball‘𝑀)(𝑥 + 1)) = {𝑧 ∈ 𝑋 ∣ (𝑦𝑀𝑧) < (𝑥 + 1)})
123	118, 122	eqtr4d 2769	. . . . . 6 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1)))
124		oveq2 7349	. . . . . . 7 ⊢ (𝑟 = (𝑥 + 1) → (𝑦(ball‘𝑀)𝑟) = (𝑦(ball‘𝑀)(𝑥 + 1)))
125	124	rspceeqv 3595	. . . . . 6 ⊢ (((𝑥 + 1) ∈ ℝ+ ∧ 𝑋 = (𝑦(ball‘𝑀)(𝑥 + 1))) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
126	100, 123, 125	syl2anc 584	. . . . 5 ⊢ ((((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) ∧ 𝑦 ∈ 𝑋) → ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
127	126	ralrimiva 3124	. . . 4 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟))
128		isbnd 37820	. . . 4 ⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∀𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ 𝑋 = (𝑦(ball‘𝑀)𝑟)))
129	87, 127, 128	sylanbrc 583	. . 3 ⊢ (((𝑀 ∈ (Met‘𝑋) ∧ 𝑥 ∈ ℝ) ∧ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
130	129	r19.29an 3136	. 2 ⊢ ((𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)) → 𝑀 ∈ (Bnd‘𝑋))
131	86, 130	impbii 209	1 ⊢ (𝑀 ∈ (Bnd‘𝑋) ↔ (𝑀 ∈ (Met‘𝑋) ∧ ∃𝑥 ∈ ℝ 𝑀:(𝑋 × 𝑋)⟶(0[,]𝑥)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  {crab 3395   ⊆ wss 3897  ∅c0 4278   class class class wbr 5086   × cxp 5609  dom cdm 5611  ran crn 5612   Fn wfn 6471  ⟶wf 6472  ‘cfv 6476  (class class class)co 7341  ℝcr 11000  0cc0 11001  1c1 11002   + caddc 11004   · cmul 11006  ℝ^*cxr 11140   < clt 11141   ≤ cle 11142  2c2 12175  ℝ⁺crp 12885  [,]cicc 13243  ∞Metcxmet 21271  Metcmet 21272  ballcbl 21273  Bndcbnd 37807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-1st 7916  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-er 8617  df-ec 8619  df-map 8747  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342  df-div 11770  df-nn 12121  df-2 12183  df-rp 12886  df-xneg 13006  df-xadd 13007  df-xmul 13008  df-icc 13247  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-bnd 37819

This theorem is referenced by:  isbnd3b  37825  prdsbnd  37833