Metamath Proof Explorer

Theorem axsup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-sup with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

Ref Expression
Assertion axsup ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 ax-pre-sup ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) )
2 1 3expia ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) ) )
3 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
4 ltxrlt ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ 𝑦 <ℝ 𝑥 ) )
5 3 4 sylan ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ 𝑦 <ℝ 𝑥 ) )
6 5 an32s ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 < 𝑥 ↔ 𝑦 <ℝ 𝑥 ) )
7 6 ralbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) )
8 7 rexbidva ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) )
9 8 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) )
10 ltxrlt ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ 𝑥 <ℝ 𝑦 ) )
11 10 ancoms ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ 𝑥 <ℝ 𝑦 ) )
12 3 11 sylan ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ 𝑥 <ℝ 𝑦 ) )
13 12 an32s ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 < 𝑦 ↔ 𝑥 <ℝ 𝑦 ) )
14 13 notbid ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 <ℝ 𝑦 ) )
15 14 ralbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ) )
16 4 ancoms ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ 𝑦 <ℝ 𝑥 ) )
17 16 adantll ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ 𝑦 <ℝ 𝑥 ) )
18 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
19 ltxrlt ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 < 𝑧 ↔ 𝑦 <ℝ 𝑧 ) )
20 19 ancoms ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 < 𝑧 ↔ 𝑦 <ℝ 𝑧 ) )
21 18 20 sylan ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑦 < 𝑧 ↔ 𝑦 <ℝ 𝑧 ) )
22 21 an32s ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 < 𝑧 ↔ 𝑦 <ℝ 𝑧 ) )
23 22 rexbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) )
24 23 adantlr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) )
25 17 24 imbi12d ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) )
26 25 ralbidva ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) )
27 15 26 anbi12d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) ) )
28 27 rexbidva ⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) ) )
29 28 adantr ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) ) )
30 2 9 29 3imtr4d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) )
31 30 3impia ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 < 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )