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