Metamath Proof Explorer

Theorem ello1mpt

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

Ref Expression
Hypotheses ello1mpt.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
ello1mpt.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion ello1mpt ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )

Proof

Step Hyp Ref Expression
1 ello1mpt.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ello1mpt.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 2 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
4 ello12 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 ) ) )
5 3 1 4 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 ) ) )
6 nfv ⊢ Ⅎ 𝑥 𝑦 ≤ 𝑧
7 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 )
8 nfcv ⊢ Ⅎ 𝑥 ≤
9 nfcv ⊢ Ⅎ 𝑥 𝑚
10 7 8 9 nfbr ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚
11 6 10 nfim ⊢ Ⅎ 𝑥 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 )
12 nfv ⊢ Ⅎ 𝑧 ( 𝑦 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ≤ 𝑚 )
13 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ≤ 𝑥 ) )
14 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
15 14 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ≤ 𝑚 ) )
16 13 15 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 ) ↔ ( 𝑦 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ≤ 𝑚 ) ) )
17 11 12 16 cbvralw ⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ≤ 𝑚 ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
19 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
20 19 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
21 18 2 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
22 21 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ≤ 𝑚 ↔ 𝐵 ≤ 𝑚 ) )
23 22 imbi2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ≤ 𝑚 ) ↔ ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
24 23 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
25 17 24 bitrid ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
26 25 2rexbidv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ≤ 𝑚 ) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
27 5 26 bitrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )