xmettx - Intuitionistic Logic Explorer

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

Theorem xmettx 14198

Description: The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.)

**Hypotheses**
Ref	Expression
xmetxp.p	⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1^st ‘𝑢)𝑀(1^st ‘𝑣)), ((2^nd ‘𝑢)𝑁(2^nd ‘𝑣))}, ℝ^*, < ))
xmetxp.1	⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))
xmetxp.2	⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))
xmettx.j	⊢ 𝐽 = (MetOpen‘𝑀)
xmettx.k	⊢ 𝐾 = (MetOpen‘𝑁)
xmettx.l	⊢ 𝐿 = (MetOpen‘𝑃)

**Assertion**
Ref	Expression
xmettx	⊢ (𝜑 → 𝐿 = (𝐽 ×_t 𝐾))

Distinct variable groups: 𝑢,𝑀,𝑣 𝑢,𝑁,𝑣 𝑢,𝑋,𝑣 𝑢,𝑌,𝑣 Allowed substitution hints: 𝜑(𝑣,𝑢) 𝑃(𝑣,𝑢) 𝐽(𝑣,𝑢) 𝐾(𝑣,𝑢) 𝐿(𝑣,𝑢)

Proof of Theorem xmettx Dummy variables 𝑗 𝑘 𝑚 𝑛 𝑥 𝑦 𝑟 𝑠 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xmetxp.p	. . 3 ⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1^st ‘𝑢)𝑀(1^st ‘𝑣)), ((2^nd ‘𝑢)𝑁(2^nd ‘𝑣))}, ℝ^*, < ))
2		xmetxp.1	. . 3 ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))
3		xmetxp.2	. . 3 ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))
4		xmettx.j	. . 3 ⊢ 𝐽 = (MetOpen‘𝑀)
5		xmettx.k	. . 3 ⊢ 𝐾 = (MetOpen‘𝑁)
6		xmettx.l	. . 3 ⊢ 𝐿 = (MetOpen‘𝑃)
7	1, 2, 3, 4, 5, 6	xmettxlem 14197	. 2 ⊢ (𝜑 → 𝐿 ⊆ (𝐽 ×_t 𝐾))
8		eqid 2177	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) = (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))
9	8	elrnmpog 5990	. . . . . . . . . . 11 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ↔ ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠)))
10	9	elv 2743	. . . . . . . . . 10 ⊢ (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ↔ ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠))
11	10	biimpi 120	. . . . . . . . 9 ⊢ (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) → ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠))
12	11	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠))
13		xpeq1 4642	. . . . . . . . . 10 ⊢ (𝑟 = 𝑥 → (𝑟 × 𝑠) = (𝑥 × 𝑠))
14	13	eqeq2d 2189	. . . . . . . . 9 ⊢ (𝑟 = 𝑥 → (𝑤 = (𝑟 × 𝑠) ↔ 𝑤 = (𝑥 × 𝑠)))
15		xpeq2 4643	. . . . . . . . . 10 ⊢ (𝑠 = 𝑦 → (𝑥 × 𝑠) = (𝑥 × 𝑦))
16	15	eqeq2d 2189	. . . . . . . . 9 ⊢ (𝑠 = 𝑦 → (𝑤 = (𝑥 × 𝑠) ↔ 𝑤 = (𝑥 × 𝑦)))
17	14, 16	cbvrex2v 2719	. . . . . . . 8 ⊢ (∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠) ↔ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 𝑤 = (𝑥 × 𝑦))
18	12, 17	sylib 122	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 𝑤 = (𝑥 × 𝑦))
19		simpr 110	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑤 = (𝑥 × 𝑦))
20		simplll 533	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝜑)
21		simplrl 535	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑥 ∈ 𝐽)
22		simplrr 536	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑦 ∈ 𝐾)
23	4	mopntopon 14131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
24	2, 23	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
25	24	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐽 ∈ (TopOn‘𝑋))
26		simprl 529	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑥 ∈ 𝐽)
27		toponss 13714	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽) → 𝑥 ⊆ 𝑋)
28	25, 26, 27	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑥 ⊆ 𝑋)
29	5	mopntopon 14131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝐾 ∈ (TopOn‘𝑌))
30	3, 29	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
31	30	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐾 ∈ (TopOn‘𝑌))
32		simprr 531	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ∈ 𝐾)
33		toponss 13714	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑦 ∈ 𝐾) → 𝑦 ⊆ 𝑌)
34	31, 32, 33	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ⊆ 𝑌)
35		xpss12 4735	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
36	28, 34, 35	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌))
37	1, 2, 3	xmetxp 14195	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌)))
38		unirnbl 14111	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → ∪ ran (ball‘𝑃) = (𝑋 × 𝑌))
39	37, 38	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ ran (ball‘𝑃) = (𝑋 × 𝑌))
40	39	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ∪ ran (ball‘𝑃) = (𝑋 × 𝑌))
41	36, 40	sseqtrrd 3196	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 × 𝑦) ⊆ ∪ ran (ball‘𝑃))
42	2	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑀 ∈ (∞Met‘𝑋))
43		simplrl 535	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑥 ∈ 𝐽)
44		xp1st 6169	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑥 × 𝑦) → (1^st ‘𝑗) ∈ 𝑥)
45	44	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (1^st ‘𝑗) ∈ 𝑥)
46	4	mopni2 14171	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝐽 ∧ (1^st ‘𝑗) ∈ 𝑥) → ∃𝑚 ∈ ℝ⁺ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)
47	42, 43, 45, 46	syl3anc 1238	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → ∃𝑚 ∈ ℝ⁺ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)
48	3	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑁 ∈ (∞Met‘𝑌))
49		simplrr 536	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑦 ∈ 𝐾)
50		xp2nd 6170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (𝑥 × 𝑦) → (2^nd ‘𝑗) ∈ 𝑦)
51	50	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (2^nd ‘𝑗) ∈ 𝑦)
52	5	mopni2 14171	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑦 ∈ 𝐾 ∧ (2^nd ‘𝑗) ∈ 𝑦) → ∃𝑛 ∈ ℝ⁺ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)
53	48, 49, 51, 52	syl3anc 1238	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → ∃𝑛 ∈ ℝ⁺ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)
54	53	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) → ∃𝑛 ∈ ℝ⁺ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)
55		blf 14098	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → (ball‘𝑃):((𝑋 × 𝑌) × ℝ^*)⟶𝒫 (𝑋 × 𝑌))
56	37, 55	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ball‘𝑃):((𝑋 × 𝑌) × ℝ^*)⟶𝒫 (𝑋 × 𝑌))
57	56	ffnd 5368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ball‘𝑃) Fn ((𝑋 × 𝑌) × ℝ^*))
58	57	ad4antr 494	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (ball‘𝑃) Fn ((𝑋 × 𝑌) × ℝ^*))
59	36	sselda 3157	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑗 ∈ (𝑋 × 𝑌))
60	59	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑗 ∈ (𝑋 × 𝑌))
61		rpxr 9664	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℝ⁺ → 𝑚 ∈ ℝ^*)
62	61	ad2antrl 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) → 𝑚 ∈ ℝ^*)
63	62	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑚 ∈ ℝ^*)
64		rpxr 9664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℝ⁺ → 𝑛 ∈ ℝ^*)
65	64	ad2antrl 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑛 ∈ ℝ^*)
66		xrmincl 11277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℝ^* ∧ 𝑛 ∈ ℝ^) → inf({𝑚, 𝑛}, ℝ^, < ) ∈ ℝ^*)
67	63, 65, 66	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ^, < ) ∈ ℝ^)
68		fnovrn 6025	. . . . . . . . . . . . . . . . . 18 ⊢ (((ball‘𝑃) Fn ((𝑋 × 𝑌) × ℝ^) ∧ 𝑗 ∈ (𝑋 × 𝑌) ∧ inf({𝑚, 𝑛}, ℝ^, < ) ∈ ℝ^) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) ∈ ran (ball‘𝑃))
69	58, 60, 67, 68	syl3anc 1238	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^*, < )) ∈ ran (ball‘𝑃))
70		eleq2 2241	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) → (𝑗 ∈ 𝑘 ↔ 𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < ))))
71		sseq1 3180	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) → (𝑘 ⊆ (𝑥 × 𝑦) ↔ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) ⊆ (𝑥 × 𝑦)))
72	70, 71	anbi12d 473	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) → ((𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)) ↔ (𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) ∧ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ (𝑥 × 𝑦))))
73	72	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) ∧ 𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < ))) → ((𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)) ↔ (𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) ∧ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ (𝑥 × 𝑦))))
74	37	ad4antr 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌)))
75		simplrl 535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑚 ∈ ℝ⁺)
76		simprl 529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑛 ∈ ℝ⁺)
77		xrminrpcl 11285	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → inf({𝑚, 𝑛}, ℝ^*, < ) ∈ ℝ⁺)
78	75, 76, 77	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ^*, < ) ∈ ℝ⁺)
79		blcntr 14104	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) ∧ 𝑗 ∈ (𝑋 × 𝑌) ∧ inf({𝑚, 𝑛}, ℝ^, < ) ∈ ℝ⁺) → 𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )))
80	74, 60, 78, 79	syl3anc 1238	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^*, < )))
81	42	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑀 ∈ (∞Met‘𝑋))
82	48	ad2antrr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑁 ∈ (∞Met‘𝑌))
83	1, 81, 82, 67, 60	xmetxpbl 14196	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) = (((1^st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ^, < )) × ((2^nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ^*, < ))))
84	28	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑥 ⊆ 𝑋)
85	84, 45	sseldd 3158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (1^st ‘𝑗) ∈ 𝑋)
86	85	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (1^st ‘𝑗) ∈ 𝑋)
87		xrmin1inf 11278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℝ^* ∧ 𝑛 ∈ ℝ^) → inf({𝑚, 𝑛}, ℝ^, < ) ≤ 𝑚)
88	63, 65, 87	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ^*, < ) ≤ 𝑚)
89		ssbl 14114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ (1^st ‘𝑗) ∈ 𝑋) ∧ (inf({𝑚, 𝑛}, ℝ^, < ) ∈ ℝ^ ∧ 𝑚 ∈ ℝ^) ∧ inf({𝑚, 𝑛}, ℝ^, < ) ≤ 𝑚) → ((1^st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ ((1^st ‘𝑗)(ball‘𝑀)𝑚))
90	81, 86, 67, 63, 88, 89	syl221anc 1249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((1^st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ ((1^st ‘𝑗)(ball‘𝑀)𝑚))
91		simplrr 536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)
92	90, 91	sstrd 3167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((1^st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ 𝑥)
93	34	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑦 ⊆ 𝑌)
94	93, 51	sseldd 3158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (2^nd ‘𝑗) ∈ 𝑌)
95	94	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (2^nd ‘𝑗) ∈ 𝑌)
96		xrmin2inf 11279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℝ^* ∧ 𝑛 ∈ ℝ^) → inf({𝑚, 𝑛}, ℝ^, < ) ≤ 𝑛)
97	63, 65, 96	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ^*, < ) ≤ 𝑛)
98		ssbl 14114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ (∞Met‘𝑌) ∧ (2^nd ‘𝑗) ∈ 𝑌) ∧ (inf({𝑚, 𝑛}, ℝ^, < ) ∈ ℝ^ ∧ 𝑛 ∈ ℝ^) ∧ inf({𝑚, 𝑛}, ℝ^, < ) ≤ 𝑛) → ((2^nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ ((2^nd ‘𝑗)(ball‘𝑁)𝑛))
99	82, 95, 67, 65, 97, 98	syl221anc 1249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((2^nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ ((2^nd ‘𝑗)(ball‘𝑁)𝑛))
100		simprr 531	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)
101	99, 100	sstrd 3167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((2^nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ 𝑦)
102		xpss12 4735	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((1^st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ^, < )) ⊆ 𝑥 ∧ ((2^nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ^, < )) ⊆ 𝑦) → (((1^st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ^, < )) × ((2^nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ^, < ))) ⊆ (𝑥 × 𝑦))
103	92, 101, 102	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (((1^st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ^, < )) × ((2^nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ^, < ))) ⊆ (𝑥 × 𝑦))
104	83, 103	eqsstrd 3193	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^*, < )) ⊆ (𝑥 × 𝑦))
105	80, 104	jca 306	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) ∧ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ^, < )) ⊆ (𝑥 × 𝑦)))
106	69, 73, 105	rspcedvd 2849	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ⁺ ∧ ((2^nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)))
107	54, 106	rexlimddv 2599	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ⁺ ∧ ((1^st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) → ∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)))
108	47, 107	rexlimddv 2599	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → ∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)))
109	108	ralrimiva 2550	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)))
110	41, 109	jca 306	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝑥 × 𝑦) ⊆ ∪ ran (ball‘𝑃) ∧ ∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦))))
111		blex 14075	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → (ball‘𝑃) ∈ V)
112	37, 111	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ball‘𝑃) ∈ V)
113	112	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (ball‘𝑃) ∈ V)
114		rnexg 4894	. . . . . . . . . . . . 13 ⊢ ((ball‘𝑃) ∈ V → ran (ball‘𝑃) ∈ V)
115		eltg2 13741	. . . . . . . . . . . . 13 ⊢ (ran (ball‘𝑃) ∈ V → ((𝑥 × 𝑦) ∈ (topGen‘ran (ball‘𝑃)) ↔ ((𝑥 × 𝑦) ⊆ ∪ ran (ball‘𝑃) ∧ ∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)))))
116	113, 114, 115	3syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝑥 × 𝑦) ∈ (topGen‘ran (ball‘𝑃)) ↔ ((𝑥 × 𝑦) ⊆ ∪ ran (ball‘𝑃) ∧ ∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)))))
117	110, 116	mpbird 167	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 × 𝑦) ∈ (topGen‘ran (ball‘𝑃)))
118	20, 21, 22, 117	syl12anc 1236	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → (𝑥 × 𝑦) ∈ (topGen‘ran (ball‘𝑃)))
119	19, 118	eqeltrd 2254	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑤 ∈ (topGen‘ran (ball‘𝑃)))
120	119	ex 115	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑤 = (𝑥 × 𝑦) → 𝑤 ∈ (topGen‘ran (ball‘𝑃))))
121	120	rexlimdvva 2602	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 𝑤 = (𝑥 × 𝑦) → 𝑤 ∈ (topGen‘ran (ball‘𝑃))))
122	18, 121	mpd 13	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → 𝑤 ∈ (topGen‘ran (ball‘𝑃)))
123	122	ex 115	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) → 𝑤 ∈ (topGen‘ran (ball‘𝑃))))
124	123	ssrdv 3163	. . . 4 ⊢ (𝜑 → ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ⊆ (topGen‘ran (ball‘𝑃)))
125	4	mopntop 14132	. . . . . . . 8 ⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
126	2, 125	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
127	5	mopntop 14132	. . . . . . . 8 ⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝐾 ∈ Top)
128	3, 127	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Top)
129		mpoexga 6216	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V)
130	126, 128, 129	syl2anc 411	. . . . . 6 ⊢ (𝜑 → (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V)
131		rnexg 4894	. . . . . 6 ⊢ ((𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V → ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V)
132	130, 131	syl 14	. . . . 5 ⊢ (𝜑 → ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V)
133	37, 111, 114	3syl 17	. . . . 5 ⊢ (𝜑 → ran (ball‘𝑃) ∈ V)
134		tgss3 13766	. . . . 5 ⊢ ((ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V ∧ ran (ball‘𝑃) ∈ V) → ((topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ⊆ (topGen‘ran (ball‘𝑃)) ↔ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ⊆ (topGen‘ran (ball‘𝑃))))
135	132, 133, 134	syl2anc 411	. . . 4 ⊢ (𝜑 → ((topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ⊆ (topGen‘ran (ball‘𝑃)) ↔ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ⊆ (topGen‘ran (ball‘𝑃))))
136	124, 135	mpbird 167	. . 3 ⊢ (𝜑 → (topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ⊆ (topGen‘ran (ball‘𝑃)))
137		eqid 2177	. . . . 5 ⊢ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) = ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))
138	137	txval 13943	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×_t 𝐾) = (topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))))
139	126, 128, 138	syl2anc 411	. . 3 ⊢ (𝜑 → (𝐽 ×_t 𝐾) = (topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))))
140	6	mopnval 14130	. . . 4 ⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → 𝐿 = (topGen‘ran (ball‘𝑃)))
141	37, 140	syl 14	. . 3 ⊢ (𝜑 → 𝐿 = (topGen‘ran (ball‘𝑃)))
142	136, 139, 141	3sstr4d 3202	. 2 ⊢ (𝜑 → (𝐽 ×_t 𝐾) ⊆ 𝐿)
143	7, 142	eqssd 3174	1 ⊢ (𝜑 → 𝐿 = (𝐽 ×_t 𝐾))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 ∈ wcel 2148 ∀wral 2455 ∃wrex 2456 Vcvv 2739 ⊆ wss 3131 𝒫 cpw 3577 {cpr 3595 ∪ cuni 3811 class class class wbr 4005 × cxp 4626 ran crn 4629 Fn wfn 5213 ⟶wf 5214 ‘cfv 5218 (class class class)co 5878 ∈ cmpo 5880 1^st c1st 6142 2^nd c2nd 6143 supcsup 6984 infcinf 6985 ℝ^*cxr 7994 < clt 7995 ≤ cle 7996 ℝ⁺crp 9656 topGenctg 12709 ∞Metcxmet 13614 ballcbl 13616 MetOpencmopn 13619 Topctop 13685 TopOnctopon 13698 ×_t ctx 13940

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589 ax-cnex 7905 ax-resscn 7906 ax-1cn 7907 ax-1re 7908 ax-icn 7909 ax-addcl 7910 ax-addrcl 7911 ax-mulcl 7912 ax-mulrcl 7913 ax-addcom 7914 ax-mulcom 7915 ax-addass 7916 ax-mulass 7917 ax-distr 7918 ax-i2m1 7919 ax-0lt1 7920 ax-1rid 7921 ax-0id 7922 ax-rnegex 7923 ax-precex 7924 ax-cnre 7925 ax-pre-ltirr 7926 ax-pre-ltwlin 7927 ax-pre-lttrn 7928 ax-pre-apti 7929 ax-pre-ltadd 7930 ax-pre-mulgt0 7931 ax-pre-mulext 7932 ax-arch 7933 ax-caucvg 7934

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-id 4295 df-po 4298 df-iso 4299 df-iord 4368 df-on 4370 df-ilim 4371 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-isom 5227 df-riota 5834 df-ov 5881 df-oprab 5882 df-mpo 5883 df-1st 6144 df-2nd 6145 df-recs 6309 df-frec 6395 df-map 6653 df-sup 6986 df-inf 6987 df-pnf 7997 df-mnf 7998 df-xr 7999 df-ltxr 8000 df-le 8001 df-sub 8133 df-neg 8134 df-reap 8535 df-ap 8542 df-div 8633 df-inn 8923 df-2 8981 df-3 8982 df-4 8983 df-n0 9180 df-z 9257 df-uz 9532 df-q 9623 df-rp 9657 df-xneg 9775 df-xadd 9776 df-seqfrec 10449 df-exp 10523 df-cj 10854 df-re 10855 df-im 10856 df-rsqrt 11010 df-abs 11011 df-topgen 12715 df-psmet 13621 df-xmet 13622 df-bl 13624 df-mopn 13625 df-top 13686 df-topon 13699 df-bases 13731 df-tx 13941

This theorem is referenced by: txmetcnp 14206

W3C validator