Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	lo1le.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
	lo1le.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	lo1le.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
	lo1le.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐵 )
Assertion	lo1le	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		lo1le.1	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
2		lo1le.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) )
3		lo1le.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4		lo1le.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
5		lo1le.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐵 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑀 ∈ ℝ )
8	6 7	ifcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ∈ ℝ )
9	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑀 ∈ ℝ )
10		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ )
11	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
12		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
13	11 12	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
14		lo1dm	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
15	2 14	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
16	13 15	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
17	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝐴 ⊆ ℝ )
18		simprr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
19	17 18	sseldd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ ℝ )
20		maxle	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ↔ ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) ) )
21	9 10 19 20	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ↔ ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) ) )
22		simpr	⊢ ( ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) → 𝑦 ≤ 𝑥 )
23	21 22	syl6bi	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝑦 ≤ 𝑥 ) )
24	23	imim1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
25	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐵 )
26	25	adantrll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ≤ 𝐵 )
27		simpl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝜑 )
28		simplr	⊢ ( ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) → 𝑥 ∈ 𝐴 )
29	27 28 4	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝐶 ∈ ℝ )
30	3 2	lo1mptrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
31	27 28 30	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝐵 ∈ ℝ )
32		simprll	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → 𝑚 ∈ ℝ )
33		letr	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝑚 ) → 𝐶 ≤ 𝑚 ) )
34	29 31 32 33	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → ( ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝑚 ) → 𝐶 ≤ 𝑚 ) )
35	26 34	mpand	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑀 ≤ 𝑥 ) ) → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) )
36	35	expr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑀 ≤ 𝑥 → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) ) )
37	36	adantrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑀 ≤ 𝑥 ∧ 𝑦 ≤ 𝑥 ) → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) ) )
38	21 37	sylbid	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → ( 𝐵 ≤ 𝑚 → 𝐶 ≤ 𝑚 ) ) )
39	38	a2d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
40	24 39	syld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
41	40	anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
42	41	ralimdva	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
43	42	reximdva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
44		breq1	⊢ ( 𝑧 = if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) → ( 𝑧 ≤ 𝑥 ↔ if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 ) )
45	44	imbi1d	⊢ ( 𝑧 = if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) → ( ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ↔ ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
46	45	rexralbidv	⊢ ( 𝑧 = if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ↔ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
47	46	rspcev	⊢ ( ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ∈ ℝ ∧ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( if ( 𝑀 ≤ 𝑦 , 𝑦 , 𝑀 ) ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) )
48	8 43 47	syl6an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
49	48	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
50	16 30	ello1mpt	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → 𝐵 ≤ 𝑚 ) ) )
51	16 4	ello1mpt	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ↔ ∃ 𝑧 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ≤ 𝑥 → 𝐶 ≤ 𝑚 ) ) )
52	49 50 51	3imtr4d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ≤𝑂(1) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) ) )
53	2 52	mpd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ ≤𝑂(1) )