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 ⊢φ→A⊆ℝ
ello1mpt.2 ⊢φ∧x∈A→B∈ℝ
Assertion ello1mpt ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→B≤m

Proof

Step Hyp Ref Expression
1 ello1mpt.1 ⊢φ→A⊆ℝ
2 ello1mpt.2 ⊢φ∧x∈A→B∈ℝ
3 2 fmpttd ⊢φ→x∈A⟼B:A⟶ℝ
4 ello12 ⊢x∈A⟼B:A⟶ℝ∧A⊆ℝ→x∈A⟼B∈≤𝑂⁡1↔∃y∈ℝ∃m∈ℝ∀z∈Ay≤z→x∈A⟼B⁡z≤m
5 3 1 4 syl2anc ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃y∈ℝ∃m∈ℝ∀z∈Ay≤z→x∈A⟼B⁡z≤m
6 nfv ⊢Ⅎxy≤z
7 nffvmpt1 ⊢Ⅎ_xx∈A⟼B⁡z
8 nfcv ⊢Ⅎ_x≤
9 nfcv ⊢Ⅎ_xm
10 7 8 9 nfbr ⊢Ⅎxx∈A⟼B⁡z≤m
11 6 10 nfim ⊢Ⅎxy≤z→x∈A⟼B⁡z≤m
12 nfv ⊢Ⅎzy≤x→x∈A⟼B⁡x≤m
13 breq2 ⊢z=x→y≤z↔y≤x
14 fveq2 ⊢z=x→x∈A⟼B⁡z=x∈A⟼B⁡x
15 14 breq1d ⊢z=x→x∈A⟼B⁡z≤m↔x∈A⟼B⁡x≤m
16 13 15 imbi12d ⊢z=x→y≤z→x∈A⟼B⁡z≤m↔y≤x→x∈A⟼B⁡x≤m
17 11 12 16 cbvralw ⊢∀z∈Ay≤z→x∈A⟼B⁡z≤m↔∀x∈Ay≤x→x∈A⟼B⁡x≤m
18 simpr ⊢φ∧x∈A→x∈A
19 eqid ⊢x∈A⟼B=x∈A⟼B
20 19 fvmpt2 ⊢x∈A∧B∈ℝ→x∈A⟼B⁡x=B
21 18 2 20 syl2anc ⊢φ∧x∈A→x∈A⟼B⁡x=B
22 21 breq1d ⊢φ∧x∈A→x∈A⟼B⁡x≤m↔B≤m
23 22 imbi2d ⊢φ∧x∈A→y≤x→x∈A⟼B⁡x≤m↔y≤x→B≤m
24 23 ralbidva ⊢φ→∀x∈Ay≤x→x∈A⟼B⁡x≤m↔∀x∈Ay≤x→B≤m
25 17 24 bitrid ⊢φ→∀z∈Ay≤z→x∈A⟼B⁡z≤m↔∀x∈Ay≤x→B≤m
26 25 2rexbidv ⊢φ→∃y∈ℝ∃m∈ℝ∀z∈Ay≤z→x∈A⟼B⁡z≤m↔∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→B≤m
27 5 26 bitrd ⊢φ→x∈A⟼B∈≤𝑂⁡1↔∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→B≤m