evth

Description: The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Hypotheses	bndth.1	$⊢ X = ⋃ J$
	bndth.2	$⊢ K = topGen (ran (.))$
	bndth.3	$⊢ φ \to J \in Comp$
	bndth.4	$⊢ φ \to F \in (J Cn K)$
	evth.5	$⊢ φ \to X \neq \emptyset$
Assertion	evth	$⊢ φ \to \exists x \in X \forall y \in X F (y) \leq F (x)$

Proof

Step	Hyp	Ref	Expression
1		bndth.1	$⊢ X = ⋃ J$
2		bndth.2	$⊢ K = topGen (ran (.))$
3		bndth.3	$⊢ φ \to J \in Comp$
4		bndth.4	$⊢ φ \to F \in (J Cn K)$
5		evth.5	$⊢ φ \to X \neq \emptyset$
6	3	adantr	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to J \in Comp$
7		cmptop	$⊢ J \in Comp \to J \in Top$
8	6 7	syl	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to J \in Top$
9	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
10	8 9	sylib	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to J \in TopOn (X)$
11		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
12	11	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
13	12	a1i	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
14		1cnd	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to 1 \in ℂ$
15	10 13 14	cnmptc	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ 1) \in (J Cn TopOpen (ℂ_{fld}))$
16		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
17	2	unieqi	$⊢ ⋃ K = ⋃ topGen (ran (.))$
18	16 17	eqtr4i	$⊢ ℝ = ⋃ K$
19	1 18	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ ℝ$
20	4 19	syl	$⊢ φ \to F : X ⟶ ℝ$
21	20	frnd	$⊢ φ \to ran F \subseteq ℝ$
22	20	fdmd	$⊢ φ \to dom F = X$
23	22 5	eqnetrd	$⊢ φ \to dom F \neq \emptyset$
24		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
25	24	necon3bii	$⊢ dom F \neq \emptyset \leftrightarrow ran F \neq \emptyset$
26	23 25	sylib	$⊢ φ \to ran F \neq \emptyset$
27	1 2 3 4	bndth	$⊢ φ \to \exists x \in ℝ \forall y \in X F (y) \leq x$
28	20	ffnd	$⊢ φ \to F Fn X$
29		breq1	$⊢ z = F (y) \to (z \leq x \leftrightarrow F (y) \leq x)$
30	29	ralrn	$⊢ F Fn X \to (\forall z \in ran F z \leq x \leftrightarrow \forall y \in X F (y) \leq x)$
31	28 30	syl	$⊢ φ \to (\forall z \in ran F z \leq x \leftrightarrow \forall y \in X F (y) \leq x)$
32	31	rexbidv	$⊢ φ \to (\exists x \in ℝ \forall z \in ran F z \leq x \leftrightarrow \exists x \in ℝ \forall y \in X F (y) \leq x)$
33	27 32	mpbird	$⊢ φ \to \exists x \in ℝ \forall z \in ran F z \leq x$
34	21 26 33	3jca	$⊢ φ \to (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall z \in ran F z \leq x)$
35		suprcl	$⊢ (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall z \in ran F z \leq x) \to sup (ran F ℝ <) \in ℝ$
36	34 35	syl	$⊢ φ \to sup (ran F ℝ <) \in ℝ$
37	36	recnd	$⊢ φ \to sup (ran F ℝ <) \in ℂ$
38	37	adantr	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to sup (ran F ℝ <) \in ℂ$
39	10 13 38	cnmptc	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ sup (ran F ℝ <)) \in (J Cn TopOpen (ℂ_{fld}))$
40	20	feqmptd	$⊢ φ \to F = (z \in X ⟼ F (z))$
41	11	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
42		cnrest2r	$⊢ TopOpen (ℂ_{fld}) \in Top \to J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) \subseteq J Cn TopOpen (ℂ_{fld})$
43	41 42	ax-mp	$⊢ J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) \subseteq J Cn TopOpen (ℂ_{fld})$
44	11	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
45	2 44	eqtri	$⊢ K = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
46	45	oveq2i	$⊢ J Cn K = J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
47	4 46	eleqtrdi	$⊢ φ \to F \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
48	43 47	sselid	$⊢ φ \to F \in (J Cn TopOpen (ℂ_{fld}))$
49	40 48	eqeltrrd	$⊢ φ \to (z \in X ⟼ F (z)) \in (J Cn TopOpen (ℂ_{fld}))$
50	49	adantr	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ F (z)) \in (J Cn TopOpen (ℂ_{fld}))$
51	11	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
52	51	a1i	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
53	10 39 50 52	cnmpt12f	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ sup (ran F ℝ <) - F (z)) \in (J Cn TopOpen (ℂ_{fld}))$
54	36	ad2antrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to sup (ran F ℝ <) \in ℝ$
55		ffvelcdm	$⊢ (F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\} \land z \in X) \to F (z) \in (ℝ ∖ \{sup (ran F ℝ <)\})$
56	55	adantll	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to F (z) \in (ℝ ∖ \{sup (ran F ℝ <)\})$
57		eldifsn	$⊢ F (z) \in (ℝ ∖ \{sup (ran F ℝ <)\}) \leftrightarrow (F (z) \in ℝ \land F (z) \neq sup (ran F ℝ <))$
58	56 57	sylib	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to (F (z) \in ℝ \land F (z) \neq sup (ran F ℝ <))$
59	58	simpld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to F (z) \in ℝ$
60	54 59	resubcld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to sup (ran F ℝ <) - F (z) \in ℝ$
61	60	recnd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to sup (ran F ℝ <) - F (z) \in ℂ$
62	54	recnd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to sup (ran F ℝ <) \in ℂ$
63	59	recnd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to F (z) \in ℂ$
64	58	simprd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to F (z) \neq sup (ran F ℝ <)$
65	64	necomd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to sup (ran F ℝ <) \neq F (z)$
66	62 63 65	subne0d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to sup (ran F ℝ <) - F (z) \neq 0$
67		eldifsn	$⊢ sup (ran F ℝ <) - F (z) \in (ℂ ∖ \{0\}) \leftrightarrow (sup (ran F ℝ <) - F (z) \in ℂ \land sup (ran F ℝ <) - F (z) \neq 0)$
68	61 66 67	sylanbrc	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to sup (ran F ℝ <) - F (z) \in (ℂ ∖ \{0\})$
69	68	fmpttd	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ sup (ran F ℝ <) - F (z)) : X ⟶ ℂ ∖ \{0\}$
70	69	frnd	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to ran (z \in X ⟼ sup (ran F ℝ <) - F (z)) \subseteq ℂ ∖ \{0\}$
71		difssd	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to ℂ ∖ \{0\} \subseteq ℂ$
72		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (z \in X ⟼ sup (ran F ℝ <) - F (z)) \subseteq ℂ ∖ \{0\} \land ℂ ∖ \{0\} \subseteq ℂ) \to ((z \in X ⟼ sup (ran F ℝ <) - F (z)) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (z \in X ⟼ sup (ran F ℝ <) - F (z)) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ \{0\}))))$
73	13 70 71 72	syl3anc	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to ((z \in X ⟼ sup (ran F ℝ <) - F (z)) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (z \in X ⟼ sup (ran F ℝ <) - F (z)) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ \{0\}))))$
74	53 73	mpbid	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ sup (ran F ℝ <) - F (z)) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ \{0\})))$
75		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ \{0\})$
76	11 75	divcn	$⊢ \div \in ((TopOpen (ℂ_{fld}) \times_{t} (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ \{0\}))) Cn TopOpen (ℂ_{fld}))$
77	76	a1i	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to \div \in ((TopOpen (ℂ_{fld}) \times_{t} (TopOpen (ℂ_{fld}) ↾_{𝑡} (ℂ ∖ \{0\}))) Cn TopOpen (ℂ_{fld}))$
78	10 15 74 77	cnmpt12f	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \in (J Cn TopOpen (ℂ_{fld}))$
79	60 66	rereccld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land z \in X) \to \frac{1}{sup (ran F ℝ <) - F (z)} \in ℝ$
80	79	fmpttd	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) : X ⟶ ℝ$
81	80	frnd	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to ran (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \subseteq ℝ$
82		ax-resscn	$⊢ ℝ \subseteq ℂ$
83	82	a1i	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to ℝ \subseteq ℂ$
84		cnrest2	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ran (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \subseteq ℝ \land ℝ \subseteq ℂ) \to ((z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
85	13 81 83 84	syl3anc	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to ((z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \in (J Cn TopOpen (ℂ_{fld})) \leftrightarrow (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)))$
86	78 85	mpbid	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \in (J Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ))$
87	86 46	eleqtrrdi	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) \in (J Cn K)$
88	1 2 6 87	bndth	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to \exists x \in ℝ \forall y \in X (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x$
89	36	ad2antrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to sup (ran F ℝ <) \in ℝ$
90		simpr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to x \in ℝ$
91		1re	$⊢ 1 \in ℝ$
92		ifcl	$⊢ (x \in ℝ \land 1 \in ℝ) \to if (1 \leq x, x, 1) \in ℝ$
93	90 91 92	sylancl	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to if (1 \leq x, x, 1) \in ℝ$
94		0red	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to 0 \in ℝ$
95	91	a1i	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to 1 \in ℝ$
96		0lt1	$⊢ 0 < 1$
97	96	a1i	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to 0 < 1$
98		max1	$⊢ (1 \in ℝ \land x \in ℝ) \to 1 \leq if (1 \leq x, x, 1)$
99	91 90 98	sylancr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to 1 \leq if (1 \leq x, x, 1)$
100	94 95 93 97 99	ltletrd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to 0 < if (1 \leq x, x, 1)$
101	100	gt0ne0d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to if (1 \leq x, x, 1) \neq 0$
102	93 101	rereccld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to \frac{1}{if (1 \leq x, x, 1)} \in ℝ$
103	93 100	recgt0d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to 0 < \frac{1}{if (1 \leq x, x, 1)}$
104	102 103	elrpd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to \frac{1}{if (1 \leq x, x, 1)} \in ℝ^{+}$
105	89 104	ltsubrpd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) < sup (ran F ℝ <)$
106	89 102	resubcld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \in ℝ$
107	106 89	ltnled	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to (sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) < sup (ran F ℝ <) \leftrightarrow \neg sup (ran F ℝ <) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
108	105 107	mpbid	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to \neg sup (ran F ℝ <) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)})$
109		simprl	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to x \in ℝ$
110		max2	$⊢ (1 \in ℝ \land x \in ℝ) \to x \leq if (1 \leq x, x, 1)$
111	91 109 110	sylancr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to x \leq if (1 \leq x, x, 1)$
112	36	ad2antrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to sup (ran F ℝ <) \in ℝ$
113		ffvelcdm	$⊢ (F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\} \land y \in X) \to F (y) \in (ℝ ∖ \{sup (ran F ℝ <)\})$
114	113	ad2ant2l	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to F (y) \in (ℝ ∖ \{sup (ran F ℝ <)\})$
115		eldifsn	$⊢ F (y) \in (ℝ ∖ \{sup (ran F ℝ <)\}) \leftrightarrow (F (y) \in ℝ \land F (y) \neq sup (ran F ℝ <))$
116	114 115	sylib	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to (F (y) \in ℝ \land F (y) \neq sup (ran F ℝ <))$
117	116	simpld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to F (y) \in ℝ$
118	112 117	resubcld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to sup (ran F ℝ <) - F (y) \in ℝ$
119		fnfvelrn	$⊢ (F Fn X \land y \in X) \to F (y) \in ran F$
120	28 119	sylan	$⊢ (φ \land y \in X) \to F (y) \in ran F$
121		suprub	$⊢ ((ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall z \in ran F z \leq x) \land F (y) \in ran F) \to F (y) \leq sup (ran F ℝ <)$
122	34 120 121	syl2an2r	$⊢ (φ \land y \in X) \to F (y) \leq sup (ran F ℝ <)$
123	122	ad2ant2rl	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to F (y) \leq sup (ran F ℝ <)$
124	116	simprd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to F (y) \neq sup (ran F ℝ <)$
125	124	necomd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to sup (ran F ℝ <) \neq F (y)$
126	117 112 123 125	leneltd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to F (y) < sup (ran F ℝ <)$
127	117 112	posdifd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to (F (y) < sup (ran F ℝ <) \leftrightarrow 0 < sup (ran F ℝ <) - F (y))$
128	126 127	mpbid	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to 0 < sup (ran F ℝ <) - F (y)$
129	128	gt0ne0d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to sup (ran F ℝ <) - F (y) \neq 0$
130	118 129	rereccld	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to \frac{1}{sup (ran F ℝ <) - F (y)} \in ℝ$
131	109 91 92	sylancl	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to if (1 \leq x, x, 1) \in ℝ$
132		letr	$⊢ (\frac{1}{sup (ran F ℝ <) - F (y)} \in ℝ \land x \in ℝ \land if (1 \leq x, x, 1) \in ℝ) \to ((\frac{1}{sup (ran F ℝ <) - F (y)} \leq x \land x \leq if (1 \leq x, x, 1)) \to \frac{1}{sup (ran F ℝ <) - F (y)} \leq if (1 \leq x, x, 1))$
133	130 109 131 132	syl3anc	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to ((\frac{1}{sup (ran F ℝ <) - F (y)} \leq x \land x \leq if (1 \leq x, x, 1)) \to \frac{1}{sup (ran F ℝ <) - F (y)} \leq if (1 \leq x, x, 1))$
134	111 133	mpan2d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to (\frac{1}{sup (ran F ℝ <) - F (y)} \leq x \to \frac{1}{sup (ran F ℝ <) - F (y)} \leq if (1 \leq x, x, 1))$
135		fveq2	$⊢ z = y \to F (z) = F (y)$
136	135	oveq2d	$⊢ z = y \to sup (ran F ℝ <) - F (z) = sup (ran F ℝ <) - F (y)$
137	136	oveq2d	$⊢ z = y \to \frac{1}{sup (ran F ℝ <) - F (z)} = \frac{1}{sup (ran F ℝ <) - F (y)}$
138		eqid	$⊢ (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) = (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)})$
139		ovex	$⊢ \frac{1}{sup (ran F ℝ <) - F (y)} \in V$
140	137 138 139	fvmpt	$⊢ y \in X \to (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) = \frac{1}{sup (ran F ℝ <) - F (y)}$
141	140	breq1d	$⊢ y \in X \to ((z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x \leftrightarrow \frac{1}{sup (ran F ℝ <) - F (y)} \leq x)$
142	141	ad2antll	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to ((z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x \leftrightarrow \frac{1}{sup (ran F ℝ <) - F (y)} \leq x)$
143	102	adantrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to \frac{1}{if (1 \leq x, x, 1)} \in ℝ$
144	100	adantrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to 0 < if (1 \leq x, x, 1)$
145	131 144	recgt0d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to 0 < \frac{1}{if (1 \leq x, x, 1)}$
146		lerec	$⊢ ((\frac{1}{if (1 \leq x, x, 1)} \in ℝ \land 0 < \frac{1}{if (1 \leq x, x, 1)}) \land (sup (ran F ℝ <) - F (y) \in ℝ \land 0 < sup (ran F ℝ <) - F (y))) \to (\frac{1}{if (1 \leq x, x, 1)} \leq sup (ran F ℝ <) - F (y) \leftrightarrow \frac{1}{sup (ran F ℝ <) - F (y)} \leq \frac{1}{\frac{1}{if (1 \leq x, x, 1)}})$
147	143 145 118 128 146	syl22anc	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to (\frac{1}{if (1 \leq x, x, 1)} \leq sup (ran F ℝ <) - F (y) \leftrightarrow \frac{1}{sup (ran F ℝ <) - F (y)} \leq \frac{1}{\frac{1}{if (1 \leq x, x, 1)}})$
148		lesub	$⊢ (\frac{1}{if (1 \leq x, x, 1)} \in ℝ \land sup (ran F ℝ <) \in ℝ \land F (y) \in ℝ) \to (\frac{1}{if (1 \leq x, x, 1)} \leq sup (ran F ℝ <) - F (y) \leftrightarrow F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
149	143 112 117 148	syl3anc	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to (\frac{1}{if (1 \leq x, x, 1)} \leq sup (ran F ℝ <) - F (y) \leftrightarrow F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
150	131	recnd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to if (1 \leq x, x, 1) \in ℂ$
151	101	adantrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to if (1 \leq x, x, 1) \neq 0$
152	150 151	recrecd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to \frac{1}{\frac{1}{if (1 \leq x, x, 1)}} = if (1 \leq x, x, 1)$
153	152	breq2d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to (\frac{1}{sup (ran F ℝ <) - F (y)} \leq \frac{1}{\frac{1}{if (1 \leq x, x, 1)}} \leftrightarrow \frac{1}{sup (ran F ℝ <) - F (y)} \leq if (1 \leq x, x, 1))$
154	147 149 153	3bitr3d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to (F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \leftrightarrow \frac{1}{sup (ran F ℝ <) - F (y)} \leq if (1 \leq x, x, 1))$
155	134 142 154	3imtr4d	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land (x \in ℝ \land y \in X)) \to ((z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x \to F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
156	155	anassrs	$⊢ (((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \land y \in X) \to ((z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x \to F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
157	156	ralimdva	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to (\forall y \in X (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x \to \forall y \in X F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
158	34	ad2antrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall z \in ran F z \leq x)$
159		suprleub	$⊢ ((ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall z \in ran F z \leq x) \land sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \in ℝ) \to (sup (ran F ℝ <) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \leftrightarrow \forall z \in ran F z \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
160	158 106 159	syl2anc	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to (sup (ran F ℝ <) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \leftrightarrow \forall z \in ran F z \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
161	28	ad2antrr	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to F Fn X$
162		breq1	$⊢ z = F (y) \to (z \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \leftrightarrow F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
163	162	ralrn	$⊢ F Fn X \to (\forall z \in ran F z \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \leftrightarrow \forall y \in X F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
164	161 163	syl	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to (\forall z \in ran F z \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \leftrightarrow \forall y \in X F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
165	160 164	bitrd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to (sup (ran F ℝ <) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}) \leftrightarrow \forall y \in X F (y) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
166	157 165	sylibrd	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to (\forall y \in X (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x \to sup (ran F ℝ <) \leq sup (ran F ℝ <) - (\frac{1}{if (1 \leq x, x, 1)}))$
167	108 166	mtod	$⊢ ((φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \land x \in ℝ) \to \neg \forall y \in X (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x$
168	167	nrexdv	$⊢ (φ \land F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}) \to \neg \exists x \in ℝ \forall y \in X (z \in X ⟼ \frac{1}{sup (ran F ℝ <) - F (z)}) (y) \leq x$
169	88 168	pm2.65da	$⊢ φ \to \neg F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\}$
170	122	ralrimiva	$⊢ φ \to \forall y \in X F (y) \leq sup (ran F ℝ <)$
171		breq2	$⊢ F (x) = sup (ran F ℝ <) \to (F (y) \leq F (x) \leftrightarrow F (y) \leq sup (ran F ℝ <))$
172	171	ralbidv	$⊢ F (x) = sup (ran F ℝ <) \to (\forall y \in X F (y) \leq F (x) \leftrightarrow \forall y \in X F (y) \leq sup (ran F ℝ <))$
173	170 172	syl5ibrcom	$⊢ φ \to (F (x) = sup (ran F ℝ <) \to \forall y \in X F (y) \leq F (x))$
174	173	necon3bd	$⊢ φ \to (\neg \forall y \in X F (y) \leq F (x) \to F (x) \neq sup (ran F ℝ <))$
175	174	adantr	$⊢ (φ \land x \in X) \to (\neg \forall y \in X F (y) \leq F (x) \to F (x) \neq sup (ran F ℝ <))$
176	20	ffvelcdmda	$⊢ (φ \land x \in X) \to F (x) \in ℝ$
177		eldifsn	$⊢ F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}) \leftrightarrow (F (x) \in ℝ \land F (x) \neq sup (ran F ℝ <))$
178	177	baib	$⊢ F (x) \in ℝ \to (F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}) \leftrightarrow F (x) \neq sup (ran F ℝ <))$
179	176 178	syl	$⊢ (φ \land x \in X) \to (F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}) \leftrightarrow F (x) \neq sup (ran F ℝ <))$
180	175 179	sylibrd	$⊢ (φ \land x \in X) \to (\neg \forall y \in X F (y) \leq F (x) \to F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}))$
181	180	ralimdva	$⊢ φ \to (\forall x \in X \neg \forall y \in X F (y) \leq F (x) \to \forall x \in X F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}))$
182		ffnfv	$⊢ F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\} \leftrightarrow (F Fn X \land \forall x \in X F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}))$
183	182	baib	$⊢ F Fn X \to (F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\} \leftrightarrow \forall x \in X F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}))$
184	28 183	syl	$⊢ φ \to (F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\} \leftrightarrow \forall x \in X F (x) \in (ℝ ∖ \{sup (ran F ℝ <)\}))$
185	181 184	sylibrd	$⊢ φ \to (\forall x \in X \neg \forall y \in X F (y) \leq F (x) \to F : X ⟶ ℝ ∖ \{sup (ran F ℝ <)\})$
186	169 185	mtod	$⊢ φ \to \neg \forall x \in X \neg \forall y \in X F (y) \leq F (x)$
187		dfrex2	$⊢ \exists x \in X \forall y \in X F (y) \leq F (x) \leftrightarrow \neg \forall x \in X \neg \forall y \in X F (y) \leq F (x)$
188	186 187	sylibr	$⊢ φ \to \exists x \in X \forall y \in X F (y) \leq F (x)$

Metamath Proof Explorer

Theorem evth

Proof