This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( ( 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 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 <ℝ 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧 ) ) )