bndth

Description: The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -u F .) (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)$
Assertion	bndth	$⊢ φ \to \exists x \in ℝ \forall y \in X F (y) \leq 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		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
6	2 5	eqeltri	$⊢ K \in TopOn (ℝ)$
7	6	toponunii	$⊢ ℝ = ⋃ K$
8	1 7	cnf	$⊢ F \in (J Cn K) \to F : X ⟶ ℝ$
9	4 8	syl	$⊢ φ \to F : X ⟶ ℝ$
10	9	frnd	$⊢ φ \to ran F \subseteq ℝ$
11		unieq	$⊢ u = (.) [\{−∞\} \times ℝ] \to ⋃ u = ⋃ (.) [\{−∞\} \times ℝ]$
12		imassrn	$⊢ (.) [\{−∞\} \times ℝ] \subseteq ran (.)$
13	12	unissi	$⊢ ⋃ (.) [\{−∞\} \times ℝ] \subseteq ⋃ ran (.)$
14		unirnioo	$⊢ ℝ = ⋃ ran (.)$
15	13 14	sseqtrri	$⊢ ⋃ (.) [\{−∞\} \times ℝ] \subseteq ℝ$
16		id	$⊢ x \in ℝ \to x \in ℝ$
17		ltp1	$⊢ x \in ℝ \to x < x + 1$
18		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
19		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
20	18 19	sselid	$⊢ x \in ℝ \to x + 1 \in ℝ^{*}$
21		elioomnf	$⊢ x + 1 \in ℝ^{*} \to (x \in (−∞, x + 1) \leftrightarrow (x \in ℝ \land x < x + 1))$
22	20 21	syl	$⊢ x \in ℝ \to (x \in (−∞, x + 1) \leftrightarrow (x \in ℝ \land x < x + 1))$
23	16 17 22	mpbir2and	$⊢ x \in ℝ \to x \in (−∞, x + 1)$
24		df-ov	$⊢ (−∞, x + 1) = (.) (⟨−∞, x + 1⟩)$
25		mnfxr	$⊢ −∞ \in ℝ^{*}$
26	25	elexi	$⊢ −∞ \in V$
27	26	snid	$⊢ −∞ \in \{−∞\}$
28		opelxpi	$⊢ (−∞ \in \{−∞\} \land x + 1 \in ℝ) \to ⟨−∞, x + 1⟩ \in (\{−∞\} \times ℝ)$
29	27 19 28	sylancr	$⊢ x \in ℝ \to ⟨−∞, x + 1⟩ \in (\{−∞\} \times ℝ)$
30		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
31		ffun	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to Fun (.)$
32	30 31	ax-mp	$⊢ Fun (.)$
33		snssi	$⊢ −∞ \in ℝ^{} \to \{−∞\} \subseteq ℝ^{}$
34	25 33	ax-mp	$⊢ \{−∞\} \subseteq ℝ^{*}$
35		xpss12	$⊢ (\{−∞\} \subseteq ℝ^{} \land ℝ \subseteq ℝ^{}) \to \{−∞\} \times ℝ \subseteq ℝ^{} \times ℝ^{}$
36	34 18 35	mp2an	$⊢ \{−∞\} \times ℝ \subseteq ℝ^{} \times ℝ^{}$
37	30	fdmi	$⊢ dom (.) = ℝ^{} \times ℝ^{}$
38	36 37	sseqtrri	$⊢ \{−∞\} \times ℝ \subseteq dom (.)$
39		funfvima2	$⊢ (Fun (.) \land \{−∞\} \times ℝ \subseteq dom (.)) \to (⟨−∞, x + 1⟩ \in (\{−∞\} \times ℝ) \to (.) (⟨−∞, x + 1⟩) \in (.) [\{−∞\} \times ℝ])$
40	32 38 39	mp2an	$⊢ ⟨−∞, x + 1⟩ \in (\{−∞\} \times ℝ) \to (.) (⟨−∞, x + 1⟩) \in (.) [\{−∞\} \times ℝ]$
41	29 40	syl	$⊢ x \in ℝ \to (.) (⟨−∞, x + 1⟩) \in (.) [\{−∞\} \times ℝ]$
42	24 41	eqeltrid	$⊢ x \in ℝ \to (−∞, x + 1) \in (.) [\{−∞\} \times ℝ]$
43		elunii	$⊢ (x \in (−∞, x + 1) \land (−∞, x + 1) \in (.) [\{−∞\} \times ℝ]) \to x \in ⋃ (.) [\{−∞\} \times ℝ]$
44	23 42 43	syl2anc	$⊢ x \in ℝ \to x \in ⋃ (.) [\{−∞\} \times ℝ]$
45	44	ssriv	$⊢ ℝ \subseteq ⋃ (.) [\{−∞\} \times ℝ]$
46	15 45	eqssi	$⊢ ⋃ (.) [\{−∞\} \times ℝ] = ℝ$
47	11 46	eqtrdi	$⊢ u = (.) [\{−∞\} \times ℝ] \to ⋃ u = ℝ$
48	47	sseq2d	$⊢ u = (.) [\{−∞\} \times ℝ] \to (ran F \subseteq ⋃ u \leftrightarrow ran F \subseteq ℝ)$
49		pweq	$⊢ u = (.) [\{−∞\} \times ℝ] \to 𝒫 u = 𝒫 (.) [\{−∞\} \times ℝ]$
50	49	ineq1d	$⊢ u = (.) [\{−∞\} \times ℝ] \to 𝒫 u \cap Fin = 𝒫 (.) [\{−∞\} \times ℝ] \cap Fin$
51	50	rexeqdv	$⊢ u = (.) [\{−∞\} \times ℝ] \to (\exists v \in (𝒫 u \cap Fin) ran F \subseteq ⋃ v \leftrightarrow \exists v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) ran F \subseteq ⋃ v)$
52	48 51	imbi12d	$⊢ u = (.) [\{−∞\} \times ℝ] \to ((ran F \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \subseteq ⋃ v) \leftrightarrow (ran F \subseteq ℝ \to \exists v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) ran F \subseteq ⋃ v))$
53		rncmp	$⊢ (J \in Comp \land F \in (J Cn K)) \to K ↾_{𝑡} ran F \in Comp$
54	3 4 53	syl2anc	$⊢ φ \to K ↾_{𝑡} ran F \in Comp$
55		retop	$⊢ topGen (ran (.)) \in Top$
56	2 55	eqeltri	$⊢ K \in Top$
57	7	cmpsub	$⊢ (K \in Top \land ran F \subseteq ℝ) \to (K ↾_{𝑡} ran F \in Comp \leftrightarrow \forall u \in 𝒫 K (ran F \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \subseteq ⋃ v))$
58	56 10 57	sylancr	$⊢ φ \to (K ↾_{𝑡} ran F \in Comp \leftrightarrow \forall u \in 𝒫 K (ran F \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \subseteq ⋃ v))$
59	54 58	mpbid	$⊢ φ \to \forall u \in 𝒫 K (ran F \subseteq ⋃ u \to \exists v \in (𝒫 u \cap Fin) ran F \subseteq ⋃ v)$
60		retopbas	$⊢ ran (.) \in TopBases$
61		bastg	$⊢ ran (.) \in TopBases \to ran (.) \subseteq topGen (ran (.))$
62	60 61	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
63	62 2	sseqtrri	$⊢ ran (.) \subseteq K$
64	12 63	sstri	$⊢ (.) [\{−∞\} \times ℝ] \subseteq K$
65	56 64	elpwi2	$⊢ (.) [\{−∞\} \times ℝ] \in 𝒫 K$
66	65	a1i	$⊢ φ \to (.) [\{−∞\} \times ℝ] \in 𝒫 K$
67	52 59 66	rspcdva	$⊢ φ \to (ran F \subseteq ℝ \to \exists v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) ran F \subseteq ⋃ v)$
68	10 67	mpd	$⊢ φ \to \exists v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) ran F \subseteq ⋃ v$
69		elin	$⊢ v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \leftrightarrow (v \in 𝒫 (.) [\{−∞\} \times ℝ] \land v \in Fin)$
70	69	bilani	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to (v \in 𝒫 (.) [\{−∞\} \times ℝ] \land v \in Fin)$
71	70	adantrr	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to (v \in 𝒫 (.) [\{−∞\} \times ℝ] \land v \in Fin)$
72	71	simprd	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to v \in Fin$
73	70	simpld	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to v \in 𝒫 (.) [\{−∞\} \times ℝ]$
74	73	elpwid	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to v \subseteq (.) [\{−∞\} \times ℝ]$
75	34	sseli	$⊢ u \in \{−∞\} \to u \in ℝ^{*}$
76	75	adantr	$⊢ (u \in \{−∞\} \land w \in ℝ) \to u \in ℝ^{*}$
77	18	sseli	$⊢ w \in ℝ \to w \in ℝ^{*}$
78	77	adantl	$⊢ (u \in \{−∞\} \land w \in ℝ) \to w \in ℝ^{*}$
79		mnflt	$⊢ w \in ℝ \to −∞ < w$
80		xrltnle	$⊢ (−∞ \in ℝ^{} \land w \in ℝ^{}) \to (−∞ < w \leftrightarrow \neg w \leq −∞)$
81	25 77 80	sylancr	$⊢ w \in ℝ \to (−∞ < w \leftrightarrow \neg w \leq −∞)$
82	79 81	mpbid	$⊢ w \in ℝ \to \neg w \leq −∞$
83	82	adantl	$⊢ (u \in \{−∞\} \land w \in ℝ) \to \neg w \leq −∞$
84		elsni	$⊢ u \in \{−∞\} \to u = −∞$
85	84	adantr	$⊢ (u \in \{−∞\} \land w \in ℝ) \to u = −∞$
86	85	breq2d	$⊢ (u \in \{−∞\} \land w \in ℝ) \to (w \leq u \leftrightarrow w \leq −∞)$
87	83 86	mtbird	$⊢ (u \in \{−∞\} \land w \in ℝ) \to \neg w \leq u$
88		ioo0	$⊢ (u \in ℝ^{} \land w \in ℝ^{}) \to ((u, w) = \emptyset \leftrightarrow w \leq u)$
89	75 77 88	syl2an	$⊢ (u \in \{−∞\} \land w \in ℝ) \to ((u, w) = \emptyset \leftrightarrow w \leq u)$
90	89	necon3abid	$⊢ (u \in \{−∞\} \land w \in ℝ) \to ((u, w) \neq \emptyset \leftrightarrow \neg w \leq u)$
91	87 90	mpbird	$⊢ (u \in \{−∞\} \land w \in ℝ) \to (u, w) \neq \emptyset$
92		df-ioo	$⊢ (.) = (y \in ℝ^{}, z \in ℝ^{} ⟼ \{v \in ℝ^{*} \| (y < v \land v < z)\})$
93		idd	$⊢ (x \in ℝ^{} \land w \in ℝ^{}) \to (x < w \to x < w)$
94		xrltle	$⊢ (x \in ℝ^{} \land w \in ℝ^{}) \to (x < w \to x \leq w)$
95		idd	$⊢ (u \in ℝ^{} \land x \in ℝ^{}) \to (u < x \to u < x)$
96		xrltle	$⊢ (u \in ℝ^{} \land x \in ℝ^{}) \to (u < x \to u \leq x)$
97	92 93 94 95 96	ixxub	$⊢ (u \in ℝ^{} \land w \in ℝ^{} \land (u, w) \neq \emptyset) \to sup ((u, w) ℝ^{*} <) = w$
98	76 78 91 97	syl3anc	$⊢ (u \in \{−∞\} \land w \in ℝ) \to sup ((u, w) ℝ^{*} <) = w$
99		simpr	$⊢ (u \in \{−∞\} \land w \in ℝ) \to w \in ℝ$
100	98 99	eqeltrd	$⊢ (u \in \{−∞\} \land w \in ℝ) \to sup ((u, w) ℝ^{*} <) \in ℝ$
101	100	rgen2	$⊢ \forall u \in \{−∞\} \forall w \in ℝ sup ((u, w) ℝ^{*} <) \in ℝ$
102		fveq2	$⊢ z = ⟨u, w⟩ \to (.) (z) = (.) (⟨u, w⟩)$
103		df-ov	$⊢ (u, w) = (.) (⟨u, w⟩)$
104	102 103	eqtr4di	$⊢ z = ⟨u, w⟩ \to (.) (z) = (u, w)$
105	104	supeq1d	$⊢ z = ⟨u, w⟩ \to sup ((.) (z) ℝ^{} <) = sup ((u, w) ℝ^{} <)$
106	105	eleq1d	$⊢ z = ⟨u, w⟩ \to (sup ((.) (z) ℝ^{} <) \in ℝ \leftrightarrow sup ((u, w) ℝ^{} <) \in ℝ)$
107	106	ralxp	$⊢ \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{} <) \in ℝ \leftrightarrow \forall u \in \{−∞\} \forall w \in ℝ sup ((u, w) ℝ^{} <) \in ℝ$
108	101 107	mpbir	$⊢ \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{*} <) \in ℝ$
109		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
110	30 109	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
111		supeq1	$⊢ w = (.) (z) \to sup (w ℝ^{} <) = sup ((.) (z) ℝ^{} <)$
112	111	eleq1d	$⊢ w = (.) (z) \to (sup (w ℝ^{} <) \in ℝ \leftrightarrow sup ((.) (z) ℝ^{} <) \in ℝ)$
113	112	ralima	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land \{−∞\} \times ℝ \subseteq ℝ^{} \times ℝ^{}) \to (\forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{} <) \in ℝ \leftrightarrow \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{} <) \in ℝ)$
114	110 36 113	mp2an	$⊢ \forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{} <) \in ℝ \leftrightarrow \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{} <) \in ℝ$
115	108 114	mpbir	$⊢ \forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{*} <) \in ℝ$
116		ssralv	$⊢ v \subseteq (.) [\{−∞\} \times ℝ] \to (\forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{} <) \in ℝ \to \forall w \in v sup (w ℝ^{} <) \in ℝ)$
117	74 115 116	mpisyl	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to \forall w \in v sup (w ℝ^{*} <) \in ℝ$
118	117	adantrr	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to \forall w \in v sup (w ℝ^{*} <) \in ℝ$
119		fimaxre3	$⊢ (v \in Fin \land \forall w \in v sup (w ℝ^{} <) \in ℝ) \to \exists x \in ℝ \forall w \in v sup (w ℝ^{} <) \leq x$
120	72 118 119	syl2anc	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to \exists x \in ℝ \forall w \in v sup (w ℝ^{*} <) \leq x$
121		simplrr	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to ran F \subseteq ⋃ v$
122	121	sselda	$⊢ (((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \land z \in ran F) \to z \in ⋃ v$
123		eluni2	$⊢ z \in ⋃ v \leftrightarrow \exists w \in v z \in w$
124		r19.29r	$⊢ (\exists w \in v z \in w \land \forall w \in v sup (w ℝ^{} <) \leq x) \to \exists w \in v (z \in w \land sup (w ℝ^{} <) \leq x)$
125		sspwuni	$⊢ (.) [\{−∞\} \times ℝ] \subseteq 𝒫 ℝ \leftrightarrow ⋃ (.) [\{−∞\} \times ℝ] \subseteq ℝ$
126	15 125	mpbir	$⊢ (.) [\{−∞\} \times ℝ] \subseteq 𝒫 ℝ$
127	74	3ad2ant1	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to v \subseteq (.) [\{−∞\} \times ℝ]$
128		simp2r	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to w \in v$
129	127 128	sseldd	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to w \in (.) [\{−∞\} \times ℝ]$
130	126 129	sselid	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to w \in 𝒫 ℝ$
131	130	elpwid	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to w \subseteq ℝ$
132		simp3l	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to z \in w$
133	131 132	sseldd	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to z \in ℝ$
134	117	r19.21bi	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land w \in v) \to sup (w ℝ^{*} <) \in ℝ$
135	134	adantrl	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v)) \to sup (w ℝ^{*} <) \in ℝ$
136	135	3adant3	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{} <) \leq x)) \to sup (w ℝ^{} <) \in ℝ$
137		simp2l	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to x \in ℝ$
138	131 18	sstrdi	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{} <) \leq x)) \to w \subseteq ℝ^{}$
139		supxrub	$⊢ (w \subseteq ℝ^{} \land z \in w) \to z \leq sup (w ℝ^{} <)$
140	138 132 139	syl2anc	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{} <) \leq x)) \to z \leq sup (w ℝ^{} <)$
141		simp3r	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{} <) \leq x)) \to sup (w ℝ^{} <) \leq x$
142	133 136 137 140 141	letrd	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v) \land (z \in w \land sup (w ℝ^{*} <) \leq x)) \to z \leq x$
143	142	3expia	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v)) \to ((z \in w \land sup (w ℝ^{*} <) \leq x) \to z \leq x)$
144	143	anassrs	$⊢ (((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land x \in ℝ) \land w \in v) \to ((z \in w \land sup (w ℝ^{*} <) \leq x) \to z \leq x)$
145	144	rexlimdva	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land x \in ℝ) \to (\exists w \in v (z \in w \land sup (w ℝ^{*} <) \leq x) \to z \leq x)$
146	145	adantlrr	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to (\exists w \in v (z \in w \land sup (w ℝ^{*} <) \leq x) \to z \leq x)$
147	124 146	syl5	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to ((\exists w \in v z \in w \land \forall w \in v sup (w ℝ^{*} <) \leq x) \to z \leq x)$
148	147	expdimp	$⊢ (((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \land \exists w \in v z \in w) \to (\forall w \in v sup (w ℝ^{*} <) \leq x \to z \leq x)$
149	123 148	sylan2b	$⊢ (((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \land z \in ⋃ v) \to (\forall w \in v sup (w ℝ^{*} <) \leq x \to z \leq x)$
150	122 149	syldan	$⊢ (((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \land z \in ran F) \to (\forall w \in v sup (w ℝ^{*} <) \leq x \to z \leq x)$
151	150	ralrimdva	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to (\forall w \in v sup (w ℝ^{*} <) \leq x \to \forall z \in ran F z \leq x)$
152	9	ffnd	$⊢ φ \to F Fn X$
153	152	ad2antrr	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to F Fn X$
154		breq1	$⊢ z = F (y) \to (z \leq x \leftrightarrow F (y) \leq x)$
155	154	ralrn	$⊢ F Fn X \to (\forall z \in ran F z \leq x \leftrightarrow \forall y \in X F (y) \leq x)$
156	153 155	syl	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to (\forall z \in ran F z \leq x \leftrightarrow \forall y \in X F (y) \leq x)$
157	151 156	sylibd	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to (\forall w \in v sup (w ℝ^{*} <) \leq x \to \forall y \in X F (y) \leq x)$
158	157	reximdva	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to (\exists x \in ℝ \forall w \in v sup (w ℝ^{*} <) \leq x \to \exists x \in ℝ \forall y \in X F (y) \leq x)$
159	120 158	mpd	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to \exists x \in ℝ \forall y \in X F (y) \leq x$
160	68 159	rexlimddv	$⊢ φ \to \exists x \in ℝ \forall y \in X F (y) \leq x$

Metamath Proof Explorer

Theorem bndth

Proof