Step |
Hyp |
Ref |
Expression |
1 |
|
xrsupsslem |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) |
2 |
|
ssdifss |
⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* ) |
3 |
|
ssxr |
⊢ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ) |
4 |
|
df-3or |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ↔ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ) |
5 |
|
neldifsn |
⊢ ¬ -∞ ∈ ( 𝐴 ∖ { -∞ } ) |
6 |
5
|
biorfi |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ↔ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ) |
7 |
4 6
|
bitr4i |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ∨ -∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ↔ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ) |
8 |
3 7
|
sylib |
⊢ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* → ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ) |
9 |
|
xrsupsslem |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* ∧ ( ( 𝐴 ∖ { -∞ } ) ⊆ ℝ ∨ +∞ ∈ ( 𝐴 ∖ { -∞ } ) ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) ) |
10 |
2 8 9
|
syl2anc2 |
⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) ) |
11 |
|
xrsupexmnf |
⊢ ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ) |
12 |
|
snssi |
⊢ ( -∞ ∈ 𝐴 → { -∞ } ⊆ 𝐴 ) |
13 |
|
undif |
⊢ ( { -∞ } ⊆ 𝐴 ↔ ( { -∞ } ∪ ( 𝐴 ∖ { -∞ } ) ) = 𝐴 ) |
14 |
|
uncom |
⊢ ( { -∞ } ∪ ( 𝐴 ∖ { -∞ } ) ) = ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) |
15 |
14
|
eqeq1i |
⊢ ( ( { -∞ } ∪ ( 𝐴 ∖ { -∞ } ) ) = 𝐴 ↔ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 ) |
16 |
13 15
|
bitri |
⊢ ( { -∞ } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 ) |
17 |
|
raleq |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ) ) |
18 |
|
rexeq |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) |
19 |
18
|
imbi2d |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ↔ ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) |
20 |
19
|
ralbidv |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) |
21 |
17 20
|
anbi12d |
⊢ ( ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) = 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) ) |
22 |
16 21
|
sylbi |
⊢ ( { -∞ } ⊆ 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) ) |
23 |
12 22
|
syl |
⊢ ( -∞ ∈ 𝐴 → ( ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) ) |
24 |
23
|
rexbidv |
⊢ ( -∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( ( 𝐴 ∖ { -∞ } ) ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) ) |
25 |
11 24
|
syl5ib |
⊢ ( -∞ ∈ 𝐴 → ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∖ { -∞ } ) 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) ) |
26 |
10 25
|
mpan9 |
⊢ ( ( 𝐴 ⊆ ℝ* ∧ -∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) |
27 |
|
ssxr |
⊢ ( 𝐴 ⊆ ℝ* → ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ) |
28 |
|
df-3or |
⊢ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ∨ -∞ ∈ 𝐴 ) ↔ ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) ) |
29 |
27 28
|
sylib |
⊢ ( 𝐴 ⊆ ℝ* → ( ( 𝐴 ⊆ ℝ ∨ +∞ ∈ 𝐴 ) ∨ -∞ ∈ 𝐴 ) ) |
30 |
1 26 29
|
mpjaodan |
⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) ) |