| Step | Hyp | Ref
| Expression |
| 1 | | reeanv 3229 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ∃𝑚 ∈
ℕ (((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) ↔ (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
| 2 | | simp1 1137 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) → 𝑝 ∈ (𝔼‘𝑛)) |
| 3 | | simp1 1137 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) → 𝑝 ∈ (𝔼‘𝑚)) |
| 4 | | axdimuniq 28928 |
. . . . . . . . . . . . . . 15
⊢ (((𝑛 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑛)) ∧ (𝑚 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑚))) → 𝑛 = 𝑚) |
| 5 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (𝔼‘𝑛) = (𝔼‘𝑚)) |
| 6 | | rabeq 3451 |
. . . . . . . . . . . . . . . . . . 19
⊢
((𝔼‘𝑛)
= (𝔼‘𝑚) →
{𝑥 ∈
(𝔼‘𝑛) ∣
𝑝OutsideOf〈𝑎, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) |
| 8 | 7 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ↔ 𝑟 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
| 9 | 8 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ (𝑟 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
| 10 | | eqtr3 2763 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠) |
| 11 | 9, 10 | biimtrdi 253 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠)) |
| 12 | 4, 11 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑛 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑛)) ∧ (𝑚 ∈ ℕ ∧ 𝑝 ∈ (𝔼‘𝑚))) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠)) |
| 13 | 12 | an4s 660 |
. . . . . . . . . . . . 13
⊢ (((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑝 ∈ (𝔼‘𝑚))) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠)) |
| 14 | 13 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑝 ∈ (𝔼‘𝑚)) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → 𝑟 = 𝑠))) |
| 15 | 14 | com3l 89 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑝 ∈ (𝔼‘𝑚)) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠))) |
| 16 | 2, 3, 15 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ (𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎)) → ((𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠))) |
| 17 | 16 | imp 406 |
. . . . . . . . 9
⊢ ((((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ (𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎)) ∧ (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠)) |
| 18 | 17 | an4s 660 |
. . . . . . . 8
⊢ ((((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) → 𝑟 = 𝑠)) |
| 19 | 18 | com12 32 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ) →
((((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠)) |
| 20 | 19 | rexlimivv 3201 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ∃𝑚 ∈
ℕ (((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠) |
| 21 | 1, 20 | sylbir 235 |
. . . . 5
⊢
((∃𝑛 ∈
ℕ ((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠) |
| 22 | 21 | gen2 1796 |
. . . 4
⊢
∀𝑟∀𝑠((∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠) |
| 23 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ↔ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
| 24 | 23 | anbi2d 630 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
| 25 | 24 | rexbidv 3179 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
| 26 | 5 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑝 ∈ (𝔼‘𝑛) ↔ 𝑝 ∈ (𝔼‘𝑚))) |
| 27 | 5 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑎 ∈ (𝔼‘𝑛) ↔ 𝑎 ∈ (𝔼‘𝑚))) |
| 28 | 26, 27 | 3anbi12d 1439 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ↔ (𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎))) |
| 29 | 7 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ↔ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
| 30 | 28, 29 | anbi12d 632 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
| 31 | 30 | cbvrexvw 3238 |
. . . . . 6
⊢
(∃𝑛 ∈
ℕ ((𝑝 ∈
(𝔼‘𝑛) ∧
𝑎 ∈
(𝔼‘𝑛) ∧
𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) |
| 32 | 25, 31 | bitrdi 287 |
. . . . 5
⊢ (𝑟 = 𝑠 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}))) |
| 33 | 32 | mo4 2566 |
. . . 4
⊢
(∃*𝑟∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∀𝑟∀𝑠((∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ∧ ∃𝑚 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑚) ∧ 𝑎 ∈ (𝔼‘𝑚) ∧ 𝑝 ≠ 𝑎) ∧ 𝑠 = {𝑥 ∈ (𝔼‘𝑚) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})) → 𝑟 = 𝑠)) |
| 34 | 22, 33 | mpbir 231 |
. . 3
⊢
∃*𝑟∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) |
| 35 | 34 | funoprab 7555 |
. 2
⊢ Fun
{〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} |
| 36 | | df-ray 36139 |
. . 3
⊢ Ray =
{〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} |
| 37 | 36 | funeqi 6587 |
. 2
⊢ (Fun Ray
↔ Fun {〈〈𝑝,
𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})}) |
| 38 | 35, 37 | mpbir 231 |
1
⊢ Fun
Ray |