rfcnnnub

Description: Given a real continuous function F defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	rfcnnnub.1	$⊢ \underline{Ⅎ} t F$
	rfcnnnub.2	$⊢ Ⅎ t φ$
	rfcnnnub.3	$⊢ K = topGen (ran (.))$
	rfcnnnub.4	$⊢ φ \to J \in Comp$
	rfcnnnub.5	$⊢ T = ⋃ J$
	rfcnnnub.6	$⊢ φ \to T \neq \emptyset$
	rfcnnnub.7	$⊢ C = J Cn K$
	rfcnnnub.8	$⊢ φ \to F \in C$
Assertion	rfcnnnub	$⊢ φ \to \exists n \in ℕ \forall t \in T F (t) < n$

Proof

Step	Hyp	Ref	Expression
1		rfcnnnub.1	$⊢ \underline{Ⅎ} t F$
2		rfcnnnub.2	$⊢ Ⅎ t φ$
3		rfcnnnub.3	$⊢ K = topGen (ran (.))$
4		rfcnnnub.4	$⊢ φ \to J \in Comp$
5		rfcnnnub.5	$⊢ T = ⋃ J$
6		rfcnnnub.6	$⊢ φ \to T \neq \emptyset$
7		rfcnnnub.7	$⊢ C = J Cn K$
8		rfcnnnub.8	$⊢ φ \to F \in C$
9		nfcv	$⊢ \underline{Ⅎ} s F$
10		nfcv	$⊢ \underline{Ⅎ} s T$
11		nfcv	$⊢ \underline{Ⅎ} t T$
12		nfv	$⊢ Ⅎ s φ$
13	8 7	eleqtrdi	$⊢ φ \to F \in (J Cn K)$
14	9 1 10 11 12 2 5 3 4 13 6	evthf	$⊢ φ \to \exists s \in T \forall t \in T F (t) \leq F (s)$
15		df-rex	$⊢ \exists s \in T \forall t \in T F (t) \leq F (s) \leftrightarrow \exists s (s \in T \land \forall t \in T F (t) \leq F (s))$
16	14 15	sylib	$⊢ φ \to \exists s (s \in T \land \forall t \in T F (t) \leq F (s))$
17	3 5 7 8	fcnre	$⊢ φ \to F : T ⟶ ℝ$
18	17	ffvelrnda	$⊢ (φ \land s \in T) \to F (s) \in ℝ$
19	18	ex	$⊢ φ \to (s \in T \to F (s) \in ℝ)$
20	19	anim1d	$⊢ φ \to ((s \in T \land \forall t \in T F (t) \leq F (s)) \to (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s)))$
21	20	eximdv	$⊢ φ \to (\exists s (s \in T \land \forall t \in T F (t) \leq F (s)) \to \exists s (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s)))$
22	16 21	mpd	$⊢ φ \to \exists s (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s))$
23	17	ffvelrnda	$⊢ (φ \land t \in T) \to F (t) \in ℝ$
24	23	ex	$⊢ φ \to (t \in T \to F (t) \in ℝ)$
25	2 24	ralrimi	$⊢ φ \to \forall t \in T F (t) \in ℝ$
26		19.41v	$⊢ \exists s ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s)) \land \forall t \in T F (t) \in ℝ) \leftrightarrow (\exists s (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s)) \land \forall t \in T F (t) \in ℝ)$
27	22 25 26	sylanbrc	$⊢ φ \to \exists s ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s)) \land \forall t \in T F (t) \in ℝ)$
28		df-3an	$⊢ (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \leftrightarrow ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s)) \land \forall t \in T F (t) \in ℝ)$
29	28	exbii	$⊢ \exists s (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \leftrightarrow \exists s ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s)) \land \forall t \in T F (t) \in ℝ)$
30	27 29	sylibr	$⊢ φ \to \exists s (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ)$
31		nfcv	$⊢ \underline{Ⅎ} t s$
32	1 31	nffv	$⊢ \underline{Ⅎ} t F (s)$
33	32	nfel1	$⊢ Ⅎ t F (s) \in ℝ$
34		nfra1	$⊢ Ⅎ t \forall t \in T F (t) \leq F (s)$
35		nfra1	$⊢ Ⅎ t \forall t \in T F (t) \in ℝ$
36	33 34 35	nf3an	$⊢ Ⅎ t (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ)$
37		nfv	$⊢ Ⅎ t n \in ℕ$
38		nfcv	$⊢ \underline{Ⅎ} t <$
39		nfcv	$⊢ \underline{Ⅎ} t n$
40	32 38 39	nfbr	$⊢ Ⅎ t F (s) < n$
41	37 40	nfan	$⊢ Ⅎ t (n \in ℕ \land F (s) < n)$
42	36 41	nfan	$⊢ Ⅎ t ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n))$
43		simpll3	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to \forall t \in T F (t) \in ℝ$
44		simpr	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to t \in T$
45		rsp	$⊢ \forall t \in T F (t) \in ℝ \to (t \in T \to F (t) \in ℝ)$
46	43 44 45	sylc	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to F (t) \in ℝ$
47		simpll1	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to F (s) \in ℝ$
48		simplrl	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to n \in ℕ$
49	48	nnred	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to n \in ℝ$
50		simpl2	$⊢ ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \to \forall t \in T F (t) \leq F (s)$
51	50	r19.21bi	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to F (t) \leq F (s)$
52		simplrr	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to F (s) < n$
53	46 47 49 51 52	lelttrd	$⊢ (((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \land t \in T) \to F (t) < n$
54	53	ex	$⊢ ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \to (t \in T \to F (t) < n)$
55	42 54	ralrimi	$⊢ ((F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \land (n \in ℕ \land F (s) < n)) \to \forall t \in T F (t) < n$
56		arch	$⊢ F (s) \in ℝ \to \exists n \in ℕ F (s) < n$
57	56	3ad2ant1	$⊢ (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \to \exists n \in ℕ F (s) < n$
58	55 57	reximddv	$⊢ (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \to \exists n \in ℕ \forall t \in T F (t) < n$
59	58	eximi	$⊢ \exists s (F (s) \in ℝ \land \forall t \in T F (t) \leq F (s) \land \forall t \in T F (t) \in ℝ) \to \exists s \exists n \in ℕ \forall t \in T F (t) < n$
60	30 59	syl	$⊢ φ \to \exists s \exists n \in ℕ \forall t \in T F (t) < n$
61		19.9v	$⊢ \exists s \exists n \in ℕ \forall t \in T F (t) < n \leftrightarrow \exists n \in ℕ \forall t \in T F (t) < n$
62	60 61	sylib	$⊢ φ \to \exists n \in ℕ \forall t \in T F (t) < n$

Metamath Proof Explorer

Theorem rfcnnnub

Proof