Theorem 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	$$⊢\phi \to X\in \mathrm{Fin}$$
	hoiqssbl.y	$$⊢\phi \to Y\in \left({ℝ}^X\right)$$
	hoiqssbl.e	$$⊢\phi \to E\in {ℝ}^{+}$$
Assertion	hoiqssbl

Proof

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