Step |
Hyp |
Ref |
Expression |
1 |
|
xrinfmsslem |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |
2 |
|
ssdifss |
⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* ) |
3 |
|
ssxr |
⊢ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) |
4 |
|
3orass |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ↔ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) ) |
5 |
|
pnfex |
⊢ +∞ ∈ V |
6 |
5
|
snid |
⊢ +∞ ∈ { +∞ } |
7 |
|
elndif |
⊢ ( +∞ ∈ { +∞ } → ¬ +∞ ∈ ( 𝐴 ∖ { +∞ } ) ) |
8 |
|
biorf |
⊢ ( ¬ +∞ ∈ ( 𝐴 ∖ { +∞ } ) → ( -∞ ∈ ( 𝐴 ∖ { +∞ } ) ↔ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) ) |
9 |
6 7 8
|
mp2b |
⊢ ( -∞ ∈ ( 𝐴 ∖ { +∞ } ) ↔ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) |
10 |
9
|
orbi2i |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ↔ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ ( +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) ) |
11 |
4 10
|
bitr4i |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { +∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ↔ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) |
12 |
3 11
|
sylib |
⊢ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) |
13 |
|
xrinfmsslem |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ* ∧ ( ( 𝐴 ∖ { +∞ } ) ⊆ ℝ ∨ -∞ ∈ ( 𝐴 ∖ { +∞ } ) ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) ) |
14 |
2 12 13
|
syl2anc2 |
⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) ) |
15 |
|
xrinfmexpnf |
⊢ ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) ) |
16 |
5
|
snss |
⊢ ( +∞ ∈ 𝐴 ↔ { +∞ } ⊆ 𝐴 ) |
17 |
|
undif |
⊢ ( { +∞ } ⊆ 𝐴 ↔ ( { +∞ } ∪ ( 𝐴 ∖ { +∞ } ) ) = 𝐴 ) |
18 |
|
uncom |
⊢ ( { +∞ } ∪ ( 𝐴 ∖ { +∞ } ) ) = ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) |
19 |
18
|
eqeq1i |
⊢ ( ( { +∞ } ∪ ( 𝐴 ∖ { +∞ } ) ) = 𝐴 ↔ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 ) |
20 |
17 19
|
bitri |
⊢ ( { +∞ } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 ) |
21 |
16 20
|
bitri |
⊢ ( +∞ ∈ 𝐴 ↔ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 ) |
22 |
|
raleq |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ) ) |
23 |
|
rexeq |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) |
24 |
23
|
imbi2d |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |
25 |
24
|
ralbidv |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |
26 |
22 25
|
anbi12d |
⊢ ( ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) = 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ) |
27 |
21 26
|
sylbi |
⊢ ( +∞ ∈ 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ) |
28 |
27
|
rexbidv |
⊢ ( +∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { +∞ } ) ∪ { +∞ } ) 𝑧 < 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ) |
29 |
15 28
|
syl5ib |
⊢ ( +∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∖ { +∞ } ) 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) ) |
30 |
14 29
|
mpan9 |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |
31 |
|
ssxr |
⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ) |
32 |
|
df-3or |
⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) ) |
33 |
|
or32 |
⊢ ( ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) ) |
34 |
32 33
|
bitri |
⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) ) |
35 |
31 34
|
sylib |
⊢ ( 𝐴 ⊆ ℝ* → ( ( 𝐴 ⊆ ℝ ∨ -∞ ∈ 𝐴 ) ∨ +∞ ∈ 𝐴 ) ) |
36 |
1 30 35
|
mpjaodan |
⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) |