ptrecube

Description: Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020) (Proof shortened by AV, 28-Sep-2020)

	Ref	Expression
Hypotheses	ptrecube.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
	ptrecube.d	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
Assertion	ptrecube	$⊢ (S \in R \land P \in S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S$

Proof

Step	Hyp	Ref	Expression
1		ptrecube.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
2		ptrecube.d	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
3		fzfi	$⊢ (1 \dots N) \in Fin$
4		retop	$⊢ topGen (ran (.)) \in Top$
5		fnconstg	$⊢ topGen (ran (.)) \in Top \to ((1 \dots N) \times \{topGen (ran (.))\}) Fn (1 \dots N)$
6	4 5	ax-mp	$⊢ ((1 \dots N) \times \{topGen (ran (.))\}) Fn (1 \dots N)$
7		eqid	$⊢ \{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\} = \{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\}$
8	7	ptval	$⊢ ((1 \dots N) \in Fin \land ((1 \dots N) \times \{topGen (ran (.))\}) Fn (1 \dots N)) \to \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) = topGen (\{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\})$
9	3 6 8	mp2an	$⊢ \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) = topGen (\{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\})$
10	1 9	eqtri	$⊢ R = topGen (\{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\})$
11	10	eleq2i	$⊢ S \in R \leftrightarrow S \in topGen (\{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\})$
12		tg2	$⊢ (S \in topGen (\{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\}) \land P \in S) \to \exists z \in \{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\} (P \in z \land z \subseteq S)$
13	7	elpt	$⊢ z \in \{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\} \leftrightarrow \exists g ((g Fn (1 \dots N) \land \forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists z \in Fin \forall n \in ((1 \dots N) ∖ z) g (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land z = ⨉_{n = 1}^{N} g (n))$
14		fvex	$⊢ topGen (ran (.)) \in V$
15	14	fvconst2	$⊢ n \in (1 \dots N) \to ((1 \dots N) \times \{topGen (ran (.))\}) (n) = topGen (ran (.))$
16	15	eleq2d	$⊢ n \in (1 \dots N) \to (g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \leftrightarrow g (n) \in topGen (ran (.)))$
17	16	ralbiia	$⊢ \forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \leftrightarrow \forall n \in (1 \dots N) g (n) \in topGen (ran (.))$
18		elixp2	$⊢ P \in ⨉_{n = 1}^{N} g (n) \leftrightarrow (P \in V \land P Fn (1 \dots N) \land \forall n \in (1 \dots N) P (n) \in g (n))$
19	18	simp3bi	$⊢ P \in ⨉_{n = 1}^{N} g (n) \to \forall n \in (1 \dots N) P (n) \in g (n)$
20		r19.26	$⊢ \forall n \in (1 \dots N) (g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \leftrightarrow (\forall n \in (1 \dots N) g (n) \in topGen (ran (.)) \land \forall n \in (1 \dots N) P (n) \in g (n))$
21		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
22	21	eltopss	$⊢ (topGen (ran (.)) \in Top \land g (n) \in topGen (ran (.))) \to g (n) \subseteq ℝ$
23	4 22	mpan	$⊢ g (n) \in topGen (ran (.)) \to g (n) \subseteq ℝ$
24	23	sselda	$⊢ (g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \to P (n) \in ℝ$
25	2	rexmet	$⊢ D \in ∞Met (ℝ)$
26		eqid	$⊢ MetOpen (D) = MetOpen (D)$
27	2 26	tgioo	$⊢ topGen (ran (.)) = MetOpen (D)$
28	27	mopni2	$⊢ (D \in ∞Met (ℝ) \land g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \to \exists y \in ℝ^{+} P (n) ball (D) y \subseteq g (n)$
29	25 28	mp3an1	$⊢ (g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \to \exists y \in ℝ^{+} P (n) ball (D) y \subseteq g (n)$
30		r19.42v	$⊢ \exists y \in ℝ^{+} (P (n) \in ℝ \land P (n) ball (D) y \subseteq g (n)) \leftrightarrow (P (n) \in ℝ \land \exists y \in ℝ^{+} P (n) ball (D) y \subseteq g (n))$
31	24 29 30	sylanbrc	$⊢ (g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \to \exists y \in ℝ^{+} (P (n) \in ℝ \land P (n) ball (D) y \subseteq g (n))$
32	31	ralimi	$⊢ \forall n \in (1 \dots N) (g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \to \forall n \in (1 \dots N) \exists y \in ℝ^{+} (P (n) \in ℝ \land P (n) ball (D) y \subseteq g (n))$
33		oveq2	$⊢ y = h (n) \to P (n) ball (D) y = P (n) ball (D) h (n)$
34	33	sseq1d	$⊢ y = h (n) \to (P (n) ball (D) y \subseteq g (n) \leftrightarrow P (n) ball (D) h (n) \subseteq g (n))$
35	34	anbi2d	$⊢ y = h (n) \to ((P (n) \in ℝ \land P (n) ball (D) y \subseteq g (n)) \leftrightarrow (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n)))$
36	35	ac6sfi	$⊢ ((1 \dots N) \in Fin \land \forall n \in (1 \dots N) \exists y \in ℝ^{+} (P (n) \in ℝ \land P (n) ball (D) y \subseteq g (n))) \to \exists h (h : (1 \dots N) ⟶ ℝ^{+} \land \forall n \in (1 \dots N) (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n)))$
37	3 32 36	sylancr	$⊢ \forall n \in (1 \dots N) (g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \to \exists h (h : (1 \dots N) ⟶ ℝ^{+} \land \forall n \in (1 \dots N) (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n)))$
38		1rp	$⊢ 1 \in ℝ^{+}$
39	38	a1i	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land (1 \dots N) = \emptyset) \to 1 \in ℝ^{+}$
40		frn	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to ran h \subseteq ℝ^{+}$
41	40	adantr	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \neg (1 \dots N) = \emptyset) \to ran h \subseteq ℝ^{+}$
42		ffn	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to h Fn (1 \dots N)$
43		fnfi	$⊢ (h Fn (1 \dots N) \land (1 \dots N) \in Fin) \to h \in Fin$
44	42 3 43	sylancl	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to h \in Fin$
45		rnfi	$⊢ h \in Fin \to ran h \in Fin$
46	44 45	syl	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to ran h \in Fin$
47	46	adantr	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \neg (1 \dots N) = \emptyset) \to ran h \in Fin$
48		dm0rn0	$⊢ dom h = \emptyset \leftrightarrow ran h = \emptyset$
49		fdm	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to dom h = (1 \dots N)$
50	49	eqeq1d	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to (dom h = \emptyset \leftrightarrow (1 \dots N) = \emptyset)$
51	48 50	bitr3id	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to (ran h = \emptyset \leftrightarrow (1 \dots N) = \emptyset)$
52	51	necon3abid	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to (ran h \neq \emptyset \leftrightarrow \neg (1 \dots N) = \emptyset)$
53	52	biimpar	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \neg (1 \dots N) = \emptyset) \to ran h \neq \emptyset$
54		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
55	40 54	sstrdi	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to ran h \subseteq ℝ$
56	55	adantr	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \neg (1 \dots N) = \emptyset) \to ran h \subseteq ℝ$
57		ltso	$⊢ < Or ℝ$
58		fiinfcl	$⊢ (< Or ℝ \land (ran h \in Fin \land ran h \neq \emptyset \land ran h \subseteq ℝ)) \to inf (ran h ℝ <) \in ran h$
59	57 58	mpan	$⊢ (ran h \in Fin \land ran h \neq \emptyset \land ran h \subseteq ℝ) \to inf (ran h ℝ <) \in ran h$
60	47 53 56 59	syl3anc	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \neg (1 \dots N) = \emptyset) \to inf (ran h ℝ <) \in ran h$
61	41 60	sseldd	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \neg (1 \dots N) = \emptyset) \to inf (ran h ℝ <) \in ℝ^{+}$
62	39 61	ifclda	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{+}$
63	62	adantr	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \forall n \in (1 \dots N) (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n))) \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{+}$
64	62	adantr	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{+}$
65	64	rpxrd	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{*}$
66		ffvelcdm	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to h (n) \in ℝ^{+}$
67	66	rpxrd	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to h (n) \in ℝ^{*}$
68		ne0i	$⊢ n \in (1 \dots N) \to (1 \dots N) \neq \emptyset$
69		ifnefalse	$⊢ (1 \dots N) \neq \emptyset \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) = inf (ran h ℝ <)$
70	68 69	syl	$⊢ n \in (1 \dots N) \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) = inf (ran h ℝ <)$
71	70	adantl	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) = inf (ran h ℝ <)$
72	55	adantr	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to ran h \subseteq ℝ$
73		0re	$⊢ 0 \in ℝ$
74		rpge0	$⊢ y \in ℝ^{+} \to 0 \leq y$
75	74	rgen	$⊢ \forall y \in ℝ^{+} 0 \leq y$
76		ssralv	$⊢ ran h \subseteq ℝ^{+} \to (\forall y \in ℝ^{+} 0 \leq y \to \forall y \in ran h 0 \leq y)$
77	40 75 76	mpisyl	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to \forall y \in ran h 0 \leq y$
78		breq1	$⊢ x = 0 \to (x \leq y \leftrightarrow 0 \leq y)$
79	78	ralbidv	$⊢ x = 0 \to (\forall y \in ran h x \leq y \leftrightarrow \forall y \in ran h 0 \leq y)$
80	79	rspcev	$⊢ (0 \in ℝ \land \forall y \in ran h 0 \leq y) \to \exists x \in ℝ \forall y \in ran h x \leq y$
81	73 77 80	sylancr	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to \exists x \in ℝ \forall y \in ran h x \leq y$
82	81	adantr	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to \exists x \in ℝ \forall y \in ran h x \leq y$
83		fnfvelrn	$⊢ (h Fn (1 \dots N) \land n \in (1 \dots N)) \to h (n) \in ran h$
84	42 83	sylan	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to h (n) \in ran h$
85		infrelb	$⊢ (ran h \subseteq ℝ \land \exists x \in ℝ \forall y \in ran h x \leq y \land h (n) \in ran h) \to inf (ran h ℝ <) \leq h (n)$
86	72 82 84 85	syl3anc	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to inf (ran h ℝ <) \leq h (n)$
87	71 86	eqbrtrd	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \leq h (n)$
88	65 67 87	jca31	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to ((if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{} \land h (n) \in ℝ^{}) \land if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \leq h (n))$
89		ssbl	$⊢ ((D \in ∞Met (ℝ) \land P (n) \in ℝ) \land (if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{} \land h (n) \in ℝ^{}) \land if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \leq h (n)) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq P (n) ball (D) h (n)$
90	89	3expb	$⊢ ((D \in ∞Met (ℝ) \land P (n) \in ℝ) \land ((if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{} \land h (n) \in ℝ^{}) \land if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \leq h (n))) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq P (n) ball (D) h (n)$
91	25 90	mpanl1	$⊢ (P (n) \in ℝ \land ((if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{} \land h (n) \in ℝ^{}) \land if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \leq h (n))) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq P (n) ball (D) h (n)$
92	91	ancoms	$⊢ (((if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{} \land h (n) \in ℝ^{}) \land if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \leq h (n)) \land P (n) \in ℝ) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq P (n) ball (D) h (n)$
93	88 92	sylan	$⊢ ((h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \land P (n) \in ℝ) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq P (n) ball (D) h (n)$
94		sstr2	$⊢ P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq P (n) ball (D) h (n) \to (P (n) ball (D) h (n) \subseteq g (n) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n))$
95	93 94	syl	$⊢ ((h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \land P (n) \in ℝ) \to (P (n) ball (D) h (n) \subseteq g (n) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n))$
96	95	expimpd	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land n \in (1 \dots N)) \to ((P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n)) \to P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n))$
97	96	ralimdva	$⊢ h : (1 \dots N) ⟶ ℝ^{+} \to (\forall n \in (1 \dots N) (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n)) \to \forall n \in (1 \dots N) P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n))$
98	97	imp	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \forall n \in (1 \dots N) (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n))) \to \forall n \in (1 \dots N) P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n)$
99	2	fveq2i	$⊢ ball (D) = ball ({(abs \circ -) ↾}_{ℝ^{2}})$
100	99	oveqi	$⊢ P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) = P (n) ball ({(abs \circ -) ↾}_{ℝ^{2}}) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <))$
101	100	sseq1i	$⊢ P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n) \leftrightarrow P (n) ball ({(abs \circ -) ↾}_{ℝ^{2}}) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n)$
102	101	ralbii	$⊢ \forall n \in (1 \dots N) P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n) \leftrightarrow \forall n \in (1 \dots N) P (n) ball ({(abs \circ -) ↾}_{ℝ^{2}}) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n)$
103		nfv	$⊢ Ⅎ d \forall n \in (1 \dots N) P (n) ball ({(abs \circ -) ↾}_{ℝ^{2}}) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n)$
104	102 103	nfxfr	$⊢ Ⅎ d \forall n \in (1 \dots N) P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n)$
105		oveq2	$⊢ d = if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \to P (n) ball (D) d = P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <))$
106	105	sseq1d	$⊢ d = if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \to (P (n) ball (D) d \subseteq g (n) \leftrightarrow P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n))$
107	106	ralbidv	$⊢ d = if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \to (\forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n) \leftrightarrow \forall n \in (1 \dots N) P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n))$
108	104 107	rspce	$⊢ (if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \in ℝ^{+} \land \forall n \in (1 \dots N) P (n) ball (D) if ((1 \dots N) = \emptyset, 1, inf (ran h ℝ <)) \subseteq g (n)) \to \exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n)$
109	63 98 108	syl2anc	$⊢ (h : (1 \dots N) ⟶ ℝ^{+} \land \forall n \in (1 \dots N) (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n))) \to \exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n)$
110	109	exlimiv	$⊢ \exists h (h : (1 \dots N) ⟶ ℝ^{+} \land \forall n \in (1 \dots N) (P (n) \in ℝ \land P (n) ball (D) h (n) \subseteq g (n))) \to \exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n)$
111	37 110	syl	$⊢ \forall n \in (1 \dots N) (g (n) \in topGen (ran (.)) \land P (n) \in g (n)) \to \exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n)$
112	20 111	sylbir	$⊢ (\forall n \in (1 \dots N) g (n) \in topGen (ran (.)) \land \forall n \in (1 \dots N) P (n) \in g (n)) \to \exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n)$
113	19 112	sylan2	$⊢ (\forall n \in (1 \dots N) g (n) \in topGen (ran (.)) \land P \in ⨉_{n = 1}^{N} g (n)) \to \exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n)$
114	17 113	sylanb	$⊢ (\forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land P \in ⨉_{n = 1}^{N} g (n)) \to \exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n)$
115		sstr2	$⊢ ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq ⨉_{n = 1}^{N} g (n) \to (⨉_{n = 1}^{N} g (n) \subseteq S \to ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
116		ss2ixp	$⊢ \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n) \to ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq ⨉_{n = 1}^{N} g (n)$
117	115 116	syl11	$⊢ ⨉_{n = 1}^{N} g (n) \subseteq S \to (\forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n) \to ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
118	117	reximdv	$⊢ ⨉_{n = 1}^{N} g (n) \subseteq S \to (\exists d \in ℝ^{+} \forall n \in (1 \dots N) P (n) ball (D) d \subseteq g (n) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
119	114 118	syl5com	$⊢ (\forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land P \in ⨉_{n = 1}^{N} g (n)) \to (⨉_{n = 1}^{N} g (n) \subseteq S \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
120	119	expimpd	$⊢ \forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \to ((P \in ⨉_{n = 1}^{N} g (n) \land ⨉_{n = 1}^{N} g (n) \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
121		eleq2	$⊢ z = ⨉_{n = 1}^{N} g (n) \to (P \in z \leftrightarrow P \in ⨉_{n = 1}^{N} g (n))$
122		sseq1	$⊢ z = ⨉_{n = 1}^{N} g (n) \to (z \subseteq S \leftrightarrow ⨉_{n = 1}^{N} g (n) \subseteq S)$
123	121 122	anbi12d	$⊢ z = ⨉_{n = 1}^{N} g (n) \to ((P \in z \land z \subseteq S) \leftrightarrow (P \in ⨉_{n = 1}^{N} g (n) \land ⨉_{n = 1}^{N} g (n) \subseteq S))$
124	123	imbi1d	$⊢ z = ⨉_{n = 1}^{N} g (n) \to (((P \in z \land z \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S) \leftrightarrow ((P \in ⨉_{n = 1}^{N} g (n) \land ⨉_{n = 1}^{N} g (n) \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S))$
125	120 124	syl5ibrcom	$⊢ \forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \to (z = ⨉_{n = 1}^{N} g (n) \to ((P \in z \land z \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S))$
126	125	3ad2ant2	$⊢ (g Fn (1 \dots N) \land \forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists z \in Fin \forall n \in ((1 \dots N) ∖ z) g (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \to (z = ⨉_{n = 1}^{N} g (n) \to ((P \in z \land z \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S))$
127	126	imp	$⊢ ((g Fn (1 \dots N) \land \forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists z \in Fin \forall n \in ((1 \dots N) ∖ z) g (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land z = ⨉_{n = 1}^{N} g (n)) \to ((P \in z \land z \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
128	127	exlimiv	$⊢ \exists g ((g Fn (1 \dots N) \land \forall n \in (1 \dots N) g (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists z \in Fin \forall n \in ((1 \dots N) ∖ z) g (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land z = ⨉_{n = 1}^{N} g (n)) \to ((P \in z \land z \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
129	13 128	sylbi	$⊢ z \in \{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\} \to ((P \in z \land z \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S)$
130	129	rexlimiv	$⊢ \exists z \in \{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\} (P \in z \land z \subseteq S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S$
131	12 130	syl	$⊢ (S \in topGen (\{x \| \exists h ((h Fn (1 \dots N) \land \forall n \in (1 \dots N) h (n) \in ((1 \dots N) \times \{topGen (ran (.))\}) (n) \land \exists w \in Fin \forall n \in ((1 \dots N) ∖ w) h (n) = ⋃ ((1 \dots N) \times \{topGen (ran (.))\}) (n)) \land x = ⨉_{n = 1}^{N} h (n))\}) \land P \in S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S$
132	11 131	sylanb	$⊢ (S \in R \land P \in S) \to \exists d \in ℝ^{+} ⨉_{n = 1}^{N} (P (n) ball (D) d) \subseteq S$

Metamath Proof Explorer

Theorem ptrecube

Proof