| Step | Hyp | Ref
| Expression |
| 1 | | df-ov 7434 |
. 2
⊢ (𝑃Ray𝐴) = (Ray‘〈𝑃, 𝐴〉) |
| 2 | | eqid 2737 |
. . . . 5
⊢ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} |
| 3 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁)) |
| 4 | 3 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑃 ∈ (𝔼‘𝑛) ↔ 𝑃 ∈ (𝔼‘𝑁))) |
| 5 | 3 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐴 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑁))) |
| 6 | 4, 5 | 3anbi12d 1439 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ↔ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴))) |
| 7 | | rabeq 3451 |
. . . . . . . . 9
⊢
((𝔼‘𝑛)
= (𝔼‘𝑁) →
{𝑥 ∈
(𝔼‘𝑛) ∣
𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) |
| 8 | 3, 7 | syl 17 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) |
| 9 | 8 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉})) |
| 10 | 6, 9 | anbi12d 632 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) ↔ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 11 | 10 | rspcev 3622 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉})) → ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉})) |
| 12 | 2, 11 | mpanr2 704 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉})) |
| 13 | | simpr1 1195 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → 𝑃 ∈ (𝔼‘𝑁)) |
| 14 | | simpr2 1196 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → 𝐴 ∈ (𝔼‘𝑁)) |
| 15 | | fvex 6919 |
. . . . . . 7
⊢
(𝔼‘𝑁)
∈ V |
| 16 | 15 | rabex 5339 |
. . . . . 6
⊢ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} ∈ V |
| 17 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → (𝑝 ∈ (𝔼‘𝑛) ↔ 𝑃 ∈ (𝔼‘𝑛))) |
| 18 | | neeq1 3003 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → (𝑝 ≠ 𝑎 ↔ 𝑃 ≠ 𝑎)) |
| 19 | 17, 18 | 3anbi13d 1440 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ↔ (𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝑎))) |
| 20 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑃 → (𝑝OutsideOf〈𝑎, 𝑥〉 ↔ 𝑃OutsideOf〈𝑎, 𝑥〉)) |
| 21 | 20 | rabbidv 3444 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉}) |
| 22 | 21 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉} ↔ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉})) |
| 23 | 19, 22 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉}))) |
| 24 | 23 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉}))) |
| 25 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑎 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛))) |
| 26 | | neeq2 3004 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑃 ≠ 𝑎 ↔ 𝑃 ≠ 𝐴)) |
| 27 | 25, 26 | 3anbi23d 1441 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝑎) ↔ (𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴))) |
| 28 | | opeq1 4873 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑥〉 = 〈𝐴, 𝑥〉) |
| 29 | 28 | breq2d 5155 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (𝑃OutsideOf〈𝑎, 𝑥〉 ↔ 𝑃OutsideOf〈𝐴, 𝑥〉)) |
| 30 | 29 | rabbidv 3444 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) |
| 31 | 30 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉} ↔ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉})) |
| 32 | 27, 31 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉}) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 33 | 32 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝑎, 𝑥〉}) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 34 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑟 = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉})) |
| 35 | 34 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑟 = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} → (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 36 | 35 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑟 = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} → (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 37 | 24, 33, 36 | eloprabg 7543 |
. . . . . 6
⊢ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} ∈ V) → (〈〈𝑃, 𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 38 | 16, 37 | mp3an3 1452 |
. . . . 5
⊢ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (〈〈𝑃, 𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 39 | 13, 14, 38 | syl2anc 584 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → (〈〈𝑃, 𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃 ≠ 𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}))) |
| 40 | 12, 39 | mpbird 257 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → 〈〈𝑃, 𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})}) |
| 41 | | df-br 5144 |
. . . . 5
⊢
(〈𝑃, 𝐴〉Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} ↔ 〈〈𝑃, 𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ Ray) |
| 42 | | df-ray 36139 |
. . . . . 6
⊢ Ray =
{〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} |
| 43 | 42 | eleq2i 2833 |
. . . . 5
⊢
(〈〈𝑃,
𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ Ray ↔
〈〈𝑃, 𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})}) |
| 44 | 41, 43 | bitri 275 |
. . . 4
⊢
(〈𝑃, 𝐴〉Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} ↔ 〈〈𝑃, 𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})}) |
| 45 | | funray 36141 |
. . . . 5
⊢ Fun
Ray |
| 46 | | funbrfv 6957 |
. . . . 5
⊢ (Fun Ray
→ (〈𝑃, 𝐴〉Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} → (Ray‘〈𝑃, 𝐴〉) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉})) |
| 47 | 45, 46 | ax-mp 5 |
. . . 4
⊢
(〈𝑃, 𝐴〉Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉} → (Ray‘〈𝑃, 𝐴〉) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) |
| 48 | 44, 47 | sylbir 235 |
. . 3
⊢
(〈〈𝑃,
𝐴〉, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}〉 ∈ {〈〈𝑝, 𝑎〉, 𝑟〉 ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf〈𝑎, 𝑥〉})} → (Ray‘〈𝑃, 𝐴〉) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) |
| 49 | 40, 48 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → (Ray‘〈𝑃, 𝐴〉) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) |
| 50 | 1, 49 | eqtrid 2789 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃 ≠ 𝐴)) → (𝑃Ray𝐴) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf〈𝐴, 𝑥〉}) |