bcthlem1

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

	Ref	Expression
Hypotheses	bcth.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	bcthlem.4	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
	bcthlem.5	⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ⁺ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } )
Assertion	bcthlem1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 𝑋 × ℝ⁺ ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bcth.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		bcthlem.4	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
3		bcthlem.5	⊢ 𝐹 = ( 𝑘 ∈ ℕ , 𝑧 ∈ ( 𝑋 × ℝ⁺ ) ↦ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } )
4		opabssxp	⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ⊆ ( 𝑋 × ℝ⁺ )
5		elfvdm	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝑋 ∈ dom CMet )
6	2 5	syl	⊢ ( 𝜑 → 𝑋 ∈ dom CMet )
7		reex	⊢ ℝ ∈ V
8		rpssre	⊢ ℝ⁺ ⊆ ℝ
9	7 8	ssexi	⊢ ℝ⁺ ∈ V
10		xpexg	⊢ ( ( 𝑋 ∈ dom CMet ∧ ℝ⁺ ∈ V ) → ( 𝑋 × ℝ⁺ ) ∈ V )
11	6 9 10	sylancl	⊢ ( 𝜑 → ( 𝑋 × ℝ⁺ ) ∈ V )
12		ssexg	⊢ ( ( { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ⊆ ( 𝑋 × ℝ⁺ ) ∧ ( 𝑋 × ℝ⁺ ) ∈ V ) → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ∈ V )
13	4 11 12	sylancr	⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ∈ V )
14		oveq2	⊢ ( 𝑘 = 𝐴 → ( 1 / 𝑘 ) = ( 1 / 𝐴 ) )
15	14	breq2d	⊢ ( 𝑘 = 𝐴 → ( 𝑟 < ( 1 / 𝑘 ) ↔ 𝑟 < ( 1 / 𝐴 ) ) )
16		fveq2	⊢ ( 𝑘 = 𝐴 → ( 𝑀 ‘ 𝑘 ) = ( 𝑀 ‘ 𝐴 ) )
17	16	difeq2d	⊢ ( 𝑘 = 𝐴 → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) = ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) )
18	17	sseq2d	⊢ ( 𝑘 = 𝐴 → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) )
19	15 18	anbi12d	⊢ ( 𝑘 = 𝐴 → ( ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ↔ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
20	19	anbi2d	⊢ ( 𝑘 = 𝐴 → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ) )
21	20	opabbidv	⊢ ( 𝑘 = 𝐴 → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝑘 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝑘 ) ) ) ) } = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } )
22		fveq2	⊢ ( 𝑧 = 𝐵 → ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) = ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) )
23	22	difeq1d	⊢ ( 𝑧 = 𝐵 → ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) = ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) )
24	23	sseq2d	⊢ ( 𝑧 = 𝐵 → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) )
25	24	anbi2d	⊢ ( 𝑧 = 𝐵 → ( ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ↔ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
26	25	anbi2d	⊢ ( 𝑧 = 𝐵 → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ) )
27	26	opabbidv	⊢ ( 𝑧 = 𝐵 → { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝑧 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } )
28	21 27 3	ovmpog	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 𝑋 × ℝ⁺ ) ∧ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ∈ V ) → ( 𝐴 𝐹 𝐵 ) = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } )
29	13 28	syl3an3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 𝑋 × ℝ⁺ ) ∧ 𝜑 ) → ( 𝐴 𝐹 𝐵 ) = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } )
30	29	3expa	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 𝑋 × ℝ⁺ ) ) ∧ 𝜑 ) → ( 𝐴 𝐹 𝐵 ) = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } )
31	30	ancoms	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 𝑋 × ℝ⁺ ) ) ) → ( 𝐴 𝐹 𝐵 ) = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } )
32	31	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 𝑋 × ℝ⁺ ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) ↔ 𝐶 ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ) )
33	4	sseli	⊢ ( 𝐶 ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } → 𝐶 ∈ ( 𝑋 × ℝ⁺ ) )
34		simp1	⊢ ( ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) → 𝐶 ∈ ( 𝑋 × ℝ⁺ ) )
35		1st2nd2	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → 𝐶 = ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ )
36	35	eleq1d	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( 𝐶 ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ↔ ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ) )
37		fvex	⊢ ( 1^st ‘ 𝐶 ) ∈ V
38		fvex	⊢ ( 2^nd ‘ 𝐶 ) ∈ V
39		eleq1	⊢ ( 𝑥 = ( 1^st ‘ 𝐶 ) → ( 𝑥 ∈ 𝑋 ↔ ( 1^st ‘ 𝐶 ) ∈ 𝑋 ) )
40		eleq1	⊢ ( 𝑟 = ( 2^nd ‘ 𝐶 ) → ( 𝑟 ∈ ℝ⁺ ↔ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) )
41	39 40	bi2anan9	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ↔ ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) ) )
42		simpr	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → 𝑟 = ( 2^nd ‘ 𝐶 ) )
43	42	breq1d	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → ( 𝑟 < ( 1 / 𝐴 ) ↔ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ) )
44		oveq12	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) = ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) )
45	44	fveq2d	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) = ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) )
46	45	sseq1d	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) )
47	43 46	anbi12d	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → ( ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ↔ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
48	41 47	anbi12d	⊢ ( ( 𝑥 = ( 1^st ‘ 𝐶 ) ∧ 𝑟 = ( 2^nd ‘ 𝐶 ) ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ↔ ( ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) ∧ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ) )
49	37 38 48	opelopaba	⊢ ( ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ↔ ( ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) ∧ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
50	36 49	bitrdi	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( 𝐶 ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ↔ ( ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) ∧ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ) )
51	35	eleq1d	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ↔ ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ∈ ( 𝑋 × ℝ⁺ ) ) )
52		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ∈ ( 𝑋 × ℝ⁺ ) ↔ ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) )
53	51 52	bitr2di	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) ↔ 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ) )
54		df-ov	⊢ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ )
55	35	fveq2d	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) = ( ( ball ‘ 𝐷 ) ‘ ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ) )
56	54 55	eqtr4id	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) = ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) )
57	56	fveq2d	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) = ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) )
58	57	sseq1d	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) )
59	58	anbi2d	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ↔ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
60	53 59	anbi12d	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) ∧ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ↔ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ) )
61		3anass	⊢ ( ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ↔ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
62	60 61	bitr4di	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( ( ( ( 1^st ‘ 𝐶 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝐶 ) ∈ ℝ⁺ ) ∧ ( ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( 1^st ‘ 𝐶 ) ( ball ‘ 𝐷 ) ( 2^nd ‘ 𝐶 ) ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) ↔ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
63	50 62	bitrd	⊢ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) → ( 𝐶 ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ↔ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )
64	33 34 63	pm5.21nii	⊢ ( 𝐶 ∈ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ∧ ( 𝑟 < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) } ↔ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) )
65	32 64	bitrdi	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( 𝑋 × ℝ⁺ ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐹 𝐵 ) ↔ ( 𝐶 ∈ ( 𝑋 × ℝ⁺ ) ∧ ( 2^nd ‘ 𝐶 ) < ( 1 / 𝐴 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( ( ball ‘ 𝐷 ) ‘ 𝐶 ) ) ⊆ ( ( ( ball ‘ 𝐷 ) ‘ 𝐵 ) ∖ ( 𝑀 ‘ 𝐴 ) ) ) ) )

Metamath Proof Explorer

Theorem bcthlem1

Proof