uzublem

Description: A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	uzublem.1	$⊢ Ⅎ j φ$
	uzublem.2	$⊢ \underline{Ⅎ} j X$
	uzublem.3	$⊢ φ \to M \in ℤ$
	uzublem.4	$⊢ Z = ℤ_{\geq M}$
	uzublem.5	$⊢ φ \to Y \in ℝ$
	uzublem.6	$⊢ W = sup (ran (j \in (M \dots K) ⟼ B) ℝ <)$
	uzublem.7	$⊢ X = if (W \leq Y, Y, W)$
	uzublem.8	$⊢ φ \to K \in Z$
	uzublem.9	$⊢ (φ \land j \in Z) \to B \in ℝ$
	uzublem.10	$⊢ φ \to \forall j \in ℤ_{\geq K} B \leq Y$
Assertion	uzublem	$⊢ φ \to \exists x \in ℝ \forall j \in Z B \leq x$

Proof

Step	Hyp	Ref	Expression
1		uzublem.1	$⊢ Ⅎ j φ$
2		uzublem.2	$⊢ \underline{Ⅎ} j X$
3		uzublem.3	$⊢ φ \to M \in ℤ$
4		uzublem.4	$⊢ Z = ℤ_{\geq M}$
5		uzublem.5	$⊢ φ \to Y \in ℝ$
6		uzublem.6	$⊢ W = sup (ran (j \in (M \dots K) ⟼ B) ℝ <)$
7		uzublem.7	$⊢ X = if (W \leq Y, Y, W)$
8		uzublem.8	$⊢ φ \to K \in Z$
9		uzublem.9	$⊢ (φ \land j \in Z) \to B \in ℝ$
10		uzublem.10	$⊢ φ \to \forall j \in ℤ_{\geq K} B \leq Y$
11	6	a1i	$⊢ φ \to W = sup (ran (j \in (M \dots K) ⟼ B) ℝ <)$
12		ltso	$⊢ < Or ℝ$
13	12	a1i	$⊢ φ \to < Or ℝ$
14		fzfid	$⊢ φ \to (M \dots K) \in Fin$
15	4	eluzelz2	$⊢ K \in Z \to K \in ℤ$
16	8 15	syl	$⊢ φ \to K \in ℤ$
17	3	zred	$⊢ φ \to M \in ℝ$
18	17	leidd	$⊢ φ \to M \leq M$
19	8 4	eleqtrdi	$⊢ φ \to K \in ℤ_{\geq M}$
20		eluzle	$⊢ K \in ℤ_{\geq M} \to M \leq K$
21	19 20	syl	$⊢ φ \to M \leq K$
22	3 16 3 18 21	elfzd	$⊢ φ \to M \in (M \dots K)$
23	22	ne0d	$⊢ φ \to (M \dots K) \neq \emptyset$
24		fzssuz	$⊢ (M \dots K) \subseteq ℤ_{\geq M}$
25	4	eqcomi	$⊢ ℤ_{\geq M} = Z$
26	24 25	sseqtri	$⊢ (M \dots K) \subseteq Z$
27		id	$⊢ j \in (M \dots K) \to j \in (M \dots K)$
28	26 27	sselid	$⊢ j \in (M \dots K) \to j \in Z$
29	28 9	sylan2	$⊢ (φ \land j \in (M \dots K)) \to B \in ℝ$
30	1 13 14 23 29	fisupclrnmpt	$⊢ φ \to sup (ran (j \in (M \dots K) ⟼ B) ℝ <) \in ℝ$
31	11 30	eqeltrd	$⊢ φ \to W \in ℝ$
32	5 31	ifcld	$⊢ φ \to if (W \leq Y, Y, W) \in ℝ$
33	7 32	eqeltrid	$⊢ φ \to X \in ℝ$
34	9	adantr	$⊢ ((φ \land j \in Z) \land K \leq j) \to B \in ℝ$
35	5	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to Y \in ℝ$
36	33	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to X \in ℝ$
37	10	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to \forall j \in ℤ_{\geq K} B \leq Y$
38		eqid	$⊢ ℤ_{\geq K} = ℤ_{\geq K}$
39	16	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to K \in ℤ$
40	4	eluzelz2	$⊢ j \in Z \to j \in ℤ$
41	40	ad2antlr	$⊢ ((φ \land j \in Z) \land K \leq j) \to j \in ℤ$
42		simpr	$⊢ ((φ \land j \in Z) \land K \leq j) \to K \leq j$
43	38 39 41 42	eluzd	$⊢ ((φ \land j \in Z) \land K \leq j) \to j \in ℤ_{\geq K}$
44		rspa	$⊢ (\forall j \in ℤ_{\geq K} B \leq Y \land j \in ℤ_{\geq K}) \to B \leq Y$
45	37 43 44	syl2anc	$⊢ ((φ \land j \in Z) \land K \leq j) \to B \leq Y$
46		max2	$⊢ (W \in ℝ \land Y \in ℝ) \to Y \leq if (W \leq Y, Y, W)$
47	31 5 46	syl2anc	$⊢ φ \to Y \leq if (W \leq Y, Y, W)$
48	47 7	breqtrrdi	$⊢ φ \to Y \leq X$
49	48	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to Y \leq X$
50	34 35 36 45 49	letrd	$⊢ ((φ \land j \in Z) \land K \leq j) \to B \leq X$
51		simpr	$⊢ ((φ \land j \in Z) \land \neg K \leq j) \to \neg K \leq j$
52		uzssre	$⊢ ℤ_{\geq M} \subseteq ℝ$
53	4 52	eqsstri	$⊢ Z \subseteq ℝ$
54	53	sseli	$⊢ j \in Z \to j \in ℝ$
55	54	ad2antlr	$⊢ ((φ \land j \in Z) \land \neg K \leq j) \to j \in ℝ$
56	53 8	sselid	$⊢ φ \to K \in ℝ$
57	56	ad2antrr	$⊢ ((φ \land j \in Z) \land \neg K \leq j) \to K \in ℝ$
58	55 57	ltnled	$⊢ ((φ \land j \in Z) \land \neg K \leq j) \to (j < K \leftrightarrow \neg K \leq j)$
59	51 58	mpbird	$⊢ ((φ \land j \in Z) \land \neg K \leq j) \to j < K$
60	9	adantr	$⊢ ((φ \land j \in Z) \land j < K) \to B \in ℝ$
61	6 31	eqeltrrid	$⊢ φ \to sup (ran (j \in (M \dots K) ⟼ B) ℝ <) \in ℝ$
62	6 61	eqeltrid	$⊢ φ \to W \in ℝ$
63	62	ad2antrr	$⊢ ((φ \land j \in Z) \land j < K) \to W \in ℝ$
64	5 62	ifcld	$⊢ φ \to if (W \leq Y, Y, W) \in ℝ$
65	7 64	eqeltrid	$⊢ φ \to X \in ℝ$
66	65	ad2antrr	$⊢ ((φ \land j \in Z) \land j < K) \to X \in ℝ$
67		simpll	$⊢ ((φ \land j \in Z) \land j < K) \to φ$
68	3	ad2antrr	$⊢ ((φ \land j \in Z) \land j < K) \to M \in ℤ$
69	16	ad2antrr	$⊢ ((φ \land j \in Z) \land j < K) \to K \in ℤ$
70	4	eleq2i	$⊢ j \in Z \leftrightarrow j \in ℤ_{\geq M}$
71	70	biimpi	$⊢ j \in Z \to j \in ℤ_{\geq M}$
72	71	ad2antlr	$⊢ ((φ \land j \in Z) \land j < K) \to j \in ℤ_{\geq M}$
73		simpr	$⊢ ((φ \land j \in Z) \land j < K) \to j < K$
74	72 69 73	elfzod	$⊢ ((φ \land j \in Z) \land j < K) \to j \in (M ..^K)$
75		elfzouz	$⊢ j \in (M ..^K) \to j \in ℤ_{\geq M}$
76	75 25	eleqtrdi	$⊢ j \in (M ..^K) \to j \in Z$
77	74 76 40	3syl	$⊢ ((φ \land j \in Z) \land j < K) \to j \in ℤ$
78		eluzle	$⊢ j \in ℤ_{\geq M} \to M \leq j$
79	71 78	syl	$⊢ j \in Z \to M \leq j$
80	79	ad2antlr	$⊢ ((φ \land j \in Z) \land j < K) \to M \leq j$
81	74 76 54	3syl	$⊢ ((φ \land j \in Z) \land j < K) \to j \in ℝ$
82	56	ad2antrr	$⊢ ((φ \land j \in Z) \land j < K) \to K \in ℝ$
83	81 82 73	ltled	$⊢ ((φ \land j \in Z) \land j < K) \to j \leq K$
84	68 69 77 80 83	elfzd	$⊢ ((φ \land j \in Z) \land j < K) \to j \in (M \dots K)$
85	1 29	ralrimia	$⊢ φ \to \forall j \in (M \dots K) B \in ℝ$
86		fimaxre3	$⊢ ((M \dots K) \in Fin \land \forall j \in (M \dots K) B \in ℝ) \to \exists y \in ℝ \forall j \in (M \dots K) B \leq y$
87	14 85 86	syl2anc	$⊢ φ \to \exists y \in ℝ \forall j \in (M \dots K) B \leq y$
88	1 29 87	suprubrnmpt	$⊢ (φ \land j \in (M \dots K)) \to B \leq sup (ran (j \in (M \dots K) ⟼ B) ℝ <)$
89	67 84 88	syl2anc	$⊢ ((φ \land j \in Z) \land j < K) \to B \leq sup (ran (j \in (M \dots K) ⟼ B) ℝ <)$
90	89 6	breqtrrdi	$⊢ ((φ \land j \in Z) \land j < K) \to B \leq W$
91		max1	$⊢ (W \in ℝ \land Y \in ℝ) \to W \leq if (W \leq Y, Y, W)$
92	31 5 91	syl2anc	$⊢ φ \to W \leq if (W \leq Y, Y, W)$
93	92 7	breqtrrdi	$⊢ φ \to W \leq X$
94	93	ad2antrr	$⊢ ((φ \land j \in Z) \land j < K) \to W \leq X$
95	60 63 66 90 94	letrd	$⊢ ((φ \land j \in Z) \land j < K) \to B \leq X$
96	59 95	syldan	$⊢ ((φ \land j \in Z) \land \neg K \leq j) \to B \leq X$
97	50 96	pm2.61dan	$⊢ (φ \land j \in Z) \to B \leq X$
98	97	ex	$⊢ φ \to (j \in Z \to B \leq X)$
99	1 98	ralrimi	$⊢ φ \to \forall j \in Z B \leq X$
100		nfv	$⊢ Ⅎ x \forall j \in Z B \leq X$
101		nfcv	$⊢ \underline{Ⅎ} j x$
102	101 2	nfeq	$⊢ Ⅎ j x = X$
103		breq2	$⊢ x = X \to (B \leq x \leftrightarrow B \leq X)$
104	102 103	ralbid	$⊢ x = X \to (\forall j \in Z B \leq x \leftrightarrow \forall j \in Z B \leq X)$
105	100 104	rspce	$⊢ (X \in ℝ \land \forall j \in Z B \leq X) \to \exists x \in ℝ \forall j \in Z B \leq x$
106	33 99 105	syl2anc	$⊢ φ \to \exists x \in ℝ \forall j \in Z B \leq x$

Metamath Proof Explorer

Theorem uzublem

Proof