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