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 𝑗 𝜓
uzwo4.2 ( 𝑗 = 𝑘 → ( 𝜑𝜓 ) )
Assertion uzwo4 ( ( 𝑆 ⊆ ( ℤ𝑀 ) ∧ ∃ 𝑗𝑆 𝜑 ) → ∃ 𝑗𝑆 ( 𝜑 ∧ ∀ 𝑘𝑆 ( 𝑘 < 𝑗 → ¬ 𝜓 ) ) )

Proof

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