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	\|- F/ j ps
	uzwo4.2	\|- ( j = k -> ( ph <-> ps ) )
Assertion	uzwo4	\|- ( ( S C_ ( ZZ>= ` M ) /\ E. j e. S ph ) -> E. j e. S ( ph /\ A. k e. S ( k < j -> -. ps ) ) )

Proof

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

Metamath Proof Explorer

Theorem uzwo4

Proof