Step |
Hyp |
Ref |
Expression |
1 |
|
id |
⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( 𝐴 (,) 𝐵 ) = ∅ ) |
2 |
|
iooid |
⊢ ( 0 (,) 0 ) = ∅ |
3 |
|
ioof |
⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ |
4 |
|
ffn |
⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) ) |
5 |
3 4
|
ax-mp |
⊢ (,) Fn ( ℝ* × ℝ* ) |
6 |
|
0xr |
⊢ 0 ∈ ℝ* |
7 |
|
fnovrn |
⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ 0 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 0 (,) 0 ) ∈ ran (,) ) |
8 |
5 6 6 7
|
mp3an |
⊢ ( 0 (,) 0 ) ∈ ran (,) |
9 |
2 8
|
eqeltrri |
⊢ ∅ ∈ ran (,) |
10 |
1 9
|
eqeltrdi |
⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ( 𝐴 (,) 𝐵 ) ∈ ran (,) ) |
11 |
|
n0 |
⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) |
12 |
|
eliooxr |
⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ) |
13 |
|
fnovrn |
⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) ) |
14 |
5 13
|
mp3an1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) ) |
15 |
12 14
|
syl |
⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) ) |
16 |
15
|
exlimiv |
⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ ran (,) ) |
17 |
11 16
|
sylbi |
⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 (,) 𝐵 ) ∈ ran (,) ) |
18 |
10 17
|
pm2.61ine |
⊢ ( 𝐴 (,) 𝐵 ) ∈ ran (,) |