suprfinzcl

Description: The supremum of a nonempty finite set of integers is a member of the set. (Contributed by AV, 1-Oct-2019)

		Ref	Expression
	Assertion	suprfinzcl	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to sup (A ℝ <) \in A$

Proof

Step	Hyp	Ref	Expression
1		zssre	$⊢ ℤ \subseteq ℝ$
2		ltso	$⊢ < Or ℝ$
3		soss	$⊢ ℤ \subseteq ℝ \to (< Or ℝ \to < Or ℤ)$
4	1 2 3	mp2	$⊢ < Or ℤ$
5	4	a1i	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to < Or ℤ$
6		simp3	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to A \in Fin$
7		simp2	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to A \neq \emptyset$
8		simp1	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to A \subseteq ℤ$
9		fisup2g	$⊢ (< Or ℤ \land (A \in Fin \land A \neq \emptyset \land A \subseteq ℤ)) \to \exists r \in A (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b))$
10	5 6 7 8 9	syl13anc	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to \exists r \in A (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b))$
11		id	$⊢ A \subseteq ℤ \to A \subseteq ℤ$
12	11 1	sstrdi	$⊢ A \subseteq ℤ \to A \subseteq ℝ$
13	12	3ad2ant1	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to A \subseteq ℝ$
14		ssrexv	$⊢ A \subseteq ℝ \to (\exists r \in A (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b)) \to \exists r \in ℝ (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b)))$
15	13 14	syl	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to (\exists r \in A (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b)) \to \exists r \in ℝ (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b)))$
16		ssel2	$⊢ (A \subseteq ℤ \land a \in A) \to a \in ℤ$
17	16	zred	$⊢ (A \subseteq ℤ \land a \in A) \to a \in ℝ$
18	17	ex	$⊢ A \subseteq ℤ \to (a \in A \to a \in ℝ)$
19	18	3ad2ant1	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to (a \in A \to a \in ℝ)$
20	19	adantr	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \to (a \in A \to a \in ℝ)$
21	20	imp	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \land a \in A) \to a \in ℝ$
22		simplr	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \land a \in A) \to r \in ℝ$
23	21 22	lenltd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \land a \in A) \to (a \leq r \leftrightarrow \neg r < a)$
24	23	bicomd	$⊢ (((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \land a \in A) \to (\neg r < a \leftrightarrow a \leq r)$
25	24	ralbidva	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \to (\forall a \in A \neg r < a \leftrightarrow \forall a \in A a \leq r)$
26	25	biimpd	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \to (\forall a \in A \neg r < a \to \forall a \in A a \leq r)$
27	26	adantrd	$⊢ ((A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \land r \in ℝ) \to ((\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b)) \to \forall a \in A a \leq r)$
28	27	reximdva	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to (\exists r \in ℝ (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b)) \to \exists r \in ℝ \forall a \in A a \leq r)$
29	15 28	syld	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to (\exists r \in A (\forall a \in A \neg r < a \land \forall a \in ℤ (a < r \to \exists b \in A a < b)) \to \exists r \in ℝ \forall a \in A a \leq r)$
30	10 29	mpd	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to \exists r \in ℝ \forall a \in A a \leq r$
31		suprzcl	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land \exists r \in ℝ \forall a \in A a \leq r) \to sup (A ℝ <) \in A$
32	30 31	syld3an3	$⊢ (A \subseteq ℤ \land A \neq \emptyset \land A \in Fin) \to sup (A ℝ <) \in A$

Metamath Proof Explorer

Theorem suprfinzcl

Proof