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

Metamath Proof Explorer

Theorem lo1eq

Proof