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	$⊢ (φ \land x \in A) \to B \in ℝ$
	lo1eq.2	$⊢ (φ \land x \in A) \to C \in ℝ$
	lo1eq.3	$⊢ φ \to D \in ℝ$
	lo1eq.4	$⊢ (φ \land (x \in A \land D \leq x)) \to B = C$
Assertion	lo1eq	$⊢ φ \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in \leq 𝑂 (1))$

Proof

Step	Hyp	Ref	Expression
1		lo1eq.1	$⊢ (φ \land x \in A) \to B \in ℝ$
2		lo1eq.2	$⊢ (φ \land x \in A) \to C \in ℝ$
3		lo1eq.3	$⊢ φ \to D \in ℝ$
4		lo1eq.4	$⊢ (φ \land (x \in A \land D \leq x)) \to B = C$
5		lo1dm	$⊢ (x \in A ⟼ B) \in \leq 𝑂 (1) \to dom (x \in A ⟼ B) \subseteq ℝ$
6		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
7	6 1	dmmptd	$⊢ φ \to dom (x \in A ⟼ B) = A$
8	7	sseq1d	$⊢ φ \to (dom (x \in A ⟼ B) \subseteq ℝ \leftrightarrow A \subseteq ℝ)$
9	5 8	imbitrid	$⊢ φ \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \to A \subseteq ℝ)$
10		lo1dm	$⊢ (x \in A ⟼ C) \in \leq 𝑂 (1) \to dom (x \in A ⟼ C) \subseteq ℝ$
11		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
12	11 2	dmmptd	$⊢ φ \to dom (x \in A ⟼ C) = A$
13	12	sseq1d	$⊢ φ \to (dom (x \in A ⟼ C) \subseteq ℝ \leftrightarrow A \subseteq ℝ)$
14	10 13	imbitrid	$⊢ φ \to ((x \in A ⟼ C) \in \leq 𝑂 (1) \to A \subseteq ℝ)$
15		elin	$⊢ x \in (A \cap [D, +∞)) \leftrightarrow (x \in A \land x \in [D, +∞))$
16	15	bilani	$⊢ (φ \land x \in (A \cap [D, +∞))) \to (x \in A \land x \in [D, +∞))$
17	16	simpld	$⊢ (φ \land x \in (A \cap [D, +∞))) \to x \in A$
18	16	simprd	$⊢ (φ \land x \in (A \cap [D, +∞))) \to x \in [D, +∞)$
19		elicopnf	$⊢ D \in ℝ \to (x \in [D, +∞) \leftrightarrow (x \in ℝ \land D \leq x))$
20	3 19	syl	$⊢ φ \to (x \in [D, +∞) \leftrightarrow (x \in ℝ \land D \leq x))$
21	20	biimpa	$⊢ (φ \land x \in [D, +∞)) \to (x \in ℝ \land D \leq x)$
22	18 21	syldan	$⊢ (φ \land x \in (A \cap [D, +∞))) \to (x \in ℝ \land D \leq x)$
23	22	simprd	$⊢ (φ \land x \in (A \cap [D, +∞))) \to D \leq x$
24	17 23	jca	$⊢ (φ \land x \in (A \cap [D, +∞))) \to (x \in A \land D \leq x)$
25	24 4	syldan	$⊢ (φ \land x \in (A \cap [D, +∞))) \to B = C$
26	25	mpteq2dva	$⊢ φ \to (x \in (A \cap [D, +∞)) ⟼ B) = (x \in (A \cap [D, +∞)) ⟼ C)$
27		inss1	$⊢ A \cap [D, +∞) \subseteq A$
28		resmpt	$⊢ A \cap [D, +∞) \subseteq A \to {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ B)$
29	27 28	ax-mp	$⊢ {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ B)$
30		resmpt	$⊢ A \cap [D, +∞) \subseteq A \to {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ C)$
31	27 30	ax-mp	$⊢ {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))} = (x \in (A \cap [D, +∞)) ⟼ C)$
32	26 29 31	3eqtr4g	$⊢ φ \to {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))} = {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))}$
33		resres	$⊢ {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ B) ↾}_{(A \cap [D, +∞))}$
34		resres	$⊢ {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{(A \cap [D, +∞))}$
35	32 33 34	3eqtr4g	$⊢ φ \to {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)}$
36		ssid	$⊢ A \subseteq A$
37		resmpt	$⊢ A \subseteq A \to {(x \in A ⟼ B) ↾}_{A} = (x \in A ⟼ B)$
38		reseq1	$⊢ {(x \in A ⟼ B) ↾}_{A} = (x \in A ⟼ B) \to {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ B) ↾}_{[D, +∞)}$
39	36 37 38	mp2b	$⊢ {({(x \in A ⟼ B) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ B) ↾}_{[D, +∞)}$
40		resmpt	$⊢ A \subseteq A \to {(x \in A ⟼ C) ↾}_{A} = (x \in A ⟼ C)$
41		reseq1	$⊢ {(x \in A ⟼ C) ↾}_{A} = (x \in A ⟼ C) \to {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{[D, +∞)}$
42	36 40 41	mp2b	$⊢ {({(x \in A ⟼ C) ↾}_{A}) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{[D, +∞)}$
43	35 39 42	3eqtr3g	$⊢ φ \to {(x \in A ⟼ B) ↾}_{[D, +∞)} = {(x \in A ⟼ C) ↾}_{[D, +∞)}$
44	43	eleq1d	$⊢ φ \to ({(x \in A ⟼ B) ↾}_{[D, +∞)} \in \leq 𝑂 (1) \leftrightarrow {(x \in A ⟼ C) ↾}_{[D, +∞)} \in \leq 𝑂 (1))$
45	44	adantr	$⊢ (φ \land A \subseteq ℝ) \to ({(x \in A ⟼ B) ↾}_{[D, +∞)} \in \leq 𝑂 (1) \leftrightarrow {(x \in A ⟼ C) ↾}_{[D, +∞)} \in \leq 𝑂 (1))$
46	1	fmpttd	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℝ$
47	46	adantr	$⊢ (φ \land A \subseteq ℝ) \to (x \in A ⟼ B) : A ⟶ ℝ$
48		simpr	$⊢ (φ \land A \subseteq ℝ) \to A \subseteq ℝ$
49	3	adantr	$⊢ (φ \land A \subseteq ℝ) \to D \in ℝ$
50	47 48 49	lo1resb	$⊢ (φ \land A \subseteq ℝ) \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \leftrightarrow {(x \in A ⟼ B) ↾}_{[D, +∞)} \in \leq 𝑂 (1))$
51	2	fmpttd	$⊢ φ \to (x \in A ⟼ C) : A ⟶ ℝ$
52	51	adantr	$⊢ (φ \land A \subseteq ℝ) \to (x \in A ⟼ C) : A ⟶ ℝ$
53	52 48 49	lo1resb	$⊢ (φ \land A \subseteq ℝ) \to ((x \in A ⟼ C) \in \leq 𝑂 (1) \leftrightarrow {(x \in A ⟼ C) ↾}_{[D, +∞)} \in \leq 𝑂 (1))$
54	45 50 53	3bitr4d	$⊢ (φ \land A \subseteq ℝ) \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in \leq 𝑂 (1))$
55	54	ex	$⊢ φ \to (A \subseteq ℝ \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in \leq 𝑂 (1)))$
56	9 14 55	pm5.21ndd	$⊢ φ \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \leftrightarrow (x \in A ⟼ C) \in \leq 𝑂 (1))$

Metamath Proof Explorer

Theorem lo1eq

Proof