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 syl6bb ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) ) )
24 23 ralbidv2 ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )
25 24 rexbidva ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )
26 25 rexbidva ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )
27 6 26 bitrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ ≤𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) ) )