Metamath Proof Explorer

Theorem nmounbi

Description: Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
nmoubi.u ⊢ 𝑈 ∈ NrmCVec
nmoubi.w ⊢ 𝑊 ∈ NrmCVec
Assertion nmounbi ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) = +∞ ↔ ∀ 𝑟 ∈ ℝ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmoubi.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 nmoubi.l ⊢ 𝐿 = ( normCV ‘ 𝑈 )
4 nmoubi.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
5 nmoubi.3 ⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6 nmoubi.u ⊢ 𝑈 ∈ NrmCVec
7 nmoubi.w ⊢ 𝑊 ∈ NrmCVec
8 1 2 3 4 5 6 7 nmobndi ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ) )
9 1 2 5 nmorepnf ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) ≠ +∞ ) )
10 6 7 9 mp3an12 ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) ≠ +∞ ) )
11 ffvelrn ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑦 ) ∈ 𝑌 )
12 2 4 nvcl ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑦 ) ∈ 𝑌 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
13 7 11 12 sylancr ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
14 lenlt ⊢ ( ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ↔ ¬ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
15 13 14 sylan ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ↔ ¬ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
16 15 an32s ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑟 ∈ ℝ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ↔ ¬ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
17 16 imbi2d ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑟 ∈ ℝ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ↔ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ¬ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
18 imnan ⊢ ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ¬ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
19 17 18 bitrdi ⊢ ( ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑟 ∈ ℝ ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ↔ ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
20 19 ralbidva ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑟 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ↔ ∀ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
21 ralnex ⊢ ( ∀ 𝑦 ∈ 𝑋 ¬ ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ¬ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
22 20 21 bitrdi ⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑟 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ↔ ¬ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
23 22 rexbidva ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ↔ ∃ 𝑟 ∈ ℝ ¬ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
24 rexnal ⊢ ( ∃ 𝑟 ∈ ℝ ¬ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ¬ ∀ 𝑟 ∈ ℝ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
25 23 24 bitrdi ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ∃ 𝑟 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 → ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ 𝑟 ) ↔ ¬ ∀ 𝑟 ∈ ℝ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
26 8 10 25 3bitr3d ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) ≠ +∞ ↔ ¬ ∀ 𝑟 ∈ ℝ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
27 26 necon4abid ⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑁 ‘ 𝑇 ) = +∞ ↔ ∀ 𝑟 ∈ ℝ ∃ 𝑦 ∈ 𝑋 ( ( 𝐿 ‘ 𝑦 ) ≤ 1 ∧ 𝑟 < ( 𝑀 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )