uzwo

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005)

		Ref	Expression
	Assertion	uzwo	$⊢ (S \subseteq ℤ_{\geq M} \land S \neq \emptyset) \to \exists j \in S \forall k \in S j \leq k$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ h = M \to (h \leq t \leftrightarrow M \leq t)$
2	1	ralbidv	$⊢ h = M \to (\forall t \in S h \leq t \leftrightarrow \forall t \in S M \leq t)$
3	2	imbi2d	$⊢ h = M \to (((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S h \leq t) \leftrightarrow ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S M \leq t))$
4		breq1	$⊢ h = m \to (h \leq t \leftrightarrow m \leq t)$
5	4	ralbidv	$⊢ h = m \to (\forall t \in S h \leq t \leftrightarrow \forall t \in S m \leq t)$
6	5	imbi2d	$⊢ h = m \to (((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S h \leq t) \leftrightarrow ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S m \leq t))$
7		breq1	$⊢ h = m + 1 \to (h \leq t \leftrightarrow m + 1 \leq t)$
8	7	ralbidv	$⊢ h = m + 1 \to (\forall t \in S h \leq t \leftrightarrow \forall t \in S m + 1 \leq t)$
9	8	imbi2d	$⊢ h = m + 1 \to (((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S h \leq t) \leftrightarrow ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S m + 1 \leq t))$
10		breq1	$⊢ h = n \to (h \leq t \leftrightarrow n \leq t)$
11	10	ralbidv	$⊢ h = n \to (\forall t \in S h \leq t \leftrightarrow \forall t \in S n \leq t)$
12	11	imbi2d	$⊢ h = n \to (((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S h \leq t) \leftrightarrow ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S n \leq t))$
13		ssel	$⊢ S \subseteq ℤ_{\geq M} \to (t \in S \to t \in ℤ_{\geq M})$
14		eluzle	$⊢ t \in ℤ_{\geq M} \to M \leq t$
15	13 14	syl6	$⊢ S \subseteq ℤ_{\geq M} \to (t \in S \to M \leq t)$
16	15	ralrimiv	$⊢ S \subseteq ℤ_{\geq M} \to \forall t \in S M \leq t$
17	16	adantr	$⊢ (S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S M \leq t$
18		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
19		sstr	$⊢ (S \subseteq ℤ_{\geq M} \land ℤ_{\geq M} \subseteq ℤ) \to S \subseteq ℤ$
20	18 19	mpan2	$⊢ S \subseteq ℤ_{\geq M} \to S \subseteq ℤ$
21		eluzelz	$⊢ m \in ℤ_{\geq M} \to m \in ℤ$
22		breq1	$⊢ j = m \to (j \leq t \leftrightarrow m \leq t)$
23	22	ralbidv	$⊢ j = m \to (\forall t \in S j \leq t \leftrightarrow \forall t \in S m \leq t)$
24	23	rspcev	$⊢ (m \in S \land \forall t \in S m \leq t) \to \exists j \in S \forall t \in S j \leq t$
25	24	expcom	$⊢ \forall t \in S m \leq t \to (m \in S \to \exists j \in S \forall t \in S j \leq t)$
26	25	con3rr3	$⊢ \neg \exists j \in S \forall t \in S j \leq t \to (\forall t \in S m \leq t \to \neg m \in S)$
27		ssel2	$⊢ (S \subseteq ℤ \land t \in S) \to t \in ℤ$
28		zre	$⊢ m \in ℤ \to m \in ℝ$
29		zre	$⊢ t \in ℤ \to t \in ℝ$
30		letri3	$⊢ (m \in ℝ \land t \in ℝ) \to (m = t \leftrightarrow (m \leq t \land t \leq m))$
31	28 29 30	syl2an	$⊢ (m \in ℤ \land t \in ℤ) \to (m = t \leftrightarrow (m \leq t \land t \leq m))$
32		zleltp1	$⊢ (t \in ℤ \land m \in ℤ) \to (t \leq m \leftrightarrow t < m + 1)$
33		peano2re	$⊢ m \in ℝ \to m + 1 \in ℝ$
34	28 33	syl	$⊢ m \in ℤ \to m + 1 \in ℝ$
35		ltnle	$⊢ (t \in ℝ \land m + 1 \in ℝ) \to (t < m + 1 \leftrightarrow \neg m + 1 \leq t)$
36	29 34 35	syl2an	$⊢ (t \in ℤ \land m \in ℤ) \to (t < m + 1 \leftrightarrow \neg m + 1 \leq t)$
37	32 36	bitrd	$⊢ (t \in ℤ \land m \in ℤ) \to (t \leq m \leftrightarrow \neg m + 1 \leq t)$
38	37	ancoms	$⊢ (m \in ℤ \land t \in ℤ) \to (t \leq m \leftrightarrow \neg m + 1 \leq t)$
39	38	anbi2d	$⊢ (m \in ℤ \land t \in ℤ) \to ((m \leq t \land t \leq m) \leftrightarrow (m \leq t \land \neg m + 1 \leq t))$
40	31 39	bitrd	$⊢ (m \in ℤ \land t \in ℤ) \to (m = t \leftrightarrow (m \leq t \land \neg m + 1 \leq t))$
41	27 40	sylan2	$⊢ (m \in ℤ \land (S \subseteq ℤ \land t \in S)) \to (m = t \leftrightarrow (m \leq t \land \neg m + 1 \leq t))$
42		eleq1a	$⊢ t \in S \to (m = t \to m \in S)$
43	42	ad2antll	$⊢ (m \in ℤ \land (S \subseteq ℤ \land t \in S)) \to (m = t \to m \in S)$
44	41 43	sylbird	$⊢ (m \in ℤ \land (S \subseteq ℤ \land t \in S)) \to ((m \leq t \land \neg m + 1 \leq t) \to m \in S)$
45	44	expd	$⊢ (m \in ℤ \land (S \subseteq ℤ \land t \in S)) \to (m \leq t \to (\neg m + 1 \leq t \to m \in S))$
46		con1	$⊢ (\neg m + 1 \leq t \to m \in S) \to (\neg m \in S \to m + 1 \leq t)$
47	45 46	syl6	$⊢ (m \in ℤ \land (S \subseteq ℤ \land t \in S)) \to (m \leq t \to (\neg m \in S \to m + 1 \leq t))$
48	47	com23	$⊢ (m \in ℤ \land (S \subseteq ℤ \land t \in S)) \to (\neg m \in S \to (m \leq t \to m + 1 \leq t))$
49	48	exp32	$⊢ m \in ℤ \to (S \subseteq ℤ \to (t \in S \to (\neg m \in S \to (m \leq t \to m + 1 \leq t))))$
50	49	com34	$⊢ m \in ℤ \to (S \subseteq ℤ \to (\neg m \in S \to (t \in S \to (m \leq t \to m + 1 \leq t))))$
51	50	imp41	$⊢ (((m \in ℤ \land S \subseteq ℤ) \land \neg m \in S) \land t \in S) \to (m \leq t \to m + 1 \leq t)$
52	51	ralimdva	$⊢ ((m \in ℤ \land S \subseteq ℤ) \land \neg m \in S) \to (\forall t \in S m \leq t \to \forall t \in S m + 1 \leq t)$
53	52	ex	$⊢ (m \in ℤ \land S \subseteq ℤ) \to (\neg m \in S \to (\forall t \in S m \leq t \to \forall t \in S m + 1 \leq t))$
54	26 53	sylan9r	$⊢ ((m \in ℤ \land S \subseteq ℤ) \land \neg \exists j \in S \forall t \in S j \leq t) \to (\forall t \in S m \leq t \to (\forall t \in S m \leq t \to \forall t \in S m + 1 \leq t))$
55	54	pm2.43d	$⊢ ((m \in ℤ \land S \subseteq ℤ) \land \neg \exists j \in S \forall t \in S j \leq t) \to (\forall t \in S m \leq t \to \forall t \in S m + 1 \leq t)$
56	55	expl	$⊢ m \in ℤ \to ((S \subseteq ℤ \land \neg \exists j \in S \forall t \in S j \leq t) \to (\forall t \in S m \leq t \to \forall t \in S m + 1 \leq t))$
57	21 56	syl	$⊢ m \in ℤ_{\geq M} \to ((S \subseteq ℤ \land \neg \exists j \in S \forall t \in S j \leq t) \to (\forall t \in S m \leq t \to \forall t \in S m + 1 \leq t))$
58	20 57	sylani	$⊢ m \in ℤ_{\geq M} \to ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to (\forall t \in S m \leq t \to \forall t \in S m + 1 \leq t))$
59	58	a2d	$⊢ m \in ℤ_{\geq M} \to (((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S m \leq t) \to ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S m + 1 \leq t))$
60	3 6 9 12 17 59	uzind4i	$⊢ n \in ℤ_{\geq M} \to ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \forall t \in S n \leq t)$
61		breq1	$⊢ j = n \to (j \leq t \leftrightarrow n \leq t)$
62	61	ralbidv	$⊢ j = n \to (\forall t \in S j \leq t \leftrightarrow \forall t \in S n \leq t)$
63	62	rspcev	$⊢ (n \in S \land \forall t \in S n \leq t) \to \exists j \in S \forall t \in S j \leq t$
64	63	expcom	$⊢ \forall t \in S n \leq t \to (n \in S \to \exists j \in S \forall t \in S j \leq t)$
65	64	con3rr3	$⊢ \neg \exists j \in S \forall t \in S j \leq t \to (\forall t \in S n \leq t \to \neg n \in S)$
66	65	adantl	$⊢ (S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to (\forall t \in S n \leq t \to \neg n \in S)$
67	60 66	sylcom	$⊢ n \in ℤ_{\geq M} \to ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \neg n \in S)$
68		ssel	$⊢ S \subseteq ℤ_{\geq M} \to (n \in S \to n \in ℤ_{\geq M})$
69	68	con3rr3	$⊢ \neg n \in ℤ_{\geq M} \to (S \subseteq ℤ_{\geq M} \to \neg n \in S)$
70	69	adantrd	$⊢ \neg n \in ℤ_{\geq M} \to ((S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \neg n \in S)$
71	67 70	pm2.61i	$⊢ (S \subseteq ℤ_{\geq M} \land \neg \exists j \in S \forall t \in S j \leq t) \to \neg n \in S$
72	71	ex	$⊢ S \subseteq ℤ_{\geq M} \to (\neg \exists j \in S \forall t \in S j \leq t \to \neg n \in S)$
73	72	alrimdv	$⊢ S \subseteq ℤ_{\geq M} \to (\neg \exists j \in S \forall t \in S j \leq t \to \forall n \neg n \in S)$
74		eq0	$⊢ S = \emptyset \leftrightarrow \forall n \neg n \in S$
75	73 74	syl6ibr	$⊢ S \subseteq ℤ_{\geq M} \to (\neg \exists j \in S \forall t \in S j \leq t \to S = \emptyset)$
76	75	necon1ad	$⊢ S \subseteq ℤ_{\geq M} \to (S \neq \emptyset \to \exists j \in S \forall t \in S j \leq t)$
77	76	imp	$⊢ (S \subseteq ℤ_{\geq M} \land S \neq \emptyset) \to \exists j \in S \forall t \in S j \leq t$
78		breq2	$⊢ t = k \to (j \leq t \leftrightarrow j \leq k)$
79	78	cbvralvw	$⊢ \forall t \in S j \leq t \leftrightarrow \forall k \in S j \leq k$
80	79	rexbii	$⊢ \exists j \in S \forall t \in S j \leq t \leftrightarrow \exists j \in S \forall k \in S j \leq k$
81	77 80	sylib	$⊢ (S \subseteq ℤ_{\geq M} \land S \neq \emptyset) \to \exists j \in S \forall k \in S j \leq k$

Metamath Proof Explorer

Theorem uzwo

Proof