hoiqssbl

Description: A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hoiqssbl.x	$⊢ φ \to X \in Fin$
	hoiqssbl.y	$⊢ φ \to Y \in (ℝ^{X})$
	hoiqssbl.e	$⊢ φ \to E \in ℝ^{+}$
Assertion	hoiqssbl	$⊢ φ \to \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E)$

Proof

Step	Hyp	Ref	Expression
1		hoiqssbl.x	$⊢ φ \to X \in Fin$
2		hoiqssbl.y	$⊢ φ \to Y \in (ℝ^{X})$
3		hoiqssbl.e	$⊢ φ \to E \in ℝ^{+}$
4		0ex	$⊢ \emptyset \in V$
5	4	snid	$⊢ \emptyset \in \{\emptyset\}$
6	5	a1i	$⊢ (φ \land X = \emptyset) \to \emptyset \in \{\emptyset\}$
7	2	adantr	$⊢ (φ \land X = \emptyset) \to Y \in (ℝ^{X})$
8		oveq2	$⊢ X = \emptyset \to ℝ^{X} = ℝ^{\emptyset}$
9		reex	$⊢ ℝ \in V$
10		mapdm0	$⊢ ℝ \in V \to ℝ^{\emptyset} = \{\emptyset\}$
11	9 10	ax-mp	$⊢ ℝ^{\emptyset} = \{\emptyset\}$
12	11	a1i	$⊢ X = \emptyset \to ℝ^{\emptyset} = \{\emptyset\}$
13	8 12	eqtrd	$⊢ X = \emptyset \to ℝ^{X} = \{\emptyset\}$
14	13	adantl	$⊢ (φ \land X = \emptyset) \to ℝ^{X} = \{\emptyset\}$
15	7 14	eleqtrd	$⊢ (φ \land X = \emptyset) \to Y \in \{\emptyset\}$
16		0fin	$⊢ \emptyset \in Fin$
17		eqid	$⊢ dist (msup) = dist (msup)$
18	17	rrxmetfi	$⊢ \emptyset \in Fin \to dist (msup) \in Met (ℝ^{\emptyset})$
19	16 18	ax-mp	$⊢ dist (msup) \in Met (ℝ^{\emptyset})$
20		metxmet	$⊢ dist (msup) \in Met (ℝ^{\emptyset}) \to dist (msup) \in ∞Met (ℝ^{\emptyset})$
21	19 20	ax-mp	$⊢ dist (msup) \in ∞Met (ℝ^{\emptyset})$
22	21	a1i	$⊢ (φ \land X = \emptyset) \to dist (msup) \in ∞Met (ℝ^{\emptyset})$
23	6 11	eleqtrrdi	$⊢ (φ \land X = \emptyset) \to \emptyset \in (ℝ^{\emptyset})$
24	3	adantr	$⊢ (φ \land X = \emptyset) \to E \in ℝ^{+}$
25		blcntr	$⊢ (dist (msup) \in ∞Met (ℝ^{\emptyset}) \land \emptyset \in (ℝ^{\emptyset}) \land E \in ℝ^{+}) \to \emptyset \in (\emptyset ball (dist (msup)) E)$
26	22 23 24 25	syl3anc	$⊢ (φ \land X = \emptyset) \to \emptyset \in (\emptyset ball (dist (msup)) E)$
27		elsni	$⊢ Y \in \{\emptyset\} \to Y = \emptyset$
28	15 27	syl	$⊢ (φ \land X = \emptyset) \to Y = \emptyset$
29	28	eqcomd	$⊢ (φ \land X = \emptyset) \to \emptyset = Y$
30	29	oveq1d	$⊢ (φ \land X = \emptyset) \to \emptyset ball (dist (msup)) E = Y ball (dist (msup)) E$
31	26 30	eleqtrd	$⊢ (φ \land X = \emptyset) \to \emptyset \in (Y ball (dist (msup)) E)$
32	31	snssd	$⊢ (φ \land X = \emptyset) \to \{\emptyset\} \subseteq Y ball (dist (msup)) E$
33	15 32	jca	$⊢ (φ \land X = \emptyset) \to (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)$
34		biidd	$⊢ d = \emptyset \to ((Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E) \leftrightarrow (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
35	34	rspcev	$⊢ (\emptyset \in \{\emptyset\} \land (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)) \to \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)$
36	6 33 35	syl2anc	$⊢ (φ \land X = \emptyset) \to \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)$
37		biidd	$⊢ c = \emptyset \to (\exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E) \leftrightarrow \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
38	37	rspcev	$⊢ (\emptyset \in \{\emptyset\} \land \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)) \to \exists c \in \{\emptyset\} \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)$
39	6 36 38	syl2anc	$⊢ (φ \land X = \emptyset) \to \exists c \in \{\emptyset\} \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)$
40		oveq2	$⊢ X = \emptyset \to ℚ^{X} = ℚ^{\emptyset}$
41		qex	$⊢ ℚ \in V$
42		mapdm0	$⊢ ℚ \in V \to ℚ^{\emptyset} = \{\emptyset\}$
43	41 42	ax-mp	$⊢ ℚ^{\emptyset} = \{\emptyset\}$
44	43	a1i	$⊢ X = \emptyset \to ℚ^{\emptyset} = \{\emptyset\}$
45	40 44	eqtr2d	$⊢ X = \emptyset \to \{\emptyset\} = ℚ^{X}$
46	45	eqcomd	$⊢ X = \emptyset \to ℚ^{X} = \{\emptyset\}$
47	46	eleq2d	$⊢ X = \emptyset \to (c \in (ℚ^{X}) \leftrightarrow c \in \{\emptyset\})$
48	46	eleq2d	$⊢ X = \emptyset \to (d \in (ℚ^{X}) \leftrightarrow d \in \{\emptyset\})$
49	48	anbi1d	$⊢ X = \emptyset \to ((d \in (ℚ^{X}) \land (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)) \leftrightarrow (d \in \{\emptyset\} \land (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)))$
50	49	rexbidv2	$⊢ X = \emptyset \to (\exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E) \leftrightarrow \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
51	47 50	anbi12d	$⊢ X = \emptyset \to ((c \in (ℚ^{X}) \land \exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)) \leftrightarrow (c \in \{\emptyset\} \land \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)))$
52	51	rexbidv2	$⊢ X = \emptyset \to (\exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E) \leftrightarrow \exists c \in \{\emptyset\} \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
53	52	adantl	$⊢ (φ \land X = \emptyset) \to (\exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E) \leftrightarrow \exists c \in \{\emptyset\} \exists d \in \{\emptyset\} (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
54	39 53	mpbird	$⊢ (φ \land X = \emptyset) \to \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E)$
55		ixpeq1	$⊢ X = \emptyset \to \underset{i \in X}{⨉} [c (i), d (i)) = \underset{i \in \emptyset}{⨉} [c (i), d (i))$
56		ixp0x	$⊢ \underset{i \in \emptyset}{⨉} [c (i), d (i)) = \{\emptyset\}$
57	56	a1i	$⊢ X = \emptyset \to \underset{i \in \emptyset}{⨉} [c (i), d (i)) = \{\emptyset\}$
58	55 57	eqtrd	$⊢ X = \emptyset \to \underset{i \in X}{⨉} [c (i), d (i)) = \{\emptyset\}$
59	58	eleq2d	$⊢ X = \emptyset \to (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \leftrightarrow Y \in \{\emptyset\})$
60		2fveq3	$⊢ X = \emptyset \to dist (msup) = dist (msup)$
61	60	fveq2d	$⊢ X = \emptyset \to ball (dist (msup)) = ball (dist (msup))$
62	61	oveqd	$⊢ X = \emptyset \to Y ball (dist (msup)) E = Y ball (dist (msup)) E$
63	58 62	sseq12d	$⊢ X = \emptyset \to (\underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E \leftrightarrow \{\emptyset\} \subseteq Y ball (dist (msup)) E)$
64	59 63	anbi12d	$⊢ X = \emptyset \to ((Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E) \leftrightarrow (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
65	64	rexbidv	$⊢ X = \emptyset \to (\exists d \in (ℚ^{X}) (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E) \leftrightarrow \exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
66	65	rexbidv	$⊢ X = \emptyset \to (\exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E) \leftrightarrow \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
67	66	adantl	$⊢ (φ \land X = \emptyset) \to (\exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E) \leftrightarrow \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \{\emptyset\} \land \{\emptyset\} \subseteq Y ball (dist (msup)) E))$
68	54 67	mpbird	$⊢ (φ \land X = \emptyset) \to \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E)$
69	1	adantr	$⊢ (φ \land \neg X = \emptyset) \to X \in Fin$
70		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
71	70	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
72	2	adantr	$⊢ (φ \land \neg X = \emptyset) \to Y \in (ℝ^{X})$
73	3	adantr	$⊢ (φ \land \neg X = \emptyset) \to E \in ℝ^{+}$
74	69 71 72 73	hoiqssbllem3	$⊢ (φ \land \neg X = \emptyset) \to \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E)$
75	68 74	pm2.61dan	$⊢ φ \to \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (Y \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq Y ball (dist (msup)) E)$

Metamath Proof Explorer

Theorem hoiqssbl

Proof