uzwo3

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 allows the lower bound B to be any real number. See also nnwo and nnwos . (Contributed by NM, 12-Nov-2004) (Proof shortened by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 27-Sep-2020)

		Ref	Expression
	Assertion	uzwo3	$⊢ (B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \to \exists! x \in A \forall y \in A x \leq y$

Proof

Step	Hyp	Ref	Expression
1		renegcl	$⊢ B \in ℝ \to - B \in ℝ$
2	1	adantr	$⊢ (B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \to - B \in ℝ$
3		arch	$⊢ - B \in ℝ \to \exists n \in ℕ - B < n$
4	2 3	syl	$⊢ (B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \to \exists n \in ℕ - B < n$
5		simplrl	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to A \subseteq \{z \in ℤ \| B \leq z\}$
6		simplrl	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to n \in ℕ$
7		nnnegz	$⊢ n \in ℕ \to - n \in ℤ$
8	6 7	syl	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to - n \in ℤ$
9	8	zred	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to - n \in ℝ$
10		simprl	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to z \in ℤ$
11	10	zred	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to z \in ℝ$
12		simpll	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to B \in ℝ$
13	6	nnred	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to n \in ℝ$
14		simplrr	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to - B < n$
15	12 13 14	ltnegcon1d	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to - n < B$
16		simprr	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to B \leq z$
17	9 12 11 15 16	ltletrd	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to - n < z$
18	9 11 17	ltled	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to - n \leq z$
19		eluz	$⊢ (- n \in ℤ \land z \in ℤ) \to (z \in ℤ_{\geq (- n)} \leftrightarrow - n \leq z)$
20	8 10 19	syl2anc	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to (z \in ℤ_{\geq (- n)} \leftrightarrow - n \leq z)$
21	18 20	mpbird	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land (z \in ℤ \land B \leq z)) \to z \in ℤ_{\geq (- n)}$
22	21	expr	$⊢ ((B \in ℝ \land (n \in ℕ \land - B < n)) \land z \in ℤ) \to (B \leq z \to z \in ℤ_{\geq (- n)})$
23	22	ralrimiva	$⊢ (B \in ℝ \land (n \in ℕ \land - B < n)) \to \forall z \in ℤ (B \leq z \to z \in ℤ_{\geq (- n)})$
24		rabss	$⊢ \{z \in ℤ \| B \leq z\} \subseteq ℤ_{\geq (- n)} \leftrightarrow \forall z \in ℤ (B \leq z \to z \in ℤ_{\geq (- n)})$
25	23 24	sylibr	$⊢ (B \in ℝ \land (n \in ℕ \land - B < n)) \to \{z \in ℤ \| B \leq z\} \subseteq ℤ_{\geq (- n)}$
26	25	adantlr	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to \{z \in ℤ \| B \leq z\} \subseteq ℤ_{\geq (- n)}$
27	5 26	sstrd	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to A \subseteq ℤ_{\geq (- n)}$
28		simplrr	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to A \neq \emptyset$
29		infssuzcl	$⊢ (A \subseteq ℤ_{\geq (- n)} \land A \neq \emptyset) \to inf (A ℝ <) \in A$
30	27 28 29	syl2anc	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to inf (A ℝ <) \in A$
31		infssuzle	$⊢ (A \subseteq ℤ_{\geq (- n)} \land y \in A) \to inf (A ℝ <) \leq y$
32	27 31	sylan	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land y \in A) \to inf (A ℝ <) \leq y$
33	32	ralrimiva	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to \forall y \in A inf (A ℝ <) \leq y$
34		breq2	$⊢ y = inf (A ℝ <) \to (x \leq y \leftrightarrow x \leq inf (A ℝ <))$
35		simprr	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to \forall y \in A x \leq y$
36	30	adantr	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to inf (A ℝ <) \in A$
37	34 35 36	rspcdva	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to x \leq inf (A ℝ <)$
38	27	adantr	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to A \subseteq ℤ_{\geq (- n)}$
39		simprl	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to x \in A$
40		infssuzle	$⊢ (A \subseteq ℤ_{\geq (- n)} \land x \in A) \to inf (A ℝ <) \leq x$
41	38 39 40	syl2anc	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to inf (A ℝ <) \leq x$
42		uzssz	$⊢ ℤ_{\geq (- n)} \subseteq ℤ$
43		zssre	$⊢ ℤ \subseteq ℝ$
44	42 43	sstri	$⊢ ℤ_{\geq (- n)} \subseteq ℝ$
45	27 44	sstrdi	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to A \subseteq ℝ$
46	45	adantr	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to A \subseteq ℝ$
47	46 39	sseldd	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to x \in ℝ$
48	45 30	sseldd	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to inf (A ℝ <) \in ℝ$
49	48	adantr	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to inf (A ℝ <) \in ℝ$
50	47 49	letri3d	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to (x = inf (A ℝ <) \leftrightarrow (x \leq inf (A ℝ <) \land inf (A ℝ <) \leq x))$
51	37 41 50	mpbir2and	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land (x \in A \land \forall y \in A x \leq y)) \to x = inf (A ℝ <)$
52	51	expr	$⊢ (((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \land x \in A) \to (\forall y \in A x \leq y \to x = inf (A ℝ <))$
53	52	ralrimiva	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to \forall x \in A (\forall y \in A x \leq y \to x = inf (A ℝ <))$
54		breq1	$⊢ x = inf (A ℝ <) \to (x \leq y \leftrightarrow inf (A ℝ <) \leq y)$
55	54	ralbidv	$⊢ x = inf (A ℝ <) \to (\forall y \in A x \leq y \leftrightarrow \forall y \in A inf (A ℝ <) \leq y)$
56	55	eqreu	$⊢ (inf (A ℝ <) \in A \land \forall y \in A inf (A ℝ <) \leq y \land \forall x \in A (\forall y \in A x \leq y \to x = inf (A ℝ <))) \to \exists! x \in A \forall y \in A x \leq y$
57	30 33 53 56	syl3anc	$⊢ ((B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \land (n \in ℕ \land - B < n)) \to \exists! x \in A \forall y \in A x \leq y$
58	4 57	rexlimddv	$⊢ (B \in ℝ \land (A \subseteq \{z \in ℤ \| B \leq z\} \land A \neq \emptyset)) \to \exists! x \in A \forall y \in A x \leq y$

Metamath Proof Explorer

Theorem uzwo3

Proof