Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uzwo3 Structured version   Visualization version   GIF version

Theorem uzwo3 11974
 Description: Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 11943 allows the lower bound 𝐵 to be any real number. See also nnwo 11944 and nnwos 11946. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.)
Assertion
Ref Expression
uzwo3 ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥𝐴𝑦𝐴 𝑥𝑦)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧

Proof of Theorem uzwo3
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 renegcl 10534 . . . 4 (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
21adantr 472 . . 3 ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) → -𝐵 ∈ ℝ)
3 arch 11479 . . 3 (-𝐵 ∈ ℝ → ∃𝑛 ∈ ℕ -𝐵 < 𝑛)
42, 3syl 17 . 2 ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) → ∃𝑛 ∈ ℕ -𝐵 < 𝑛)
5 simplrl 819 . . . . 5 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧})
6 simplrl 819 . . . . . . . . . . . . 13 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑛 ∈ ℕ)
7 nnnegz 11570 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → -𝑛 ∈ ℤ)
86, 7syl 17 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 ∈ ℤ)
98zred 11672 . . . . . . . . . . 11 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 ∈ ℝ)
10 simprl 811 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑧 ∈ ℤ)
1110zred 11672 . . . . . . . . . . 11 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑧 ∈ ℝ)
12 simpll 807 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝐵 ∈ ℝ)
136nnred 11225 . . . . . . . . . . . . 13 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑛 ∈ ℝ)
14 simplrr 820 . . . . . . . . . . . . 13 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝐵 < 𝑛)
1512, 13, 14ltnegcon1d 10797 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 < 𝐵)
16 simprr 813 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝐵𝑧)
179, 12, 11, 15, 16ltletrd 10387 . . . . . . . . . . 11 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 < 𝑧)
189, 11, 17ltled 10375 . . . . . . . . . 10 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛𝑧)
19 eluz 11891 . . . . . . . . . . 11 ((-𝑛 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑧 ∈ (ℤ‘-𝑛) ↔ -𝑛𝑧))
208, 10, 19syl2anc 696 . . . . . . . . . 10 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → (𝑧 ∈ (ℤ‘-𝑛) ↔ -𝑛𝑧))
2118, 20mpbird 247 . . . . . . . . 9 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑧 ∈ (ℤ‘-𝑛))
2221expr 644 . . . . . . . 8 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ 𝑧 ∈ ℤ) → (𝐵𝑧𝑧 ∈ (ℤ‘-𝑛)))
2322ralrimiva 3102 . . . . . . 7 ((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∀𝑧 ∈ ℤ (𝐵𝑧𝑧 ∈ (ℤ‘-𝑛)))
24 rabss 3818 . . . . . . 7 ({𝑧 ∈ ℤ ∣ 𝐵𝑧} ⊆ (ℤ‘-𝑛) ↔ ∀𝑧 ∈ ℤ (𝐵𝑧𝑧 ∈ (ℤ‘-𝑛)))
2523, 24sylibr 224 . . . . . 6 ((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → {𝑧 ∈ ℤ ∣ 𝐵𝑧} ⊆ (ℤ‘-𝑛))
2625adantlr 753 . . . . 5 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → {𝑧 ∈ ℤ ∣ 𝐵𝑧} ⊆ (ℤ‘-𝑛))
275, 26sstrd 3752 . . . 4 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ⊆ (ℤ‘-𝑛))
28 simplrr 820 . . . 4 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ≠ ∅)
29 infssuzcl 11963 . . . 4 ((𝐴 ⊆ (ℤ‘-𝑛) ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ, < ) ∈ 𝐴)
3027, 28, 29syl2anc 696 . . 3 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → inf(𝐴, ℝ, < ) ∈ 𝐴)
31 infssuzle 11962 . . . . 5 ((𝐴 ⊆ (ℤ‘-𝑛) ∧ 𝑦𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑦)
3227, 31sylan 489 . . . 4 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ 𝑦𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑦)
3332ralrimiva 3102 . . 3 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∀𝑦𝐴 inf(𝐴, ℝ, < ) ≤ 𝑦)
3430adantr 472 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → inf(𝐴, ℝ, < ) ∈ 𝐴)
35 simprr 813 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → ∀𝑦𝐴 𝑥𝑦)
36 breq2 4806 . . . . . . . 8 (𝑦 = inf(𝐴, ℝ, < ) → (𝑥𝑦𝑥 ≤ inf(𝐴, ℝ, < )))
3736rspcv 3443 . . . . . . 7 (inf(𝐴, ℝ, < ) ∈ 𝐴 → (∀𝑦𝐴 𝑥𝑦𝑥 ≤ inf(𝐴, ℝ, < )))
3834, 35, 37sylc 65 . . . . . 6 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥 ≤ inf(𝐴, ℝ, < ))
3927adantr 472 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝐴 ⊆ (ℤ‘-𝑛))
40 simprl 811 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥𝐴)
41 infssuzle 11962 . . . . . . 7 ((𝐴 ⊆ (ℤ‘-𝑛) ∧ 𝑥𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑥)
4239, 40, 41syl2anc 696 . . . . . 6 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → inf(𝐴, ℝ, < ) ≤ 𝑥)
43 uzssz 11897 . . . . . . . . . . 11 (ℤ‘-𝑛) ⊆ ℤ
44 zssre 11574 . . . . . . . . . . 11 ℤ ⊆ ℝ
4543, 44sstri 3751 . . . . . . . . . 10 (ℤ‘-𝑛) ⊆ ℝ
4627, 45syl6ss 3754 . . . . . . . . 9 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ⊆ ℝ)
4746adantr 472 . . . . . . . 8 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝐴 ⊆ ℝ)
4847, 40sseldd 3743 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥 ∈ ℝ)
4946, 30sseldd 3743 . . . . . . . 8 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → inf(𝐴, ℝ, < ) ∈ ℝ)
5049adantr 472 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → inf(𝐴, ℝ, < ) ∈ ℝ)
5148, 50letri3d 10369 . . . . . 6 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → (𝑥 = inf(𝐴, ℝ, < ) ↔ (𝑥 ≤ inf(𝐴, ℝ, < ) ∧ inf(𝐴, ℝ, < ) ≤ 𝑥)))
5238, 42, 51mpbir2and 995 . . . . 5 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥 = inf(𝐴, ℝ, < ))
5352expr 644 . . . 4 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ 𝑥𝐴) → (∀𝑦𝐴 𝑥𝑦𝑥 = inf(𝐴, ℝ, < )))
5453ralrimiva 3102 . . 3 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∀𝑥𝐴 (∀𝑦𝐴 𝑥𝑦𝑥 = inf(𝐴, ℝ, < )))
55 breq1 4805 . . . . 5 (𝑥 = inf(𝐴, ℝ, < ) → (𝑥𝑦 ↔ inf(𝐴, ℝ, < ) ≤ 𝑦))
5655ralbidv 3122 . . . 4 (𝑥 = inf(𝐴, ℝ, < ) → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐴 inf(𝐴, ℝ, < ) ≤ 𝑦))
5756eqreu 3537 . . 3 ((inf(𝐴, ℝ, < ) ∈ 𝐴 ∧ ∀𝑦𝐴 inf(𝐴, ℝ, < ) ≤ 𝑦 ∧ ∀𝑥𝐴 (∀𝑦𝐴 𝑥𝑦𝑥 = inf(𝐴, ℝ, < ))) → ∃!𝑥𝐴𝑦𝐴 𝑥𝑦)
5830, 33, 54, 57syl3anc 1477 . 2 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∃!𝑥𝐴𝑦𝐴 𝑥𝑦)
594, 58rexlimddv 3171 1 ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥𝐴𝑦𝐴 𝑥𝑦)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1630   ∈ wcel 2137   ≠ wne 2930  ∀wral 3048  ∃wrex 3049  ∃!wreu 3050  {crab 3052   ⊆ wss 3713  ∅c0 4056   class class class wbr 4802  ‘cfv 6047  infcinf 8510  ℝcr 10125   < clt 10264   ≤ cle 10265  -cneg 10457  ℕcn 11210  ℤcz 11567  ℤ≥cuz 11877 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-sup 8511  df-inf 8512  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-nn 11211  df-n0 11483  df-z 11568  df-uz 11878 This theorem is referenced by:  zmin  11975
 Copyright terms: Public domain W3C validator