lo1le

Description: Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	lo1le.1	$⊢ φ \to M \in ℝ$
	lo1le.2	$⊢ φ \to (x \in A ⟼ B) \in \leq 𝑂 (1)$
	lo1le.3	$⊢ (φ \land x \in A) \to B \in V$
	lo1le.4	$⊢ (φ \land x \in A) \to C \in ℝ$
	lo1le.5	$⊢ (φ \land (x \in A \land M \leq x)) \to C \leq B$
Assertion	lo1le	$⊢ φ \to (x \in A ⟼ C) \in \leq 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		lo1le.1	$⊢ φ \to M \in ℝ$
2		lo1le.2	$⊢ φ \to (x \in A ⟼ B) \in \leq 𝑂 (1)$
3		lo1le.3	$⊢ (φ \land x \in A) \to B \in V$
4		lo1le.4	$⊢ (φ \land x \in A) \to C \in ℝ$
5		lo1le.5	$⊢ (φ \land (x \in A \land M \leq x)) \to C \leq B$
6		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
7	1	adantr	$⊢ (φ \land y \in ℝ) \to M \in ℝ$
8	6 7	ifcld	$⊢ (φ \land y \in ℝ) \to if (M \leq y, y, M) \in ℝ$
9	1	ad2antrr	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to M \in ℝ$
10		simplr	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to y \in ℝ$
11	3	ralrimiva	$⊢ φ \to \forall x \in A B \in V$
12		dmmptg	$⊢ \forall x \in A B \in V \to dom (x \in A ⟼ B) = A$
13	11 12	syl	$⊢ φ \to dom (x \in A ⟼ B) = A$
14		lo1dm	$⊢ (x \in A ⟼ B) \in \leq 𝑂 (1) \to dom (x \in A ⟼ B) \subseteq ℝ$
15	2 14	syl	$⊢ φ \to dom (x \in A ⟼ B) \subseteq ℝ$
16	13 15	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
17	16	ad2antrr	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to A \subseteq ℝ$
18		simprr	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to x \in A$
19	17 18	sseldd	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to x \in ℝ$
20		maxle	$⊢ (M \in ℝ \land y \in ℝ \land x \in ℝ) \to (if (M \leq y, y, M) \leq x \leftrightarrow (M \leq x \land y \leq x))$
21	9 10 19 20	syl3anc	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to (if (M \leq y, y, M) \leq x \leftrightarrow (M \leq x \land y \leq x))$
22		simpr	$⊢ (M \leq x \land y \leq x) \to y \leq x$
23	21 22	syl6bi	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to (if (M \leq y, y, M) \leq x \to y \leq x)$
24	23	imim1d	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to ((y \leq x \to B \leq m) \to (if (M \leq y, y, M) \leq x \to B \leq m))$
25	5	adantlr	$⊢ ((φ \land y \in ℝ) \land (x \in A \land M \leq x)) \to C \leq B$
26	25	adantrll	$⊢ ((φ \land y \in ℝ) \land ((m \in ℝ \land x \in A) \land M \leq x)) \to C \leq B$
27		simpl	$⊢ (φ \land y \in ℝ) \to φ$
28		simplr	$⊢ ((m \in ℝ \land x \in A) \land M \leq x) \to x \in A$
29	27 28 4	syl2an	$⊢ ((φ \land y \in ℝ) \land ((m \in ℝ \land x \in A) \land M \leq x)) \to C \in ℝ$
30	3 2	lo1mptrcl	$⊢ (φ \land x \in A) \to B \in ℝ$
31	27 28 30	syl2an	$⊢ ((φ \land y \in ℝ) \land ((m \in ℝ \land x \in A) \land M \leq x)) \to B \in ℝ$
32		simprll	$⊢ ((φ \land y \in ℝ) \land ((m \in ℝ \land x \in A) \land M \leq x)) \to m \in ℝ$
33		letr	$⊢ (C \in ℝ \land B \in ℝ \land m \in ℝ) \to ((C \leq B \land B \leq m) \to C \leq m)$
34	29 31 32 33	syl3anc	$⊢ ((φ \land y \in ℝ) \land ((m \in ℝ \land x \in A) \land M \leq x)) \to ((C \leq B \land B \leq m) \to C \leq m)$
35	26 34	mpand	$⊢ ((φ \land y \in ℝ) \land ((m \in ℝ \land x \in A) \land M \leq x)) \to (B \leq m \to C \leq m)$
36	35	expr	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to (M \leq x \to (B \leq m \to C \leq m))$
37	36	adantrd	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to ((M \leq x \land y \leq x) \to (B \leq m \to C \leq m))$
38	21 37	sylbid	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to (if (M \leq y, y, M) \leq x \to (B \leq m \to C \leq m))$
39	38	a2d	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to ((if (M \leq y, y, M) \leq x \to B \leq m) \to (if (M \leq y, y, M) \leq x \to C \leq m))$
40	24 39	syld	$⊢ ((φ \land y \in ℝ) \land (m \in ℝ \land x \in A)) \to ((y \leq x \to B \leq m) \to (if (M \leq y, y, M) \leq x \to C \leq m))$
41	40	anassrs	$⊢ (((φ \land y \in ℝ) \land m \in ℝ) \land x \in A) \to ((y \leq x \to B \leq m) \to (if (M \leq y, y, M) \leq x \to C \leq m))$
42	41	ralimdva	$⊢ ((φ \land y \in ℝ) \land m \in ℝ) \to (\forall x \in A (y \leq x \to B \leq m) \to \forall x \in A (if (M \leq y, y, M) \leq x \to C \leq m))$
43	42	reximdva	$⊢ (φ \land y \in ℝ) \to (\exists m \in ℝ \forall x \in A (y \leq x \to B \leq m) \to \exists m \in ℝ \forall x \in A (if (M \leq y, y, M) \leq x \to C \leq m))$
44		breq1	$⊢ z = if (M \leq y, y, M) \to (z \leq x \leftrightarrow if (M \leq y, y, M) \leq x)$
45	44	imbi1d	$⊢ z = if (M \leq y, y, M) \to ((z \leq x \to C \leq m) \leftrightarrow (if (M \leq y, y, M) \leq x \to C \leq m))$
46	45	rexralbidv	$⊢ z = if (M \leq y, y, M) \to (\exists m \in ℝ \forall x \in A (z \leq x \to C \leq m) \leftrightarrow \exists m \in ℝ \forall x \in A (if (M \leq y, y, M) \leq x \to C \leq m))$
47	46	rspcev	$⊢ (if (M \leq y, y, M) \in ℝ \land \exists m \in ℝ \forall x \in A (if (M \leq y, y, M) \leq x \to C \leq m)) \to \exists z \in ℝ \exists m \in ℝ \forall x \in A (z \leq x \to C \leq m)$
48	8 43 47	syl6an	$⊢ (φ \land y \in ℝ) \to (\exists m \in ℝ \forall x \in A (y \leq x \to B \leq m) \to \exists z \in ℝ \exists m \in ℝ \forall x \in A (z \leq x \to C \leq m))$
49	48	rexlimdva	$⊢ φ \to (\exists y \in ℝ \exists m \in ℝ \forall x \in A (y \leq x \to B \leq m) \to \exists z \in ℝ \exists m \in ℝ \forall x \in A (z \leq x \to C \leq m))$
50	16 30	ello1mpt	$⊢ φ \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \leftrightarrow \exists y \in ℝ \exists m \in ℝ \forall x \in A (y \leq x \to B \leq m))$
51	16 4	ello1mpt	$⊢ φ \to ((x \in A ⟼ C) \in \leq 𝑂 (1) \leftrightarrow \exists z \in ℝ \exists m \in ℝ \forall x \in A (z \leq x \to C \leq m))$
52	49 50 51	3imtr4d	$⊢ φ \to ((x \in A ⟼ B) \in \leq 𝑂 (1) \to (x \in A ⟼ C) \in \leq 𝑂 (1))$
53	2 52	mpd	$⊢ φ \to (x \in A ⟼ C) \in \leq 𝑂 (1)$

Metamath Proof Explorer

Theorem lo1le

Proof