Step | Hyp | Ref
| Expression |
1 | | reeanv 3270 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ∃𝑚 ∈
ℕ (((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) ↔ (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
2 | | simp1 1137 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) → 𝑝 ∈ (𝔼‘𝑛)) |
3 | | simp1 1137 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) → 𝑝 ∈ (𝔼‘𝑚)) |
4 | | axdimuniq 26859 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑛)) ∧ (𝑚 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑚))) → 𝑛 = 𝑚) |
5 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (𝔼‘𝑛) = (𝔼‘𝑚)) |
6 | | rabeq 3385 |
. . . . . . . . . . . . . . . . . . 19
⊢
((𝔼‘𝑛)
= (𝔼‘𝑚) →
{𝑥 ∈
(𝔼‘𝑛) ∣
𝑝OutsideOf〈𝑎, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) |
8 | 7 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ↔ 𝑟 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
9 | 8 | anbi1d 633 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ (𝑟 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
10 | | eqtr3 2760 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠) |
11 | 9, 10 | syl6bi 256 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠)) |
12 | 4, 11 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑛)) ∧ (𝑚 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑚))) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠)) |
13 | 12 | an4s 660 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑝 ∈ (𝔼‘𝑚))) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠)) |
14 | 13 | ex 416 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑝 ∈ (𝔼‘𝑚)) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠))) |
15 | 14 | com3l 89 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑝 ∈ (𝔼‘𝑚)) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠))) |
16 | 2, 3, 15 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ (𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎)) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠))) |
17 | 16 | imp 410 |
. . . . . . . . 9
⊢ ((((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ (𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎)) ∧ (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠)) |
18 | 17 | an4s 660 |
. . . . . . . 8
⊢ ((((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠)) |
19 | 18 | com12 32 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) →
((((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠)) |
20 | 19 | rexlimivv 3202 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ∃𝑚 ∈
ℕ (((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠) |
21 | 1, 20 | sylbir 238 |
. . . . 5
⊢
((∃𝑛 ∈
ℕ ((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠) |
22 | 21 | gen2 1803 |
. . . 4
⊢
∀𝑟∀𝑠((∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠) |
23 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ↔ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
24 | 23 | anbi2d 632 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
25 | 24 | rexbidv 3207 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
26 | 5 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑝 ∈ (𝔼‘𝑛) ↔ 𝑝 ∈ (𝔼‘𝑚))) |
27 | 5 | eleq2d 2818 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑎 ∈ (𝔼‘𝑛) ↔ 𝑎 ∈ (𝔼‘𝑚))) |
28 | 26, 27 | 3anbi12d 1438 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ↔ (𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎))) |
29 | 7 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ↔ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
30 | 28, 29 | anbi12d 634 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
31 | 30 | cbvrexvw 3350 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
32 | 25, 31 | bitrdi 290 |
. . . . 5
⊢ (𝑟 = 𝑠 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
33 | 32 | mo4 2566 |
. . . 4
⊢
(∃*𝑟∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∀𝑟∀𝑠((∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠)) |
34 | 22, 33 | mpbir 234 |
. . 3
⊢
∃*𝑟∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) |
35 | 34 | funoprab 7288 |
. 2
⊢ Fun
{〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} |
36 | | df-ray 34078 |
. . 3
⊢ Ray =
{〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} |
37 | 36 | funeqi 6360 |
. 2
⊢ (Fun Ray
↔ Fun {〈〈𝑝,
𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})}) |
38 | 35, 37 | mpbir 234 |
1
⊢ Fun
Ray |