Metamath Proof Explorer

Theorem lo1eq

Description: Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses lo1eq.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
lo1eq.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
lo1eq.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
lo1eq.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 = 𝐶 )
Assertion lo1eq ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) )

Proof

Step Hyp Ref Expression
1 lo1eq.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 lo1eq.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
3 lo1eq.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
4 lo1eq.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 = 𝐶 )
5 lo1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
6 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7 6 1 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
8 7 sseq1d ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ↔ 𝐴 ⊆ ℝ ) )
9 5 8 imbitrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → 𝐴 ⊆ ℝ ) )
10 lo1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ℝ )
11 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
12 11 2 dmmptd ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = 𝐴 )
13 12 sseq1d ⊢ ( 𝜑 → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⊆ ℝ ↔ 𝐴 ⊆ ℝ ) )
14 10 13 imbitrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) → 𝐴 ⊆ ℝ ) )
15 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐷 [,) +∞ ) ) )
16 15 bilani ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐷 [,) +∞ ) ) )
17 16 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) → 𝑥 ∈ 𝐴 )
18 16 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) → 𝑥 ∈ ( 𝐷 [,) +∞ ) )
19 elicopnf ⊢ ( 𝐷 ∈ ℝ → ( 𝑥 ∈ ( 𝐷 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐷 ≤ 𝑥 ) ) )
20 3 19 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐷 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐷 ≤ 𝑥 ) ) )
21 20 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐷 [,) +∞ ) ) → ( 𝑥 ∈ ℝ ∧ 𝐷 ≤ 𝑥 ) )
22 18 21 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝐷 ≤ 𝑥 ) )
23 22 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) → 𝐷 ≤ 𝑥 )
24 17 23 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝐷 ≤ 𝑥 ) )
25 24 4 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) → 𝐵 = 𝐶 )
26 25 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ↦ 𝐶 ) )
27 inss1 ⊢ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ⊆ 𝐴
28 resmpt ⊢ ( ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ↦ 𝐵 ) )
29 27 28 ax-mp ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ↦ 𝐵 )
30 resmpt ⊢ ( ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ↦ 𝐶 ) )
31 27 30 ax-mp ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) = ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ↦ 𝐶 )
32 26 29 31 3eqtr4g ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) ) )
33 resres ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) )
34 resres ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐴 ∩ ( 𝐷 [,) +∞ ) ) )
35 32 33 34 3eqtr4g ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) )
36 ssid ⊢ 𝐴 ⊆ 𝐴
37 resmpt ⊢ ( 𝐴 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
38 reseq1 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) )
39 36 37 38 mp2b ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) )
40 resmpt ⊢ ( 𝐴 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
41 reseq1 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) )
42 36 40 41 mp2b ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ 𝐴 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) )
43 35 39 42 3eqtr3g ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) )
44 43 eleq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) ∈ ≤𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) ∈ ≤𝑂(1) ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) ∈ ≤𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) ∈ ≤𝑂(1) ) )
46 1 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℝ )
48 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → 𝐴 ⊆ ℝ )
49 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → 𝐷 ∈ ℝ )
50 47 48 49 lo1resb ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ ( 𝐷 [,) +∞ ) ) ∈ ≤𝑂(1) ) )
51 2 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℝ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℝ )
53 52 48 49 lo1resb ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ↾ ( 𝐷 [,) +∞ ) ) ∈ ≤𝑂(1) ) )
54 45 50 53 3bitr4d ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ℝ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) )
55 54 ex ⊢ ( 𝜑 → ( 𝐴 ⊆ ℝ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) ) )
56 9 14 55 pm5.21ndd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) )