sstotbnd3

Description: Use a net that is not necessarily finite, but for which only finitely many balls meet the subset. (Contributed by Mario Carneiro, 14-Sep-2015)

		Ref	Expression
	Hypothesis	sstotbnd.2	$⊢ N = {M ↾}_{(Y \times Y)}$
	Assertion	sstotbnd3	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin))$

Proof

Step	Hyp	Ref	Expression
1		sstotbnd.2	$⊢ N = {M ↾}_{(Y \times Y)}$
2	1	sstotbnd2	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in v} (x ball (M) d))$
3		elin	$⊢ v \in (𝒫 X \cap Fin) \leftrightarrow (v \in 𝒫 X \land v \in Fin)$
4		rabfi	$⊢ v \in Fin \to \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin$
5	4	anim2i	$⊢ (v \in 𝒫 X \land v \in Fin) \to (v \in 𝒫 X \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)$
6	3 5	sylbi	$⊢ v \in (𝒫 X \cap Fin) \to (v \in 𝒫 X \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)$
7	6	anim2i	$⊢ (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land v \in (𝒫 X \cap Fin)) \to (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land (v \in 𝒫 X \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin))$
8	7	ancoms	$⊢ (v \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in v} (x ball (M) d)) \to (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land (v \in 𝒫 X \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin))$
9		an12	$⊢ (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land (v \in 𝒫 X \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)) \leftrightarrow (v \in 𝒫 X \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin))$
10	8 9	sylib	$⊢ (v \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in v} (x ball (M) d)) \to (v \in 𝒫 X \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin))$
11	10	reximi2	$⊢ \exists v \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in v} (x ball (M) d) \to \exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)$
12	11	ralimi	$⊢ \forall d \in ℝ^{+} \exists v \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in v} (x ball (M) d) \to \forall d \in ℝ^{+} \exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)$
13	2 12	biimtrdi	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \to \forall d \in ℝ^{+} \exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin))$
14		ssrab2	$⊢ \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \subseteq v$
15		elpwi	$⊢ v \in 𝒫 X \to v \subseteq X$
16	15	ad2antlr	$⊢ (((M \in Met (X) \land Y \subseteq X) \land v \in 𝒫 X) \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)) \to v \subseteq X$
17	14 16	sstrid	$⊢ (((M \in Met (X) \land Y \subseteq X) \land v \in 𝒫 X) \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)) \to \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \subseteq X$
18		simprr	$⊢ (((M \in Met (X) \land Y \subseteq X) \land v \in 𝒫 X) \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)) \to \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin$
19		elfpw	$⊢ \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in (𝒫 X \cap Fin) \leftrightarrow (\{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \subseteq X \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)$
20	17 18 19	sylanbrc	$⊢ (((M \in Met (X) \land Y \subseteq X) \land v \in 𝒫 X) \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)) \to \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in (𝒫 X \cap Fin)$
21		ssel2	$⊢ (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land z \in Y) \to z \in ⋃_{x \in v} (x ball (M) d)$
22		eliun	$⊢ z \in ⋃_{x \in v} (x ball (M) d) \leftrightarrow \exists x \in v z \in (x ball (M) d)$
23	21 22	sylib	$⊢ (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land z \in Y) \to \exists x \in v z \in (x ball (M) d)$
24		inelcm	$⊢ (z \in (x ball (M) d) \land z \in Y) \to (x ball (M) d) \cap Y \neq \emptyset$
25	24	expcom	$⊢ z \in Y \to (z \in (x ball (M) d) \to (x ball (M) d) \cap Y \neq \emptyset)$
26	25	ancrd	$⊢ z \in Y \to (z \in (x ball (M) d) \to ((x ball (M) d) \cap Y \neq \emptyset \land z \in (x ball (M) d)))$
27	26	reximdv	$⊢ z \in Y \to (\exists x \in v z \in (x ball (M) d) \to \exists x \in v ((x ball (M) d) \cap Y \neq \emptyset \land z \in (x ball (M) d)))$
28	27	impcom	$⊢ (\exists x \in v z \in (x ball (M) d) \land z \in Y) \to \exists x \in v ((x ball (M) d) \cap Y \neq \emptyset \land z \in (x ball (M) d))$
29	23 28	sylancom	$⊢ (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land z \in Y) \to \exists x \in v ((x ball (M) d) \cap Y \neq \emptyset \land z \in (x ball (M) d))$
30		eliun	$⊢ z \in ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d) \leftrightarrow \exists y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} z \in (y ball (M) d)$
31		oveq1	$⊢ y = x \to y ball (M) d = x ball (M) d$
32	31	eleq2d	$⊢ y = x \to (z \in (y ball (M) d) \leftrightarrow z \in (x ball (M) d))$
33	32	rexrab2	$⊢ \exists y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} z \in (y ball (M) d) \leftrightarrow \exists x \in v ((x ball (M) d) \cap Y \neq \emptyset \land z \in (x ball (M) d))$
34	30 33	bitri	$⊢ z \in ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d) \leftrightarrow \exists x \in v ((x ball (M) d) \cap Y \neq \emptyset \land z \in (x ball (M) d))$
35	29 34	sylibr	$⊢ (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land z \in Y) \to z \in ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d)$
36	35	ex	$⊢ Y \subseteq ⋃_{x \in v} (x ball (M) d) \to (z \in Y \to z \in ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d))$
37	36	ssrdv	$⊢ Y \subseteq ⋃_{x \in v} (x ball (M) d) \to Y \subseteq ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d)$
38	37	ad2antrl	$⊢ (((M \in Met (X) \land Y \subseteq X) \land v \in 𝒫 X) \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)) \to Y \subseteq ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d)$
39		iuneq1	$⊢ w = \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \to ⋃_{y \in w} (y ball (M) d) = ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d)$
40	39	sseq2d	$⊢ w = \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \to (Y \subseteq ⋃_{y \in w} (y ball (M) d) \leftrightarrow Y \subseteq ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d))$
41	40	rspcev	$⊢ (\{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{y \in \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\}} (y ball (M) d)) \to \exists w \in (𝒫 X \cap Fin) Y \subseteq ⋃_{y \in w} (y ball (M) d)$
42	20 38 41	syl2anc	$⊢ (((M \in Met (X) \land Y \subseteq X) \land v \in 𝒫 X) \land (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin)) \to \exists w \in (𝒫 X \cap Fin) Y \subseteq ⋃_{y \in w} (y ball (M) d)$
43	42	rexlimdva2	$⊢ (M \in Met (X) \land Y \subseteq X) \to (\exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin) \to \exists w \in (𝒫 X \cap Fin) Y \subseteq ⋃_{y \in w} (y ball (M) d))$
44	43	ralimdv	$⊢ (M \in Met (X) \land Y \subseteq X) \to (\forall d \in ℝ^{+} \exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin) \to \forall d \in ℝ^{+} \exists w \in (𝒫 X \cap Fin) Y \subseteq ⋃_{y \in w} (y ball (M) d))$
45	1	sstotbnd2	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists w \in (𝒫 X \cap Fin) Y \subseteq ⋃_{y \in w} (y ball (M) d))$
46	44 45	sylibrd	$⊢ (M \in Met (X) \land Y \subseteq X) \to (\forall d \in ℝ^{+} \exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin) \to N \in TotBnd (Y))$
47	13 46	impbid	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists v \in 𝒫 X (Y \subseteq ⋃_{x \in v} (x ball (M) d) \land \{x \in v \| (x ball (M) d) \cap Y \neq \emptyset\} \in Fin))$

Metamath Proof Explorer

Theorem sstotbnd3

Proof