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

Theorem uzwo3 11521
Description: Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 11488 allows the lower bound 𝐵 to be any real number. See also nnwo 11489 and nnwos 11491. (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 10093 . . . 4 (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
21adantr 479 . . 3 ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) → -𝐵 ∈ ℝ)
3 arch 11042 . . 3 (-𝐵 ∈ ℝ → ∃𝑛 ∈ ℕ -𝐵 < 𝑛)
42, 3syl 17 . 2 ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) → ∃𝑛 ∈ ℕ -𝐵 < 𝑛)
5 simplrl 795 . . . . 5 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧})
6 simplrl 795 . . . . . . . . . . . . 13 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑛 ∈ ℕ)
7 nnnegz 11119 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → -𝑛 ∈ ℤ)
86, 7syl 17 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 ∈ ℤ)
98zred 11220 . . . . . . . . . . 11 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 ∈ ℝ)
10 simprl 789 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑧 ∈ ℤ)
1110zred 11220 . . . . . . . . . . 11 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑧 ∈ ℝ)
12 simpll 785 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝐵 ∈ ℝ)
136nnred 10788 . . . . . . . . . . . . 13 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑛 ∈ ℝ)
14 simplrr 796 . . . . . . . . . . . . 13 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝐵 < 𝑛)
1512, 13, 14ltnegcon1d 10354 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 < 𝐵)
16 simprr 791 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝐵𝑧)
179, 12, 11, 15, 16ltletrd 9946 . . . . . . . . . . 11 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛 < 𝑧)
189, 11, 17ltled 9934 . . . . . . . . . 10 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → -𝑛𝑧)
19 eluz 11437 . . . . . . . . . . 11 ((-𝑛 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑧 ∈ (ℤ‘-𝑛) ↔ -𝑛𝑧))
208, 10, 19syl2anc 690 . . . . . . . . . 10 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → (𝑧 ∈ (ℤ‘-𝑛) ↔ -𝑛𝑧))
2118, 20mpbird 245 . . . . . . . . 9 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑧 ∈ ℤ ∧ 𝐵𝑧)) → 𝑧 ∈ (ℤ‘-𝑛))
2221expr 640 . . . . . . . 8 (((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ 𝑧 ∈ ℤ) → (𝐵𝑧𝑧 ∈ (ℤ‘-𝑛)))
2322ralrimiva 2853 . . . . . . 7 ((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∀𝑧 ∈ ℤ (𝐵𝑧𝑧 ∈ (ℤ‘-𝑛)))
24 rabss 3546 . . . . . . 7 ({𝑧 ∈ ℤ ∣ 𝐵𝑧} ⊆ (ℤ‘-𝑛) ↔ ∀𝑧 ∈ ℤ (𝐵𝑧𝑧 ∈ (ℤ‘-𝑛)))
2523, 24sylibr 222 . . . . . 6 ((𝐵 ∈ ℝ ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → {𝑧 ∈ ℤ ∣ 𝐵𝑧} ⊆ (ℤ‘-𝑛))
2625adantlr 746 . . . . 5 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → {𝑧 ∈ ℤ ∣ 𝐵𝑧} ⊆ (ℤ‘-𝑛))
275, 26sstrd 3482 . . . 4 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ⊆ (ℤ‘-𝑛))
28 simplrr 796 . . . 4 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ≠ ∅)
29 infssuzcl 11508 . . . 4 ((𝐴 ⊆ (ℤ‘-𝑛) ∧ 𝐴 ≠ ∅) → inf(𝐴, ℝ, < ) ∈ 𝐴)
3027, 28, 29syl2anc 690 . . 3 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → inf(𝐴, ℝ, < ) ∈ 𝐴)
31 infssuzle 11507 . . . . 5 ((𝐴 ⊆ (ℤ‘-𝑛) ∧ 𝑦𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑦)
3227, 31sylan 486 . . . 4 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ 𝑦𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑦)
3332ralrimiva 2853 . . 3 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∀𝑦𝐴 inf(𝐴, ℝ, < ) ≤ 𝑦)
3430adantr 479 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → inf(𝐴, ℝ, < ) ∈ 𝐴)
35 simprr 791 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → ∀𝑦𝐴 𝑥𝑦)
36 breq2 4485 . . . . . . . 8 (𝑦 = inf(𝐴, ℝ, < ) → (𝑥𝑦𝑥 ≤ inf(𝐴, ℝ, < )))
3736rspcv 3182 . . . . . . 7 (inf(𝐴, ℝ, < ) ∈ 𝐴 → (∀𝑦𝐴 𝑥𝑦𝑥 ≤ inf(𝐴, ℝ, < )))
3834, 35, 37sylc 62 . . . . . 6 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥 ≤ inf(𝐴, ℝ, < ))
3927adantr 479 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝐴 ⊆ (ℤ‘-𝑛))
40 simprl 789 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥𝐴)
41 infssuzle 11507 . . . . . . 7 ((𝐴 ⊆ (ℤ‘-𝑛) ∧ 𝑥𝐴) → inf(𝐴, ℝ, < ) ≤ 𝑥)
4239, 40, 41syl2anc 690 . . . . . 6 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → inf(𝐴, ℝ, < ) ≤ 𝑥)
43 uzssz 11443 . . . . . . . . . . 11 (ℤ‘-𝑛) ⊆ ℤ
44 zssre 11123 . . . . . . . . . . 11 ℤ ⊆ ℝ
4543, 44sstri 3481 . . . . . . . . . 10 (ℤ‘-𝑛) ⊆ ℝ
4627, 45syl6ss 3484 . . . . . . . . 9 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → 𝐴 ⊆ ℝ)
4746adantr 479 . . . . . . . 8 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝐴 ⊆ ℝ)
4847, 40sseldd 3473 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥 ∈ ℝ)
4946, 30sseldd 3473 . . . . . . . 8 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → inf(𝐴, ℝ, < ) ∈ ℝ)
5049adantr 479 . . . . . . 7 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → inf(𝐴, ℝ, < ) ∈ ℝ)
5148, 50letri3d 9928 . . . . . 6 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → (𝑥 = inf(𝐴, ℝ, < ) ↔ (𝑥 ≤ inf(𝐴, ℝ, < ) ∧ inf(𝐴, ℝ, < ) ≤ 𝑥)))
5238, 42, 51mpbir2and 958 . . . . 5 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ (𝑥𝐴 ∧ ∀𝑦𝐴 𝑥𝑦)) → 𝑥 = inf(𝐴, ℝ, < ))
5352expr 640 . . . 4 ((((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) ∧ 𝑥𝐴) → (∀𝑦𝐴 𝑥𝑦𝑥 = inf(𝐴, ℝ, < )))
5453ralrimiva 2853 . . 3 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∀𝑥𝐴 (∀𝑦𝐴 𝑥𝑦𝑥 = inf(𝐴, ℝ, < )))
55 breq1 4484 . . . . 5 (𝑥 = inf(𝐴, ℝ, < ) → (𝑥𝑦 ↔ inf(𝐴, ℝ, < ) ≤ 𝑦))
5655ralbidv 2873 . . . 4 (𝑥 = inf(𝐴, ℝ, < ) → (∀𝑦𝐴 𝑥𝑦 ↔ ∀𝑦𝐴 inf(𝐴, ℝ, < ) ≤ 𝑦))
5756eqreu 3269 . . 3 ((inf(𝐴, ℝ, < ) ∈ 𝐴 ∧ ∀𝑦𝐴 inf(𝐴, ℝ, < ) ≤ 𝑦 ∧ ∀𝑥𝐴 (∀𝑦𝐴 𝑥𝑦𝑥 = inf(𝐴, ℝ, < ))) → ∃!𝑥𝐴𝑦𝐴 𝑥𝑦)
5830, 33, 54, 57syl3anc 1317 . 2 (((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) ∧ (𝑛 ∈ ℕ ∧ -𝐵 < 𝑛)) → ∃!𝑥𝐴𝑦𝐴 𝑥𝑦)
594, 58rexlimddv 2921 1 ((𝐵 ∈ ℝ ∧ (𝐴 ⊆ {𝑧 ∈ ℤ ∣ 𝐵𝑧} ∧ 𝐴 ≠ ∅)) → ∃!𝑥𝐴𝑦𝐴 𝑥𝑦)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  wne 2684  wral 2800  wrex 2801  ∃!wreu 2802  {crab 2804  wss 3444  c0 3777   class class class wbr 4481  cfv 5689  infcinf 8104  cr 9688   < clt 9827  cle 9828  -cneg 10016  cn 10773  cz 11116  cuz 11423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721  ax-cnex 9745  ax-resscn 9746  ax-1cn 9747  ax-icn 9748  ax-addcl 9749  ax-addrcl 9750  ax-mulcl 9751  ax-mulrcl 9752  ax-mulcom 9753  ax-addass 9754  ax-mulass 9755  ax-distr 9756  ax-i2m1 9757  ax-1ne0 9758  ax-1rid 9759  ax-rnegex 9760  ax-rrecex 9761  ax-cnre 9762  ax-pre-lttri 9763  ax-pre-lttrn 9764  ax-pre-ltadd 9765  ax-pre-mulgt0 9766  ax-pre-sup 9767
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6387  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-om 6832  df-wrecs 7167  df-recs 7229  df-rdg 7267  df-er 7503  df-en 7716  df-dom 7717  df-sdom 7718  df-sup 8105  df-inf 8106  df-pnf 9829  df-mnf 9830  df-xr 9831  df-ltxr 9832  df-le 9833  df-sub 10017  df-neg 10018  df-nn 10774  df-n0 11046  df-z 11117  df-uz 11424
This theorem is referenced by:  zmin  11522
  Copyright terms: Public domain W3C validator