Metamath Proof Explorer


Theorem axpre-sup

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. Note: The more general version with ordering on extended reals is axsup . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 elreal2 ( 𝑥 ∈ ℝ ↔ ( ( 1st𝑥 ) ∈ R𝑥 = ⟨ ( 1st𝑥 ) , 0R ⟩ ) )
2 1 simplbi ( 𝑥 ∈ ℝ → ( 1st𝑥 ) ∈ R )
3 2 adantl ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ ) → ( 1st𝑥 ) ∈ R )
4 fo1st 1st : V –onto→ V
5 fof ( 1st : V –onto→ V → 1st : V ⟶ V )
6 ffn ( 1st : V ⟶ V → 1st Fn V )
7 4 5 6 mp2b 1st Fn V
8 ssv 𝐴 ⊆ V
9 fvelimab ( ( 1st Fn V ∧ 𝐴 ⊆ V ) → ( 𝑤 ∈ ( 1st𝐴 ) ↔ ∃ 𝑦𝐴 ( 1st𝑦 ) = 𝑤 ) )
10 7 8 9 mp2an ( 𝑤 ∈ ( 1st𝐴 ) ↔ ∃ 𝑦𝐴 ( 1st𝑦 ) = 𝑤 )
11 r19.29 ( ( ∀ 𝑦𝐴 𝑦 < 𝑥 ∧ ∃ 𝑦𝐴 ( 1st𝑦 ) = 𝑤 ) → ∃ 𝑦𝐴 ( 𝑦 < 𝑥 ∧ ( 1st𝑦 ) = 𝑤 ) )
12 ssel2 ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) → 𝑦 ∈ ℝ )
13 ltresr2 ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ ( 1st𝑦 ) <R ( 1st𝑥 ) ) )
14 breq1 ( ( 1st𝑦 ) = 𝑤 → ( ( 1st𝑦 ) <R ( 1st𝑥 ) ↔ 𝑤 <R ( 1st𝑥 ) ) )
15 13 14 sylan9bb ( ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ∧ ( 1st𝑦 ) = 𝑤 ) → ( 𝑦 < 𝑥𝑤 <R ( 1st𝑥 ) ) )
16 15 biimpd ( ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ∧ ( 1st𝑦 ) = 𝑤 ) → ( 𝑦 < 𝑥𝑤 <R ( 1st𝑥 ) ) )
17 16 exp31 ( 𝑦 ∈ ℝ → ( 𝑥 ∈ ℝ → ( ( 1st𝑦 ) = 𝑤 → ( 𝑦 < 𝑥𝑤 <R ( 1st𝑥 ) ) ) ) )
18 12 17 syl ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) → ( 𝑥 ∈ ℝ → ( ( 1st𝑦 ) = 𝑤 → ( 𝑦 < 𝑥𝑤 <R ( 1st𝑥 ) ) ) ) )
19 18 imp4b ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 1st𝑦 ) = 𝑤𝑦 < 𝑥 ) → 𝑤 <R ( 1st𝑥 ) ) )
20 19 ancomsd ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑦 < 𝑥 ∧ ( 1st𝑦 ) = 𝑤 ) → 𝑤 <R ( 1st𝑥 ) ) )
21 20 an32s ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( ( 𝑦 < 𝑥 ∧ ( 1st𝑦 ) = 𝑤 ) → 𝑤 <R ( 1st𝑥 ) ) )
22 21 rexlimdva ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑦𝐴 ( 𝑦 < 𝑥 ∧ ( 1st𝑦 ) = 𝑤 ) → 𝑤 <R ( 1st𝑥 ) ) )
23 11 22 syl5 ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑦𝐴 𝑦 < 𝑥 ∧ ∃ 𝑦𝐴 ( 1st𝑦 ) = 𝑤 ) → 𝑤 <R ( 1st𝑥 ) ) )
24 23 expd ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦𝐴 𝑦 < 𝑥 → ( ∃ 𝑦𝐴 ( 1st𝑦 ) = 𝑤𝑤 <R ( 1st𝑥 ) ) ) )
25 10 24 syl7bi ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦𝐴 𝑦 < 𝑥 → ( 𝑤 ∈ ( 1st𝐴 ) → 𝑤 <R ( 1st𝑥 ) ) ) )
26 25 impr ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦𝐴 𝑦 < 𝑥 ) ) → ( 𝑤 ∈ ( 1st𝐴 ) → 𝑤 <R ( 1st𝑥 ) ) )
27 26 adantlr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦𝐴 𝑦 < 𝑥 ) ) → ( 𝑤 ∈ ( 1st𝐴 ) → 𝑤 <R ( 1st𝑥 ) ) )
28 27 ralrimiv ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ( 𝑥 ∈ ℝ ∧ ∀ 𝑦𝐴 𝑦 < 𝑥 ) ) → ∀ 𝑤 ∈ ( 1st𝐴 ) 𝑤 <R ( 1st𝑥 ) )
29 28 expr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦𝐴 𝑦 < 𝑥 → ∀ 𝑤 ∈ ( 1st𝐴 ) 𝑤 <R ( 1st𝑥 ) ) )
30 brralrspcev ( ( ( 1st𝑥 ) ∈ R ∧ ∀ 𝑤 ∈ ( 1st𝐴 ) 𝑤 <R ( 1st𝑥 ) ) → ∃ 𝑣R𝑤 ∈ ( 1st𝐴 ) 𝑤 <R 𝑣 )
31 3 29 30 syl6an ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦𝐴 𝑦 < 𝑥 → ∃ 𝑣R𝑤 ∈ ( 1st𝐴 ) 𝑤 <R 𝑣 ) )
32 31 rexlimdva ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 → ∃ 𝑣R𝑤 ∈ ( 1st𝐴 ) 𝑤 <R 𝑣 ) )
33 n0 ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦𝐴 )
34 fnfvima ( ( 1st Fn V ∧ 𝐴 ⊆ V ∧ 𝑦𝐴 ) → ( 1st𝑦 ) ∈ ( 1st𝐴 ) )
35 7 8 34 mp3an12 ( 𝑦𝐴 → ( 1st𝑦 ) ∈ ( 1st𝐴 ) )
36 35 ne0d ( 𝑦𝐴 → ( 1st𝐴 ) ≠ ∅ )
37 36 exlimiv ( ∃ 𝑦 𝑦𝐴 → ( 1st𝐴 ) ≠ ∅ )
38 33 37 sylbi ( 𝐴 ≠ ∅ → ( 1st𝐴 ) ≠ ∅ )
39 supsr ( ( ( 1st𝐴 ) ≠ ∅ ∧ ∃ 𝑣R𝑤 ∈ ( 1st𝐴 ) 𝑤 <R 𝑣 ) → ∃ 𝑣R ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 ∧ ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) ) )
40 39 ex ( ( 1st𝐴 ) ≠ ∅ → ( ∃ 𝑣R𝑤 ∈ ( 1st𝐴 ) 𝑤 <R 𝑣 → ∃ 𝑣R ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 ∧ ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) ) ) )
41 38 40 syl ( 𝐴 ≠ ∅ → ( ∃ 𝑣R𝑤 ∈ ( 1st𝐴 ) 𝑤 <R 𝑣 → ∃ 𝑣R ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 ∧ ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) ) ) )
42 41 adantl ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑣R𝑤 ∈ ( 1st𝐴 ) 𝑤 <R 𝑣 → ∃ 𝑣R ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 ∧ ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) ) ) )
43 breq2 ( 𝑤 = ( 1st𝑦 ) → ( 𝑣 <R 𝑤𝑣 <R ( 1st𝑦 ) ) )
44 43 notbid ( 𝑤 = ( 1st𝑦 ) → ( ¬ 𝑣 <R 𝑤 ↔ ¬ 𝑣 <R ( 1st𝑦 ) ) )
45 44 rspccv ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 → ( ( 1st𝑦 ) ∈ ( 1st𝐴 ) → ¬ 𝑣 <R ( 1st𝑦 ) ) )
46 35 45 syl5com ( 𝑦𝐴 → ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R ( 1st𝑦 ) ) )
47 46 adantl ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) → ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 → ¬ 𝑣 <R ( 1st𝑦 ) ) )
48 elreal2 ( 𝑦 ∈ ℝ ↔ ( ( 1st𝑦 ) ∈ R𝑦 = ⟨ ( 1st𝑦 ) , 0R ⟩ ) )
49 48 simprbi ( 𝑦 ∈ ℝ → 𝑦 = ⟨ ( 1st𝑦 ) , 0R ⟩ )
50 49 breq2d ( 𝑦 ∈ ℝ → ( ⟨ 𝑣 , 0R ⟩ < 𝑦 ↔ ⟨ 𝑣 , 0R ⟩ < ⟨ ( 1st𝑦 ) , 0R ⟩ ) )
51 ltresr ( ⟨ 𝑣 , 0R ⟩ < ⟨ ( 1st𝑦 ) , 0R ⟩ ↔ 𝑣 <R ( 1st𝑦 ) )
52 50 51 bitrdi ( 𝑦 ∈ ℝ → ( ⟨ 𝑣 , 0R ⟩ < 𝑦𝑣 <R ( 1st𝑦 ) ) )
53 12 52 syl ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) → ( ⟨ 𝑣 , 0R ⟩ < 𝑦𝑣 <R ( 1st𝑦 ) ) )
54 53 notbid ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) → ( ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ↔ ¬ 𝑣 <R ( 1st𝑦 ) ) )
55 47 54 sylibrd ( ( 𝐴 ⊆ ℝ ∧ 𝑦𝐴 ) → ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 → ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ) )
56 55 ralrimdva ( 𝐴 ⊆ ℝ → ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 → ∀ 𝑦𝐴 ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ) )
57 56 ad2antrr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣R ) → ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 → ∀ 𝑦𝐴 ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ) )
58 49 breq1d ( 𝑦 ∈ ℝ → ( 𝑦 <𝑣 , 0R ⟩ ↔ ⟨ ( 1st𝑦 ) , 0R ⟩ <𝑣 , 0R ⟩ ) )
59 ltresr ( ⟨ ( 1st𝑦 ) , 0R ⟩ <𝑣 , 0R ⟩ ↔ ( 1st𝑦 ) <R 𝑣 )
60 58 59 bitrdi ( 𝑦 ∈ ℝ → ( 𝑦 <𝑣 , 0R ⟩ ↔ ( 1st𝑦 ) <R 𝑣 ) )
61 48 simplbi ( 𝑦 ∈ ℝ → ( 1st𝑦 ) ∈ R )
62 breq1 ( 𝑤 = ( 1st𝑦 ) → ( 𝑤 <R 𝑣 ↔ ( 1st𝑦 ) <R 𝑣 ) )
63 breq1 ( 𝑤 = ( 1st𝑦 ) → ( 𝑤 <R 𝑢 ↔ ( 1st𝑦 ) <R 𝑢 ) )
64 63 rexbidv ( 𝑤 = ( 1st𝑦 ) → ( ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ↔ ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 ) )
65 62 64 imbi12d ( 𝑤 = ( 1st𝑦 ) → ( ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) ↔ ( ( 1st𝑦 ) <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 ) ) )
66 65 rspccv ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ( ( 1st𝑦 ) ∈ R → ( ( 1st𝑦 ) <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 ) ) )
67 61 66 syl5 ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ( 𝑦 ∈ ℝ → ( ( 1st𝑦 ) <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 ) ) )
68 67 com3l ( 𝑦 ∈ ℝ → ( ( 1st𝑦 ) <R 𝑣 → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 ) ) )
69 60 68 sylbid ( 𝑦 ∈ ℝ → ( 𝑦 <𝑣 , 0R ⟩ → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 ) ) )
70 69 adantr ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑦 <𝑣 , 0R ⟩ → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 ) ) )
71 fvelimab ( ( 1st Fn V ∧ 𝐴 ⊆ V ) → ( 𝑢 ∈ ( 1st𝐴 ) ↔ ∃ 𝑧𝐴 ( 1st𝑧 ) = 𝑢 ) )
72 7 8 71 mp2an ( 𝑢 ∈ ( 1st𝐴 ) ↔ ∃ 𝑧𝐴 ( 1st𝑧 ) = 𝑢 )
73 ssel2 ( ( 𝐴 ⊆ ℝ ∧ 𝑧𝐴 ) → 𝑧 ∈ ℝ )
74 ltresr2 ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 < 𝑧 ↔ ( 1st𝑦 ) <R ( 1st𝑧 ) ) )
75 73 74 sylan2 ( ( 𝑦 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑧𝐴 ) ) → ( 𝑦 < 𝑧 ↔ ( 1st𝑦 ) <R ( 1st𝑧 ) ) )
76 breq2 ( ( 1st𝑧 ) = 𝑢 → ( ( 1st𝑦 ) <R ( 1st𝑧 ) ↔ ( 1st𝑦 ) <R 𝑢 ) )
77 75 76 sylan9bb ( ( ( 𝑦 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑧𝐴 ) ) ∧ ( 1st𝑧 ) = 𝑢 ) → ( 𝑦 < 𝑧 ↔ ( 1st𝑦 ) <R 𝑢 ) )
78 77 exbiri ( ( 𝑦 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑧𝐴 ) ) → ( ( 1st𝑧 ) = 𝑢 → ( ( 1st𝑦 ) <R 𝑢𝑦 < 𝑧 ) ) )
79 78 expr ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑧𝐴 → ( ( 1st𝑧 ) = 𝑢 → ( ( 1st𝑦 ) <R 𝑢𝑦 < 𝑧 ) ) ) )
80 79 com4r ( ( 1st𝑦 ) <R 𝑢 → ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑧𝐴 → ( ( 1st𝑧 ) = 𝑢𝑦 < 𝑧 ) ) ) )
81 80 imp ( ( ( 1st𝑦 ) <R 𝑢 ∧ ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) ) → ( 𝑧𝐴 → ( ( 1st𝑧 ) = 𝑢𝑦 < 𝑧 ) ) )
82 81 reximdvai ( ( ( 1st𝑦 ) <R 𝑢 ∧ ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) ) → ( ∃ 𝑧𝐴 ( 1st𝑧 ) = 𝑢 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) )
83 72 82 syl5bi ( ( ( 1st𝑦 ) <R 𝑢 ∧ ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) ) → ( 𝑢 ∈ ( 1st𝐴 ) → ∃ 𝑧𝐴 𝑦 < 𝑧 ) )
84 83 expcom ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ( 1st𝑦 ) <R 𝑢 → ( 𝑢 ∈ ( 1st𝐴 ) → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
85 84 com23 ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑢 ∈ ( 1st𝐴 ) → ( ( 1st𝑦 ) <R 𝑢 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
86 85 rexlimdv ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∃ 𝑢 ∈ ( 1st𝐴 ) ( 1st𝑦 ) <R 𝑢 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) )
87 70 86 syl6d ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( 𝑦 <𝑣 , 0R ⟩ → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
88 87 com23 ( ( 𝑦 ∈ ℝ ∧ 𝐴 ⊆ ℝ ) → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
89 88 ex ( 𝑦 ∈ ℝ → ( 𝐴 ⊆ ℝ → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
90 89 com3l ( 𝐴 ⊆ ℝ → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ( 𝑦 ∈ ℝ → ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
91 90 ad2antrr ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣R ) → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ( 𝑦 ∈ ℝ → ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
92 91 ralrimdv ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣R ) → ( ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) → ∀ 𝑦 ∈ ℝ ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
93 opelreal ( ⟨ 𝑣 , 0R ⟩ ∈ ℝ ↔ 𝑣R )
94 93 biimpri ( 𝑣R → ⟨ 𝑣 , 0R ⟩ ∈ ℝ )
95 94 adantl ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣R ) → ⟨ 𝑣 , 0R ⟩ ∈ ℝ )
96 breq1 ( 𝑥 = ⟨ 𝑣 , 0R ⟩ → ( 𝑥 < 𝑦 ↔ ⟨ 𝑣 , 0R ⟩ < 𝑦 ) )
97 96 notbid ( 𝑥 = ⟨ 𝑣 , 0R ⟩ → ( ¬ 𝑥 < 𝑦 ↔ ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ) )
98 97 ralbidv ( 𝑥 = ⟨ 𝑣 , 0R ⟩ → ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦𝐴 ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ) )
99 breq2 ( 𝑥 = ⟨ 𝑣 , 0R ⟩ → ( 𝑦 < 𝑥𝑦 <𝑣 , 0R ⟩ ) )
100 99 imbi1d ( 𝑥 = ⟨ 𝑣 , 0R ⟩ → ( ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ↔ ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
101 100 ralbidv ( 𝑥 = ⟨ 𝑣 , 0R ⟩ → ( ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
102 98 101 anbi12d ( 𝑥 = ⟨ 𝑣 , 0R ⟩ → ( ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦𝐴 ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
103 102 rspcev ( ( ⟨ 𝑣 , 0R ⟩ ∈ ℝ ∧ ( ∀ 𝑦𝐴 ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
104 103 ex ( ⟨ 𝑣 , 0R ⟩ ∈ ℝ → ( ( ∀ 𝑦𝐴 ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
105 95 104 syl ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣R ) → ( ( ∀ 𝑦𝐴 ¬ ⟨ 𝑣 , 0R ⟩ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <𝑣 , 0R ⟩ → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
106 57 92 105 syl2and ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ 𝑣R ) → ( ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 ∧ ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
107 106 rexlimdva ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑣R ( ∀ 𝑤 ∈ ( 1st𝐴 ) ¬ 𝑣 <R 𝑤 ∧ ∀ 𝑤R ( 𝑤 <R 𝑣 → ∃ 𝑢 ∈ ( 1st𝐴 ) 𝑤 <R 𝑢 ) ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
108 32 42 107 3syld ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ) )
109 108 3impia ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦 < 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )