bcthlem1

Description: Lemma for bcth . Substitutions for the function F . (Contributed by Mario Carneiro, 9-Jan-2014)

	Ref	Expression
Hypotheses	bcth.2	$⊢ J = MetOpen (D)$
	bcthlem.4	$⊢ φ \to D \in CMet (X)$
	bcthlem.5	$⊢ F = (k \in ℕ, z \in (X \times ℝ^{+}) ⟼ \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\})$
Assertion	bcthlem1	$⊢ (φ \land (A \in ℕ \land B \in (X \times ℝ^{+}))) \to (C \in (A F B) \leftrightarrow (C \in (X \times ℝ^{+}) \land 2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)))$

Proof

Step	Hyp	Ref	Expression
1		bcth.2	$⊢ J = MetOpen (D)$
2		bcthlem.4	$⊢ φ \to D \in CMet (X)$
3		bcthlem.5	$⊢ F = (k \in ℕ, z \in (X \times ℝ^{+}) ⟼ \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\})$
4		opabssxp	$⊢ \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \subseteq X \times ℝ^{+}$
5		elfvdm	$⊢ D \in CMet (X) \to X \in dom CMet$
6	2 5	syl	$⊢ φ \to X \in dom CMet$
7		reex	$⊢ ℝ \in V$
8		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
9	7 8	ssexi	$⊢ ℝ^{+} \in V$
10		xpexg	$⊢ (X \in dom CMet \land ℝ^{+} \in V) \to X \times ℝ^{+} \in V$
11	6 9 10	sylancl	$⊢ φ \to X \times ℝ^{+} \in V$
12		ssexg	$⊢ (\{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \subseteq X \times ℝ^{+} \land X \times ℝ^{+} \in V) \to \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \in V$
13	4 11 12	sylancr	$⊢ φ \to \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \in V$
14		oveq2	$⊢ k = A \to \frac{1}{k} = \frac{1}{A}$
15	14	breq2d	$⊢ k = A \to (r < \frac{1}{k} \leftrightarrow r < \frac{1}{A})$
16		fveq2	$⊢ k = A \to M (k) = M (A)$
17	16	difeq2d	$⊢ k = A \to ball (D) (z) ∖ M (k) = ball (D) (z) ∖ M (A)$
18	17	sseq2d	$⊢ k = A \to (cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k) \leftrightarrow cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A))$
19	15 18	anbi12d	$⊢ k = A \to ((r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)) \leftrightarrow (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A)))$
20	19	anbi2d	$⊢ k = A \to (((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k))) \leftrightarrow ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A))))$
21	20	opabbidv	$⊢ k = A \to \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{k} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (k)))\} = \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A)))\}$
22		fveq2	$⊢ z = B \to ball (D) (z) = ball (D) (B)$
23	22	difeq1d	$⊢ z = B \to ball (D) (z) ∖ M (A) = ball (D) (B) ∖ M (A)$
24	23	sseq2d	$⊢ z = B \to (cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A) \leftrightarrow cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A))$
25	24	anbi2d	$⊢ z = B \to ((r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A)) \leftrightarrow (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))$
26	25	anbi2d	$⊢ z = B \to (((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A))) \leftrightarrow ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A))))$
27	26	opabbidv	$⊢ z = B \to \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (z) ∖ M (A)))\} = \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\}$
28	21 27 3	ovmpog	$⊢ (A \in ℕ \land B \in (X \times ℝ^{+}) \land \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \in V) \to A F B = \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\}$
29	13 28	syl3an3	$⊢ (A \in ℕ \land B \in (X \times ℝ^{+}) \land φ) \to A F B = \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\}$
30	29	3expa	$⊢ ((A \in ℕ \land B \in (X \times ℝ^{+})) \land φ) \to A F B = \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\}$
31	30	ancoms	$⊢ (φ \land (A \in ℕ \land B \in (X \times ℝ^{+}))) \to A F B = \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\}$
32	31	eleq2d	$⊢ (φ \land (A \in ℕ \land B \in (X \times ℝ^{+}))) \to (C \in (A F B) \leftrightarrow C \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\})$
33	4	sseli	$⊢ C \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \to C \in (X \times ℝ^{+})$
34		simp1	$⊢ (C \in (X \times ℝ^{+}) \land 2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)) \to C \in (X \times ℝ^{+})$
35		1st2nd2	$⊢ C \in (X \times ℝ^{+}) \to C = ⟨1^{st} (C), 2^{nd} (C)⟩$
36	35	eleq1d	$⊢ C \in (X \times ℝ^{+}) \to (C \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \leftrightarrow ⟨1^{st} (C), 2^{nd} (C)⟩ \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\})$
37		fvex	$⊢ 1^{st} (C) \in V$
38		fvex	$⊢ 2^{nd} (C) \in V$
39		eleq1	$⊢ x = 1^{st} (C) \to (x \in X \leftrightarrow 1^{st} (C) \in X)$
40		eleq1	$⊢ r = 2^{nd} (C) \to (r \in ℝ^{+} \leftrightarrow 2^{nd} (C) \in ℝ^{+})$
41	39 40	bi2anan9	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to ((x \in X \land r \in ℝ^{+}) \leftrightarrow (1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+}))$
42		simpr	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to r = 2^{nd} (C)$
43	42	breq1d	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to (r < \frac{1}{A} \leftrightarrow 2^{nd} (C) < \frac{1}{A})$
44		oveq12	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to x ball (D) r = 1^{st} (C) ball (D) 2^{nd} (C)$
45	44	fveq2d	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to cls (J) (x ball (D) r) = cls (J) (1^{st} (C) ball (D) 2^{nd} (C))$
46	45	sseq1d	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to (cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A) \leftrightarrow cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A))$
47	43 46	anbi12d	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to ((r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)) \leftrightarrow (2^{nd} (C) < \frac{1}{A} \land cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A)))$
48	41 47	anbi12d	$⊢ (x = 1^{st} (C) \land r = 2^{nd} (C)) \to (((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A))) \leftrightarrow ((1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+}) \land (2^{nd} (C) < \frac{1}{A} \land cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A))))$
49	37 38 48	opelopaba	$⊢ ⟨1^{st} (C), 2^{nd} (C)⟩ \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \leftrightarrow ((1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+}) \land (2^{nd} (C) < \frac{1}{A} \land cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A)))$
50	36 49	bitrdi	$⊢ C \in (X \times ℝ^{+}) \to (C \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \leftrightarrow ((1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+}) \land (2^{nd} (C) < \frac{1}{A} \land cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A))))$
51	35	eleq1d	$⊢ C \in (X \times ℝ^{+}) \to (C \in (X \times ℝ^{+}) \leftrightarrow ⟨1^{st} (C), 2^{nd} (C)⟩ \in (X \times ℝ^{+}))$
52		opelxp	$⊢ ⟨1^{st} (C), 2^{nd} (C)⟩ \in (X \times ℝ^{+}) \leftrightarrow (1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+})$
53	51 52	bitr2di	$⊢ C \in (X \times ℝ^{+}) \to ((1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+}) \leftrightarrow C \in (X \times ℝ^{+}))$
54		df-ov	$⊢ 1^{st} (C) ball (D) 2^{nd} (C) = ball (D) (⟨1^{st} (C), 2^{nd} (C)⟩)$
55	35	fveq2d	$⊢ C \in (X \times ℝ^{+}) \to ball (D) (C) = ball (D) (⟨1^{st} (C), 2^{nd} (C)⟩)$
56	54 55	eqtr4id	$⊢ C \in (X \times ℝ^{+}) \to 1^{st} (C) ball (D) 2^{nd} (C) = ball (D) (C)$
57	56	fveq2d	$⊢ C \in (X \times ℝ^{+}) \to cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) = cls (J) (ball (D) (C))$
58	57	sseq1d	$⊢ C \in (X \times ℝ^{+}) \to (cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A) \leftrightarrow cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A))$
59	58	anbi2d	$⊢ C \in (X \times ℝ^{+}) \to ((2^{nd} (C) < \frac{1}{A} \land cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A)) \leftrightarrow (2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)))$
60	53 59	anbi12d	$⊢ C \in (X \times ℝ^{+}) \to (((1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+}) \land (2^{nd} (C) < \frac{1}{A} \land cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A))) \leftrightarrow (C \in (X \times ℝ^{+}) \land (2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A))))$
61		3anass	$⊢ (C \in (X \times ℝ^{+}) \land 2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)) \leftrightarrow (C \in (X \times ℝ^{+}) \land (2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)))$
62	60 61	bitr4di	$⊢ C \in (X \times ℝ^{+}) \to (((1^{st} (C) \in X \land 2^{nd} (C) \in ℝ^{+}) \land (2^{nd} (C) < \frac{1}{A} \land cls (J) (1^{st} (C) ball (D) 2^{nd} (C)) \subseteq ball (D) (B) ∖ M (A))) \leftrightarrow (C \in (X \times ℝ^{+}) \land 2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)))$
63	50 62	bitrd	$⊢ C \in (X \times ℝ^{+}) \to (C \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \leftrightarrow (C \in (X \times ℝ^{+}) \land 2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)))$
64	33 34 63	pm5.21nii	$⊢ C \in \{⟨x, r⟩ \| ((x \in X \land r \in ℝ^{+}) \land (r < \frac{1}{A} \land cls (J) (x ball (D) r) \subseteq ball (D) (B) ∖ M (A)))\} \leftrightarrow (C \in (X \times ℝ^{+}) \land 2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A))$
65	32 64	bitrdi	$⊢ (φ \land (A \in ℕ \land B \in (X \times ℝ^{+}))) \to (C \in (A F B) \leftrightarrow (C \in (X \times ℝ^{+}) \land 2^{nd} (C) < \frac{1}{A} \land cls (J) (ball (D) (C)) \subseteq ball (D) (B) ∖ M (A)))$

Metamath Proof Explorer

Theorem bcthlem1

Proof