Metamath Proof Explorer

Theorem uzwo3

Description: Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 allows the lower bound B to be any real number. See also nnwo and nnwos . (Contributed by NM, 12-Nov-2004) (Proof shortened by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Assertion uzwo3 ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )

Proof

Step Hyp Ref Expression
1 renegcl ⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
2 1 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) → - 𝐵 ∈ ℝ )
3 arch ⊢ ( - 𝐵 ∈ ℝ → ∃ 𝑛 ∈ ℕ - 𝐵 < 𝑛 )
4 2 3 syl ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) → ∃ 𝑛 ∈ ℕ - 𝐵 < 𝑛 )
5 simplrl ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } )
6 simplrl ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → 𝑛 ∈ ℕ )
7 nnnegz ⊢ ( 𝑛 ∈ ℕ → - 𝑛 ∈ ℤ )
8 6 7 syl ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → - 𝑛 ∈ ℤ )
9 8 zred ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → - 𝑛 ∈ ℝ )
10 simprl ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → 𝑧 ∈ ℤ )
11 10 zred ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → 𝑧 ∈ ℝ )
12 simpll ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → 𝐵 ∈ ℝ )
13 6 nnred ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → 𝑛 ∈ ℝ )
14 simplrr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → - 𝐵 < 𝑛 )
15 12 13 14 ltnegcon1d ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → - 𝑛 < 𝐵 )
16 simprr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → 𝐵 ≤ 𝑧 )
17 9 12 11 15 16 ltletrd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → - 𝑛 < 𝑧 )
18 9 11 17 ltled ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → - 𝑛 ≤ 𝑧 )
19 eluz ⊢ ( ( - 𝑛 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ∈ ( ℤ≥ ‘ - 𝑛 ) ↔ - 𝑛 ≤ 𝑧 ) )
20 8 10 19 syl2anc ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → ( 𝑧 ∈ ( ℤ≥ ‘ - 𝑛 ) ↔ - 𝑛 ≤ 𝑧 ) )
21 18 20 mpbird ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑧 ∈ ℤ ∧ 𝐵 ≤ 𝑧 ) ) → 𝑧 ∈ ( ℤ≥ ‘ - 𝑛 ) )
22 21 expr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ 𝑧 ∈ ℤ ) → ( 𝐵 ≤ 𝑧 → 𝑧 ∈ ( ℤ≥ ‘ - 𝑛 ) ) )
23 22 ralrimiva ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → ∀ 𝑧 ∈ ℤ ( 𝐵 ≤ 𝑧 → 𝑧 ∈ ( ℤ≥ ‘ - 𝑛 ) ) )
24 rabss ⊢ ( { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ⊆ ( ℤ≥ ‘ - 𝑛 ) ↔ ∀ 𝑧 ∈ ℤ ( 𝐵 ≤ 𝑧 → 𝑧 ∈ ( ℤ≥ ‘ - 𝑛 ) ) )
25 23 24 sylibr ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ⊆ ( ℤ≥ ‘ - 𝑛 ) )
26 25 adantlr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ⊆ ( ℤ≥ ‘ - 𝑛 ) )
27 5 26 sstrd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → 𝐴 ⊆ ( ℤ≥ ‘ - 𝑛 ) )
28 simplrr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → 𝐴 ≠ ∅ )
29 infssuzcl ⊢ ( ( 𝐴 ⊆ ( ℤ≥ ‘ - 𝑛 ) ∧ 𝐴 ≠ ∅ ) → inf ( 𝐴 , ℝ , < ) ∈ 𝐴 )
30 27 28 29 syl2anc ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → inf ( 𝐴 , ℝ , < ) ∈ 𝐴 )
31 infssuzle ⊢ ( ( 𝐴 ⊆ ( ℤ≥ ‘ - 𝑛 ) ∧ 𝑦 ∈ 𝐴 ) → inf ( 𝐴 , ℝ , < ) ≤ 𝑦 )
32 27 31 sylan ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ 𝑦 ∈ 𝐴 ) → inf ( 𝐴 , ℝ , < ) ≤ 𝑦 )
33 32 ralrimiva ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → ∀ 𝑦 ∈ 𝐴 inf ( 𝐴 , ℝ , < ) ≤ 𝑦 )
34 breq2 ⊢ ( 𝑦 = inf ( 𝐴 , ℝ , < ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ≤ inf ( 𝐴 , ℝ , < ) ) )
35 simprr ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
36 30 adantr ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → inf ( 𝐴 , ℝ , < ) ∈ 𝐴 )
37 34 35 36 rspcdva ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → 𝑥 ≤ inf ( 𝐴 , ℝ , < ) )
38 27 adantr ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → 𝐴 ⊆ ( ℤ≥ ‘ - 𝑛 ) )
39 simprl ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → 𝑥 ∈ 𝐴 )
40 infssuzle ⊢ ( ( 𝐴 ⊆ ( ℤ≥ ‘ - 𝑛 ) ∧ 𝑥 ∈ 𝐴 ) → inf ( 𝐴 , ℝ , < ) ≤ 𝑥 )
41 38 39 40 syl2anc ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → inf ( 𝐴 , ℝ , < ) ≤ 𝑥 )
42 uzssz ⊢ ( ℤ≥ ‘ - 𝑛 ) ⊆ ℤ
43 zssre ⊢ ℤ ⊆ ℝ
44 42 43 sstri ⊢ ( ℤ≥ ‘ - 𝑛 ) ⊆ ℝ
45 27 44 sstrdi ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → 𝐴 ⊆ ℝ )
46 45 adantr ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → 𝐴 ⊆ ℝ )
47 46 39 sseldd ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → 𝑥 ∈ ℝ )
48 45 30 sseldd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ )
49 48 adantr ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ )
50 47 49 letri3d ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → ( 𝑥 = inf ( 𝐴 , ℝ , < ) ↔ ( 𝑥 ≤ inf ( 𝐴 , ℝ , < ) ∧ inf ( 𝐴 , ℝ , < ) ≤ 𝑥 ) ) )
51 37 41 50 mpbir2and ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) ) → 𝑥 = inf ( 𝐴 , ℝ , < ) )
52 51 expr ⊢ ( ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → 𝑥 = inf ( 𝐴 , ℝ , < ) ) )
53 52 ralrimiva ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → 𝑥 = inf ( 𝐴 , ℝ , < ) ) )
54 breq1 ⊢ ( 𝑥 = inf ( 𝐴 , ℝ , < ) → ( 𝑥 ≤ 𝑦 ↔ inf ( 𝐴 , ℝ , < ) ≤ 𝑦 ) )
55 54 ralbidv ⊢ ( 𝑥 = inf ( 𝐴 , ℝ , < ) → ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 inf ( 𝐴 , ℝ , < ) ≤ 𝑦 ) )
56 55 eqreu ⊢ ( ( inf ( 𝐴 , ℝ , < ) ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 inf ( 𝐴 , ℝ , < ) ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 → 𝑥 = inf ( 𝐴 , ℝ , < ) ) ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
57 30 33 53 56 syl3anc ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) ∧ ( 𝑛 ∈ ℕ ∧ - 𝐵 < 𝑛 ) ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
58 4 57 rexlimddv ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ⊆ { 𝑧 ∈ ℤ ∣ 𝐵 ≤ 𝑧 } ∧ 𝐴 ≠ ∅ ) ) → ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )