uzwo4

Description: Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	uzwo4.1	$⊢ Ⅎ j ψ$
	uzwo4.2	$⊢ j = k \to (φ \leftrightarrow ψ)$
Assertion	uzwo4	$⊢ (S \subseteq ℤ_{\geq M} \land \exists j \in S φ) \to \exists j \in S (φ \land \forall k \in S (k < j \to \neg ψ))$

Proof

Step	Hyp	Ref	Expression
1		uzwo4.1	$⊢ Ⅎ j ψ$
2		uzwo4.2	$⊢ j = k \to (φ \leftrightarrow ψ)$
3		ssrab2	$⊢ \{j \in S \| φ\} \subseteq S$
4	3	a1i	$⊢ S \subseteq ℤ_{\geq M} \to \{j \in S \| φ\} \subseteq S$
5		id	$⊢ S \subseteq ℤ_{\geq M} \to S \subseteq ℤ_{\geq M}$
6	4 5	sstrd	$⊢ S \subseteq ℤ_{\geq M} \to \{j \in S \| φ\} \subseteq ℤ_{\geq M}$
7	6	adantr	$⊢ (S \subseteq ℤ_{\geq M} \land \exists j \in S φ) \to \{j \in S \| φ\} \subseteq ℤ_{\geq M}$
8		rabn0	$⊢ \{j \in S \| φ\} \neq \emptyset \leftrightarrow \exists j \in S φ$
9	8	bicomi	$⊢ \exists j \in S φ \leftrightarrow \{j \in S \| φ\} \neq \emptyset$
10	9	biimpi	$⊢ \exists j \in S φ \to \{j \in S \| φ\} \neq \emptyset$
11	10	adantl	$⊢ (S \subseteq ℤ_{\geq M} \land \exists j \in S φ) \to \{j \in S \| φ\} \neq \emptyset$
12		uzwo	$⊢ (\{j \in S \| φ\} \subseteq ℤ_{\geq M} \land \{j \in S \| φ\} \neq \emptyset) \to \exists i \in \{j \in S \| φ\} \forall k \in \{j \in S \| φ\} i \leq k$
13	7 11 12	syl2anc	$⊢ (S \subseteq ℤ_{\geq M} \land \exists j \in S φ) \to \exists i \in \{j \in S \| φ\} \forall k \in \{j \in S \| φ\} i \leq k$
14	3	sseli	$⊢ i \in \{j \in S \| φ\} \to i \in S$
15	14	adantr	$⊢ (i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to i \in S$
16	15	3adant1	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to i \in S$
17		nfcv	$⊢ \underline{Ⅎ} j i$
18		nfcv	$⊢ \underline{Ⅎ} j S$
19	17	nfsbc1	$⊢ Ⅎ j \underset{˙}{[} i / j \underset{˙}{]} φ$
20		sbceq1a	$⊢ j = i \to (φ \leftrightarrow \underset{˙}{[} i / j \underset{˙}{]} φ)$
21	17 18 19 20	elrabf	$⊢ i \in \{j \in S \| φ\} \leftrightarrow (i \in S \land \underset{˙}{[} i / j \underset{˙}{]} φ)$
22	21	biimpi	$⊢ i \in \{j \in S \| φ\} \to (i \in S \land \underset{˙}{[} i / j \underset{˙}{]} φ)$
23	22	simprd	$⊢ i \in \{j \in S \| φ\} \to \underset{˙}{[} i / j \underset{˙}{]} φ$
24	23	adantr	$⊢ (i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to \underset{˙}{[} i / j \underset{˙}{]} φ$
25	24	3adant1	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to \underset{˙}{[} i / j \underset{˙}{]} φ$
26		nfv	$⊢ Ⅎ k S \subseteq ℤ_{\geq M}$
27		nfv	$⊢ Ⅎ k i \in \{j \in S \| φ\}$
28		nfra1	$⊢ Ⅎ k \forall k \in \{j \in S \| φ\} i \leq k$
29	26 27 28	nf3an	$⊢ Ⅎ k (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k)$
30		simpl13	$⊢ (((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \land ψ) \to \forall k \in \{j \in S \| φ\} i \leq k$
31		simpl2	$⊢ (((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \land ψ) \to k \in S$
32		simpr	$⊢ (((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \land ψ) \to ψ$
33		simpll	$⊢ ((\forall k \in \{j \in S \| φ\} i \leq k \land k \in S) \land ψ) \to \forall k \in \{j \in S \| φ\} i \leq k$
34		id	$⊢ (k \in S \land ψ) \to (k \in S \land ψ)$
35		nfcv	$⊢ \underline{Ⅎ} j k$
36	35 18 1 2	elrabf	$⊢ k \in \{j \in S \| φ\} \leftrightarrow (k \in S \land ψ)$
37	34 36	sylibr	$⊢ (k \in S \land ψ) \to k \in \{j \in S \| φ\}$
38	37	adantll	$⊢ ((\forall k \in \{j \in S \| φ\} i \leq k \land k \in S) \land ψ) \to k \in \{j \in S \| φ\}$
39		rspa	$⊢ (\forall k \in \{j \in S \| φ\} i \leq k \land k \in \{j \in S \| φ\}) \to i \leq k$
40	33 38 39	syl2anc	$⊢ ((\forall k \in \{j \in S \| φ\} i \leq k \land k \in S) \land ψ) \to i \leq k$
41	30 31 32 40	syl21anc	$⊢ (((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \land ψ) \to i \leq k$
42	6	sselda	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\}) \to i \in ℤ_{\geq M}$
43		eluzelz	$⊢ i \in ℤ_{\geq M} \to i \in ℤ$
44	42 43	syl	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\}) \to i \in ℤ$
45	44	zred	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\}) \to i \in ℝ$
46	45	3adant3	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to i \in ℝ$
47	46	3ad2ant1	$⊢ ((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \to i \in ℝ$
48		ssel2	$⊢ (S \subseteq ℤ_{\geq M} \land k \in S) \to k \in ℤ_{\geq M}$
49		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
50	48 49	syl	$⊢ (S \subseteq ℤ_{\geq M} \land k \in S) \to k \in ℤ$
51	50	zred	$⊢ (S \subseteq ℤ_{\geq M} \land k \in S) \to k \in ℝ$
52	51	3ad2antl1	$⊢ ((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S) \to k \in ℝ$
53	52	3adant3	$⊢ ((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \to k \in ℝ$
54		simp3	$⊢ ((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \to k < i$
55		simp3	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to k < i$
56		simp2	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to k \in ℝ$
57		simp1	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to i \in ℝ$
58	56 57	ltnled	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to (k < i \leftrightarrow \neg i \leq k)$
59	55 58	mpbid	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to \neg i \leq k$
60	47 53 54 59	syl3anc	$⊢ ((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \to \neg i \leq k$
61	60	adantr	$⊢ (((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \land ψ) \to \neg i \leq k$
62	41 61	pm2.65da	$⊢ ((S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \land k \in S \land k < i) \to \neg ψ$
63	62	3exp	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to (k \in S \to (k < i \to \neg ψ))$
64	29 63	ralrimi	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to \forall k \in S (k < i \to \neg ψ)$
65	25 64	jca	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to (\underset{˙}{[} i / j \underset{˙}{]} φ \land \forall k \in S (k < i \to \neg ψ))$
66		nfv	$⊢ Ⅎ j k < i$
67	1	nfn	$⊢ Ⅎ j \neg ψ$
68	66 67	nfim	$⊢ Ⅎ j (k < i \to \neg ψ)$
69	18 68	nfralw	$⊢ Ⅎ j \forall k \in S (k < i \to \neg ψ)$
70	19 69	nfan	$⊢ Ⅎ j (\underset{˙}{[} i / j \underset{˙}{]} φ \land \forall k \in S (k < i \to \neg ψ))$
71		breq2	$⊢ j = i \to (k < j \leftrightarrow k < i)$
72	71	imbi1d	$⊢ j = i \to ((k < j \to \neg ψ) \leftrightarrow (k < i \to \neg ψ))$
73	72	ralbidv	$⊢ j = i \to (\forall k \in S (k < j \to \neg ψ) \leftrightarrow \forall k \in S (k < i \to \neg ψ))$
74	20 73	anbi12d	$⊢ j = i \to ((φ \land \forall k \in S (k < j \to \neg ψ)) \leftrightarrow (\underset{˙}{[} i / j \underset{˙}{]} φ \land \forall k \in S (k < i \to \neg ψ)))$
75	70 74	rspce	$⊢ (i \in S \land (\underset{˙}{[} i / j \underset{˙}{]} φ \land \forall k \in S (k < i \to \neg ψ))) \to \exists j \in S (φ \land \forall k \in S (k < j \to \neg ψ))$
76	16 65 75	syl2anc	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to \exists j \in S (φ \land \forall k \in S (k < j \to \neg ψ))$
77	76	3exp	$⊢ S \subseteq ℤ_{\geq M} \to (i \in \{j \in S \| φ\} \to (\forall k \in \{j \in S \| φ\} i \leq k \to \exists j \in S (φ \land \forall k \in S (k < j \to \neg ψ))))$
78	77	rexlimdv	$⊢ S \subseteq ℤ_{\geq M} \to (\exists i \in \{j \in S \| φ\} \forall k \in \{j \in S \| φ\} i \leq k \to \exists j \in S (φ \land \forall k \in S (k < j \to \neg ψ)))$
79	78	adantr	$⊢ (S \subseteq ℤ_{\geq M} \land \exists j \in S φ) \to (\exists i \in \{j \in S \| φ\} \forall k \in \{j \in S \| φ\} i \leq k \to \exists j \in S (φ \land \forall k \in S (k < j \to \neg ψ)))$
80	13 79	mpd	$⊢ (S \subseteq ℤ_{\geq M} \land \exists j \in S φ) \to \exists j \in S (φ \land \forall k \in S (k < j \to \neg ψ))$

Metamath Proof Explorer

Theorem uzwo4

Proof