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	bilanri	$⊢ (S \subseteq ℤ_{\geq M} \land \exists j \in S φ) \to \{j \in S \| φ\} \neq \emptyset$
10		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$
11	7 9 10	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$
12	3	sseli	$⊢ i \in \{j \in S \| φ\} \to i \in S$
13	12	adantr	$⊢ (i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to i \in S$
14	13	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$
15		nfcv	$⊢ \underline{Ⅎ} j i$
16		nfcv	$⊢ \underline{Ⅎ} j S$
17	15	nfsbc1	$⊢ Ⅎ j \underset{˙}{[} i / j \underset{˙}{]} φ$
18		sbceq1a	$⊢ j = i \to (φ \leftrightarrow \underset{˙}{[} i / j \underset{˙}{]} φ)$
19	15 16 17 18	elrabf	$⊢ i \in \{j \in S \| φ\} \leftrightarrow (i \in S \land \underset{˙}{[} i / j \underset{˙}{]} φ)$
20	19	biimpi	$⊢ i \in \{j \in S \| φ\} \to (i \in S \land \underset{˙}{[} i / j \underset{˙}{]} φ)$
21	20	simprd	$⊢ i \in \{j \in S \| φ\} \to \underset{˙}{[} i / j \underset{˙}{]} φ$
22	21	adantr	$⊢ (i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to \underset{˙}{[} i / j \underset{˙}{]} φ$
23	22	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{˙}{]} φ$
24		nfv	$⊢ Ⅎ k S \subseteq ℤ_{\geq M}$
25		nfv	$⊢ Ⅎ k i \in \{j \in S \| φ\}$
26		nfra1	$⊢ Ⅎ k \forall k \in \{j \in S \| φ\} i \leq k$
27	24 25 26	nf3an	$⊢ Ⅎ k (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k)$
28		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$
29		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$
30		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 ψ$
31		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$
32		id	$⊢ (k \in S \land ψ) \to (k \in S \land ψ)$
33		nfcv	$⊢ \underline{Ⅎ} j k$
34	33 16 1 2	elrabf	$⊢ k \in \{j \in S \| φ\} \leftrightarrow (k \in S \land ψ)$
35	32 34	sylibr	$⊢ (k \in S \land ψ) \to k \in \{j \in S \| φ\}$
36	35	adantll	$⊢ ((\forall k \in \{j \in S \| φ\} i \leq k \land k \in S) \land ψ) \to k \in \{j \in S \| φ\}$
37		rspa	$⊢ (\forall k \in \{j \in S \| φ\} i \leq k \land k \in \{j \in S \| φ\}) \to i \leq k$
38	31 36 37	syl2anc	$⊢ ((\forall k \in \{j \in S \| φ\} i \leq k \land k \in S) \land ψ) \to i \leq k$
39	28 29 30 38	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$
40	6	sselda	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\}) \to i \in ℤ_{\geq M}$
41		eluzelz	$⊢ i \in ℤ_{\geq M} \to i \in ℤ$
42	40 41	syl	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\}) \to i \in ℤ$
43	42	zred	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\}) \to i \in ℝ$
44	43	3adant3	$⊢ (S \subseteq ℤ_{\geq M} \land i \in \{j \in S \| φ\} \land \forall k \in \{j \in S \| φ\} i \leq k) \to i \in ℝ$
45	44	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 ℝ$
46		ssel2	$⊢ (S \subseteq ℤ_{\geq M} \land k \in S) \to k \in ℤ_{\geq M}$
47		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
48	46 47	syl	$⊢ (S \subseteq ℤ_{\geq M} \land k \in S) \to k \in ℤ$
49	48	zred	$⊢ (S \subseteq ℤ_{\geq M} \land k \in S) \to k \in ℝ$
50	49	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 ℝ$
51	50	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 ℝ$
52		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$
53		simp3	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to k < i$
54		simp2	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to k \in ℝ$
55		simp1	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to i \in ℝ$
56	54 55	ltnled	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to (k < i \leftrightarrow \neg i \leq k)$
57	53 56	mpbid	$⊢ (i \in ℝ \land k \in ℝ \land k < i) \to \neg i \leq k$
58	45 51 52 57	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$
59	58	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$
60	39 59	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 ψ$
61	60	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 ψ))$
62	27 61	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 ψ)$
63	23 62	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 ψ))$
64		nfv	$⊢ Ⅎ j k < i$
65	1	nfn	$⊢ Ⅎ j \neg ψ$
66	64 65	nfim	$⊢ Ⅎ j (k < i \to \neg ψ)$
67	16 66	nfralw	$⊢ Ⅎ j \forall k \in S (k < i \to \neg ψ)$
68	17 67	nfan	$⊢ Ⅎ j (\underset{˙}{[} i / j \underset{˙}{]} φ \land \forall k \in S (k < i \to \neg ψ))$
69		breq2	$⊢ j = i \to (k < j \leftrightarrow k < i)$
70	69	imbi1d	$⊢ j = i \to ((k < j \to \neg ψ) \leftrightarrow (k < i \to \neg ψ))$
71	70	ralbidv	$⊢ j = i \to (\forall k \in S (k < j \to \neg ψ) \leftrightarrow \forall k \in S (k < i \to \neg ψ))$
72	18 71	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 ψ)))$
73	68 72	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 ψ))$
74	14 63 73	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 ψ))$
75	74	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 ψ))))$
76	75	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 ψ)))$
77	76	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 ψ)))$
78	11 77	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