Metamath Proof Explorer


Theorem ello12

Description: Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion ello12 ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑦 ) ≤ 𝑚 ) ) )

Proof

Step Hyp Ref Expression
1 reex ℝ ∈ V
2 elpm2r ( ( ( ℝ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
3 1 1 2 mpanl12 ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
4 ello1 ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹𝑦 ) ≤ 𝑚 ) )
5 4 baib ( 𝐹 ∈ ( ℝ ↑pm ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹𝑦 ) ≤ 𝑚 ) )
6 3 5 syl ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹𝑦 ) ≤ 𝑚 ) )
7 elin ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦 ∈ dom 𝐹𝑦 ∈ ( 𝑥 [,) +∞ ) ) )
8 fdm ( 𝐹 : 𝐴 ⟶ ℝ → dom 𝐹 = 𝐴 )
9 8 ad3antrrr ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → dom 𝐹 = 𝐴 )
10 9 eleq2d ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ dom 𝐹𝑦𝐴 ) )
11 10 anbi1d ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑦 ∈ ( 𝑥 [,) +∞ ) ) ) )
12 simpllr ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → 𝐴 ⊆ ℝ )
13 12 sselda ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ )
14 simpllr ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → 𝑥 ∈ ℝ )
15 elicopnf ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥𝑦 ) ) )
16 14 15 syl ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥𝑦 ) ) )
17 13 16 mpbirand ( ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑦 ∈ ( 𝑥 [,) +∞ ) ↔ 𝑥𝑦 ) )
18 17 pm5.32da ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦𝐴𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑥𝑦 ) ) )
19 11 18 bitrd ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ dom 𝐹𝑦 ∈ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑥𝑦 ) ) )
20 7 19 syl5bb ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ↔ ( 𝑦𝐴𝑥𝑦 ) ) )
21 20 imbi1d ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( 𝐹𝑦 ) ≤ 𝑚 ) ↔ ( ( 𝑦𝐴𝑥𝑦 ) → ( 𝐹𝑦 ) ≤ 𝑚 ) ) )
22 impexp ( ( ( 𝑦𝐴𝑥𝑦 ) → ( 𝐹𝑦 ) ≤ 𝑚 ) ↔ ( 𝑦𝐴 → ( 𝑥𝑦 → ( 𝐹𝑦 ) ≤ 𝑚 ) ) )
23 21 22 bitrdi ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( 𝐹𝑦 ) ≤ 𝑚 ) ↔ ( 𝑦𝐴 → ( 𝑥𝑦 → ( 𝐹𝑦 ) ≤ 𝑚 ) ) ) )
24 23 ralbidv2 ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹𝑦 ) ≤ 𝑚 ↔ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑦 ) ≤ 𝑚 ) ) )
25 24 rexbidva ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹𝑦 ) ≤ 𝑚 ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑦 ) ≤ 𝑚 ) ) )
26 25 rexbidva ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹𝑦 ) ≤ 𝑚 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑦 ) ≤ 𝑚 ) ) )
27 6 26 bitrd ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( 𝐹𝑦 ) ≤ 𝑚 ) ) )