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		simpr	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)$
70		elin	$⊢ v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \leftrightarrow (v \in 𝒫 (.) [\{−∞\} \times ℝ] \land v \in Fin)$
71	69 70	sylib	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to (v \in 𝒫 (.) [\{−∞\} \times ℝ] \land v \in Fin)$
72	71	adantrr	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to (v \in 𝒫 (.) [\{−∞\} \times ℝ] \land v \in Fin)$
73	72	simprd	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to v \in Fin$
74	71	simpld	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to v \in 𝒫 (.) [\{−∞\} \times ℝ]$
75	74	elpwid	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to v \subseteq (.) [\{−∞\} \times ℝ]$
76	34	sseli	$⊢ u \in \{−∞\} \to u \in ℝ^{*}$
77	76	adantr	$⊢ (u \in \{−∞\} \land w \in ℝ) \to u \in ℝ^{*}$
78	18	sseli	$⊢ w \in ℝ \to w \in ℝ^{*}$
79	78	adantl	$⊢ (u \in \{−∞\} \land w \in ℝ) \to w \in ℝ^{*}$
80		mnflt	$⊢ w \in ℝ \to −∞ < w$
81		xrltnle	$⊢ (−∞ \in ℝ^{} \land w \in ℝ^{}) \to (−∞ < w \leftrightarrow \neg w \leq −∞)$
82	25 78 81	sylancr	$⊢ w \in ℝ \to (−∞ < w \leftrightarrow \neg w \leq −∞)$
83	80 82	mpbid	$⊢ w \in ℝ \to \neg w \leq −∞$
84	83	adantl	$⊢ (u \in \{−∞\} \land w \in ℝ) \to \neg w \leq −∞$
85		elsni	$⊢ u \in \{−∞\} \to u = −∞$
86	85	adantr	$⊢ (u \in \{−∞\} \land w \in ℝ) \to u = −∞$
87	86	breq2d	$⊢ (u \in \{−∞\} \land w \in ℝ) \to (w \leq u \leftrightarrow w \leq −∞)$
88	84 87	mtbird	$⊢ (u \in \{−∞\} \land w \in ℝ) \to \neg w \leq u$
89		ioo0	$⊢ (u \in ℝ^{} \land w \in ℝ^{}) \to ((u, w) = \emptyset \leftrightarrow w \leq u)$
90	76 78 89	syl2an	$⊢ (u \in \{−∞\} \land w \in ℝ) \to ((u, w) = \emptyset \leftrightarrow w \leq u)$
91	90	necon3abid	$⊢ (u \in \{−∞\} \land w \in ℝ) \to ((u, w) \neq \emptyset \leftrightarrow \neg w \leq u)$
92	88 91	mpbird	$⊢ (u \in \{−∞\} \land w \in ℝ) \to (u, w) \neq \emptyset$
93		df-ioo	$⊢ (.) = (y \in ℝ^{}, z \in ℝ^{} ⟼ \{v \in ℝ^{*} \| (y < v \land v < z)\})$
94		idd	$⊢ (x \in ℝ^{} \land w \in ℝ^{}) \to (x < w \to x < w)$
95		xrltle	$⊢ (x \in ℝ^{} \land w \in ℝ^{}) \to (x < w \to x \leq w)$
96		idd	$⊢ (u \in ℝ^{} \land x \in ℝ^{}) \to (u < x \to u < x)$
97		xrltle	$⊢ (u \in ℝ^{} \land x \in ℝ^{}) \to (u < x \to u \leq x)$
98	93 94 95 96 97	ixxub	$⊢ (u \in ℝ^{} \land w \in ℝ^{} \land (u, w) \neq \emptyset) \to sup ((u, w) ℝ^{*} <) = w$
99	77 79 92 98	syl3anc	$⊢ (u \in \{−∞\} \land w \in ℝ) \to sup ((u, w) ℝ^{*} <) = w$
100		simpr	$⊢ (u \in \{−∞\} \land w \in ℝ) \to w \in ℝ$
101	99 100	eqeltrd	$⊢ (u \in \{−∞\} \land w \in ℝ) \to sup ((u, w) ℝ^{*} <) \in ℝ$
102	101	rgen2	$⊢ \forall u \in \{−∞\} \forall w \in ℝ sup ((u, w) ℝ^{*} <) \in ℝ$
103		fveq2	$⊢ z = ⟨u, w⟩ \to (.) (z) = (.) (⟨u, w⟩)$
104		df-ov	$⊢ (u, w) = (.) (⟨u, w⟩)$
105	103 104	eqtr4di	$⊢ z = ⟨u, w⟩ \to (.) (z) = (u, w)$
106	105	supeq1d	$⊢ z = ⟨u, w⟩ \to sup ((.) (z) ℝ^{} <) = sup ((u, w) ℝ^{} <)$
107	106	eleq1d	$⊢ z = ⟨u, w⟩ \to (sup ((.) (z) ℝ^{} <) \in ℝ \leftrightarrow sup ((u, w) ℝ^{} <) \in ℝ)$
108	107	ralxp	$⊢ \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{} <) \in ℝ \leftrightarrow \forall u \in \{−∞\} \forall w \in ℝ sup ((u, w) ℝ^{} <) \in ℝ$
109	102 108	mpbir	$⊢ \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{*} <) \in ℝ$
110		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
111	30 110	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
112		supeq1	$⊢ w = (.) (z) \to sup (w ℝ^{} <) = sup ((.) (z) ℝ^{} <)$
113	112	eleq1d	$⊢ w = (.) (z) \to (sup (w ℝ^{} <) \in ℝ \leftrightarrow sup ((.) (z) ℝ^{} <) \in ℝ)$
114	113	ralima	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land \{−∞\} \times ℝ \subseteq ℝ^{} \times ℝ^{}) \to (\forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{} <) \in ℝ \leftrightarrow \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{} <) \in ℝ)$
115	111 36 114	mp2an	$⊢ \forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{} <) \in ℝ \leftrightarrow \forall z \in (\{−∞\} \times ℝ) sup ((.) (z) ℝ^{} <) \in ℝ$
116	109 115	mpbir	$⊢ \forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{*} <) \in ℝ$
117		ssralv	$⊢ v \subseteq (.) [\{−∞\} \times ℝ] \to (\forall w \in (.) [\{−∞\} \times ℝ] sup (w ℝ^{} <) \in ℝ \to \forall w \in v sup (w ℝ^{} <) \in ℝ)$
118	75 116 117	mpisyl	$⊢ (φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \to \forall w \in v sup (w ℝ^{*} <) \in ℝ$
119	118	adantrr	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to \forall w \in v sup (w ℝ^{*} <) \in ℝ$
120		fimaxre3	$⊢ (v \in Fin \land \forall w \in v sup (w ℝ^{} <) \in ℝ) \to \exists x \in ℝ \forall w \in v sup (w ℝ^{} <) \leq x$
121	73 119 120	syl2anc	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to \exists x \in ℝ \forall w \in v sup (w ℝ^{*} <) \leq x$
122		simplrr	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to ran F \subseteq ⋃ v$
123	122	sselda	$⊢ (((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \land z \in ran F) \to z \in ⋃ v$
124		eluni2	$⊢ z \in ⋃ v \leftrightarrow \exists w \in v z \in w$
125		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)$
126		sspwuni	$⊢ (.) [\{−∞\} \times ℝ] \subseteq 𝒫 ℝ \leftrightarrow ⋃ (.) [\{−∞\} \times ℝ] \subseteq ℝ$
127	15 126	mpbir	$⊢ (.) [\{−∞\} \times ℝ] \subseteq 𝒫 ℝ$
128	75	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 ℝ]$
129		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$
130	128 129	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 ℝ]$
131	127 130	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 𝒫 ℝ$
132	131	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 ℝ$
133		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$
134	132 133	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 ℝ$
135	118	r19.21bi	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land w \in v) \to sup (w ℝ^{*} <) \in ℝ$
136	135	adantrl	$⊢ ((φ \land v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin)) \land (x \in ℝ \land w \in v)) \to sup (w ℝ^{*} <) \in ℝ$
137	136	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 ℝ$
138		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 ℝ$
139	132 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 ℝ^{}$
140		supxrub	$⊢ (w \subseteq ℝ^{} \land z \in w) \to z \leq sup (w ℝ^{} <)$
141	139 133 140	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 ℝ^{} <)$
142		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$
143	134 137 138 141 142	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$
144	143	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)$
145	144	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)$
146	145	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)$
147	146	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)$
148	125 147	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)$
149	148	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)$
150	124 149	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)$
151	123 150	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)$
152	151	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)$
153	9	ffnd	$⊢ φ \to F Fn X$
154	153	ad2antrr	$⊢ ((φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \land x \in ℝ) \to F Fn X$
155		breq1	$⊢ z = F (y) \to (z \leq x \leftrightarrow F (y) \leq x)$
156	155	ralrn	$⊢ F Fn X \to (\forall z \in ran F z \leq x \leftrightarrow \forall y \in X F (y) \leq x)$
157	154 156	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)$
158	152 157	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)$
159	158	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)$
160	121 159	mpd	$⊢ (φ \land (v \in (𝒫 (.) [\{−∞\} \times ℝ] \cap Fin) \land ran F \subseteq ⋃ v)) \to \exists x \in ℝ \forall y \in X F (y) \leq x$
161	68 160	rexlimddv	$⊢ φ \to \exists x \in ℝ \forall y \in X F (y) \leq x$

Metamath Proof Explorer

Theorem bndth

Proof