Theorem ubthlem3

Description: Lemma for ubth . Prove the reverse implication, using nmblolbi . (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ubth.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ubth.2	⊢ 𝑁 = ( normCV ‘ 𝑊 )
	ubthlem.3	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
	ubthlem.4	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	ubthlem.5	⊢ 𝑈 ∈ CBan
	ubthlem.6	⊢ 𝑊 ∈ NrmCVec
	ubthlem.7	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
Assertion	ubthlem3	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )

Proof

Step	Hyp	Ref	Expression
1		ubth.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ubth.2	⊢ 𝑁 = ( normCV ‘ 𝑊 )
3		ubthlem.3	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
4		ubthlem.4	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
5		ubthlem.5	⊢ 𝑈 ∈ CBan
6		ubthlem.6	⊢ 𝑊 ∈ NrmCVec
7		ubthlem.7	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
8		fveq1	⊢ ( 𝑢 = 𝑡 → ( 𝑢 ‘ 𝑧 ) = ( 𝑡 ‘ 𝑧 ) )
9	8	fveq2d	⊢ ( 𝑢 = 𝑡 → ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) )
10	9	breq1d	⊢ ( 𝑢 = 𝑡 → ( ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 ) )
11	10	cbvralvw	⊢ ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 )
12		breq2	⊢ ( 𝑑 = 𝑐 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ) )
13	12	ralbidv	⊢ ( 𝑑 = 𝑐 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ) )
14	11 13	bitrid	⊢ ( 𝑑 = 𝑐 → ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ) )
15	14	cbvrexvw	⊢ ( ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 )
16		2fveq3	⊢ ( 𝑧 = 𝑥 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) )
17	16	breq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
18	17	rexralbidv	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑐 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
19	15 18	bitrid	⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
20	19	cbvralvw	⊢ ( ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
21	7	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
22		simpr	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 )
23	22 20	sylib	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
24		fveq1	⊢ ( 𝑢 = 𝑡 → ( 𝑢 ‘ 𝑑 ) = ( 𝑡 ‘ 𝑑 ) )
25	24	fveq2d	⊢ ( 𝑢 = 𝑡 → ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) )
26	25	breq1d	⊢ ( 𝑢 = 𝑡 → ( ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 ) )
27	26	cbvralvw	⊢ ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 )
28		2fveq3	⊢ ( 𝑑 = 𝑧 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) = ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) )
29	28	breq1d	⊢ ( 𝑑 = 𝑧 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ) )
30	29	ralbidv	⊢ ( 𝑑 = 𝑧 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ) )
31	27 30	bitrid	⊢ ( 𝑑 = 𝑧 → ( ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ) )
32	31	cbvrabv	⊢ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 }
33		breq2	⊢ ( 𝑚 = 𝑘 → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ↔ ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 ) )
34	33	ralbidv	⊢ ( 𝑚 = 𝑘 → ( ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 ↔ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 ) )
35	34	rabbidv	⊢ ( 𝑚 = 𝑘 → { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑚 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
36	32 35	eqtrid	⊢ ( 𝑚 = 𝑘 → { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } = { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
37	36	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) = ( 𝑘 ∈ ℕ ↦ { 𝑧 ∈ 𝑋 ∣ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑧 ) ) ≤ 𝑘 } )
38	1 2 3 4 5 6 21 23 37	ubthlem1	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∃ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) )
39	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) )
40	23	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
41		simplrl	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑛 ∈ ℕ )
42		simplrr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑦 ∈ 𝑋 )
43		simprl	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → 𝑟 ∈ ℝ+ )
44		simprr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) )
45	1 2 3 4 5 6 39 40 37 41 42 43 44	ubthlem2	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) ) ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )
46	45	expr	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
47	46	rexlimdva	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋 ) ) → ( ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
48	47	rexlimdvva	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑦 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ { 𝑧 ∈ 𝑋 ∣ ( 𝑦 𝐷 𝑧 ) ≤ 𝑟 } ⊆ ( ( 𝑚 ∈ ℕ ↦ { 𝑑 ∈ 𝑋 ∣ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑑 ) ) ≤ 𝑚 } ) ‘ 𝑛 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
49	38 48	mpd	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 ) → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )
50	49	ex	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑋 ∃ 𝑑 ∈ ℝ ∀ 𝑢 ∈ 𝑇 ( 𝑁 ‘ ( 𝑢 ‘ 𝑧 ) ) ≤ 𝑑 → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
51	20 50	biimtrrid	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 → ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )
52		simpr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) → 𝑑 ∈ ℝ )
53		bnnv	⊢ ( 𝑈 ∈ CBan → 𝑈 ∈ NrmCVec )
54	5 53	ax-mp	⊢ 𝑈 ∈ NrmCVec
55		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
56	1 55	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ )
57	54 56	mpan	⊢ ( 𝑥 ∈ 𝑋 → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ )
58		remulcl	⊢ ( ( 𝑑 ∈ ℝ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ) → ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
59	52 57 58	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
60	7	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
61	60	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
62	61	ad2ant2r	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) )
63		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
64		eqid	⊢ ( 𝑈 BLnOp 𝑊 ) = ( 𝑈 BLnOp 𝑊 )
65	1 63 64	blof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
66	54 6 65	mp3an12	⊢ ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
67	62 66	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
68		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑥 ∈ 𝑋 )
69	67 68	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) )
70	63 2	nvcl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
71	6 70	mpan	⊢ ( ( 𝑡 ‘ 𝑥 ) ∈ ( BaseSet ‘ 𝑊 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
72	69 71	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ∈ ℝ )
73		eqid	⊢ ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
74	1 63 73	nmoxr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* )
75	54 6 74	mp3an12	⊢ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* )
76	67 75	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* )
77		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → 𝑑 ∈ ℝ )
78	1 63 73	nmogtmnf	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) → -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) )
79	54 6 78	mp3an12	⊢ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) → -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) )
80	67 79	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) )
81		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 )
82		xrre	⊢ ( ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ* ∧ 𝑑 ∈ ℝ ) ∧ ( -∞ < ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ )
83	76 77 80 81 82	syl22anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ )
84	57	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ )
85		remulcl	⊢ ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ ∧ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
86	83 84 85	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
87	59	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ )
88	1 55 2 73 64 54 6	nmblolbi	⊢ ( ( 𝑡 ∈ ( 𝑈 BLnOp 𝑊 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
89	62 68 88	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
90	1 55	nvge0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) )
91	54 90	mpan	⊢ ( 𝑥 ∈ 𝑋 → 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) )
92	57 91	jca	⊢ ( 𝑥 ∈ 𝑋 → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
93	92	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
94		lemul1a	⊢ ( ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
95	83 77 93 81 94	syl31anc	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
96	72 86 87 89 95	letrd	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) )
97	96	expr	⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
98	97	ralimdva	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) )
99		brralrspcev	⊢ ( ( ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∈ ℝ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ ( 𝑑 · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 )
100	59 98 99	syl6an	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
101	100	ralrimdva	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ℝ ) → ( ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
102	101	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) )
103	51 102	impbid	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) )