suprnmpt

Description: An explicit bound for the range of a bounded function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	suprnmpt.a	$⊢ φ \to A \neq \emptyset$
	suprnmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ$
	suprnmpt.bnd	$⊢ φ \to \exists y \in ℝ \forall x \in A B \leq y$
	suprnmpt.f	$⊢ F = (x \in A ⟼ B)$
	suprnmpt.c	$⊢ C = sup (ran F ℝ <)$
Assertion	suprnmpt	$⊢ φ \to (C \in ℝ \land \forall x \in A B \leq C)$

Proof

Step	Hyp	Ref	Expression
1		suprnmpt.a	$⊢ φ \to A \neq \emptyset$
2		suprnmpt.b	$⊢ (φ \land x \in A) \to B \in ℝ$
3		suprnmpt.bnd	$⊢ φ \to \exists y \in ℝ \forall x \in A B \leq y$
4		suprnmpt.f	$⊢ F = (x \in A ⟼ B)$
5		suprnmpt.c	$⊢ C = sup (ran F ℝ <)$
6	2	ralrimiva	$⊢ φ \to \forall x \in A B \in ℝ$
7	4	rnmptss	$⊢ \forall x \in A B \in ℝ \to ran F \subseteq ℝ$
8	6 7	syl	$⊢ φ \to ran F \subseteq ℝ$
9		nfv	$⊢ Ⅎ x φ$
10	9 2 4 1	rnmptn0	$⊢ φ \to ran F \neq \emptyset$
11		nfv	$⊢ Ⅎ y φ$
12		nfre1	$⊢ Ⅎ y \exists y \in ℝ \forall z \in ran F z \leq y$
13		simp2	$⊢ (φ \land y \in ℝ \land \forall x \in A B \leq y) \to y \in ℝ$
14		simpl1	$⊢ ((φ \land y \in ℝ \land \forall x \in A B \leq y) \land z \in ran F) \to φ$
15		simpl3	$⊢ ((φ \land y \in ℝ \land \forall x \in A B \leq y) \land z \in ran F) \to \forall x \in A B \leq y$
16		vex	$⊢ z \in V$
17	4	elrnmpt	$⊢ z \in V \to (z \in ran F \leftrightarrow \exists x \in A z = B)$
18	16 17	ax-mp	$⊢ z \in ran F \leftrightarrow \exists x \in A z = B$
19	18	biimpi	$⊢ z \in ran F \to \exists x \in A z = B$
20	19	adantl	$⊢ ((φ \land y \in ℝ \land \forall x \in A B \leq y) \land z \in ran F) \to \exists x \in A z = B$
21		simp3	$⊢ (φ \land \forall x \in A B \leq y \land \exists x \in A z = B) \to \exists x \in A z = B$
22		nfra1	$⊢ Ⅎ x \forall x \in A B \leq y$
23		nfre1	$⊢ Ⅎ x \exists x \in A z = B$
24	9 22 23	nf3an	$⊢ Ⅎ x (φ \land \forall x \in A B \leq y \land \exists x \in A z = B)$
25		nfv	$⊢ Ⅎ x z \leq y$
26		simp3	$⊢ (\forall x \in A B \leq y \land x \in A \land z = B) \to z = B$
27		rspa	$⊢ (\forall x \in A B \leq y \land x \in A) \to B \leq y$
28	27	3adant3	$⊢ (\forall x \in A B \leq y \land x \in A \land z = B) \to B \leq y$
29	26 28	eqbrtrd	$⊢ (\forall x \in A B \leq y \land x \in A \land z = B) \to z \leq y$
30	29	3exp	$⊢ \forall x \in A B \leq y \to (x \in A \to (z = B \to z \leq y))$
31	30	3ad2ant2	$⊢ (φ \land \forall x \in A B \leq y \land \exists x \in A z = B) \to (x \in A \to (z = B \to z \leq y))$
32	24 25 31	rexlimd	$⊢ (φ \land \forall x \in A B \leq y \land \exists x \in A z = B) \to (\exists x \in A z = B \to z \leq y)$
33	21 32	mpd	$⊢ (φ \land \forall x \in A B \leq y \land \exists x \in A z = B) \to z \leq y$
34	14 15 20 33	syl3anc	$⊢ ((φ \land y \in ℝ \land \forall x \in A B \leq y) \land z \in ran F) \to z \leq y$
35	34	ralrimiva	$⊢ (φ \land y \in ℝ \land \forall x \in A B \leq y) \to \forall z \in ran F z \leq y$
36		19.8a	$⊢ (y \in ℝ \land \forall z \in ran F z \leq y) \to \exists y (y \in ℝ \land \forall z \in ran F z \leq y)$
37	13 35 36	syl2anc	$⊢ (φ \land y \in ℝ \land \forall x \in A B \leq y) \to \exists y (y \in ℝ \land \forall z \in ran F z \leq y)$
38		df-rex	$⊢ \exists y \in ℝ \forall z \in ran F z \leq y \leftrightarrow \exists y (y \in ℝ \land \forall z \in ran F z \leq y)$
39	37 38	sylibr	$⊢ (φ \land y \in ℝ \land \forall x \in A B \leq y) \to \exists y \in ℝ \forall z \in ran F z \leq y$
40	39	3exp	$⊢ φ \to (y \in ℝ \to (\forall x \in A B \leq y \to \exists y \in ℝ \forall z \in ran F z \leq y))$
41	11 12 40	rexlimd	$⊢ φ \to (\exists y \in ℝ \forall x \in A B \leq y \to \exists y \in ℝ \forall z \in ran F z \leq y)$
42	3 41	mpd	$⊢ φ \to \exists y \in ℝ \forall z \in ran F z \leq y$
43		suprcl	$⊢ (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists y \in ℝ \forall z \in ran F z \leq y) \to sup (ran F ℝ <) \in ℝ$
44	8 10 42 43	syl3anc	$⊢ φ \to sup (ran F ℝ <) \in ℝ$
45	5 44	eqeltrid	$⊢ φ \to C \in ℝ$
46	8	adantr	$⊢ (φ \land x \in A) \to ran F \subseteq ℝ$
47		simpr	$⊢ (φ \land x \in A) \to x \in A$
48	4	elrnmpt1	$⊢ (x \in A \land B \in ℝ) \to B \in ran F$
49	47 2 48	syl2anc	$⊢ (φ \land x \in A) \to B \in ran F$
50	49	ne0d	$⊢ (φ \land x \in A) \to ran F \neq \emptyset$
51	42	adantr	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall z \in ran F z \leq y$
52		suprub	$⊢ ((ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists y \in ℝ \forall z \in ran F z \leq y) \land B \in ran F) \to B \leq sup (ran F ℝ <)$
53	46 50 51 49 52	syl31anc	$⊢ (φ \land x \in A) \to B \leq sup (ran F ℝ <)$
54	53 5	breqtrrdi	$⊢ (φ \land x \in A) \to B \leq C$
55	54	ralrimiva	$⊢ φ \to \forall x \in A B \leq C$
56	45 55	jca	$⊢ φ \to (C \in ℝ \land \forall x \in A B \leq C)$

Metamath Proof Explorer

Theorem suprnmpt

Proof