Metamath Proof Explorer


Theorem 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 φ ψ
Assertion uzwo4 S M j S φ j S φ k S k < j ¬ ψ

Proof

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