Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fvray Structured version   Visualization version   GIF version

Theorem fvray 31418
 Description: Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
fvray ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → (𝑃Ray𝐴) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
Distinct variable groups:   𝑥,𝐴   𝑥,𝑁   𝑥,𝑃

Proof of Theorem fvray
Dummy variables 𝑎 𝑛 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ov 6552 . 2 (𝑃Ray𝐴) = (Ray‘⟨𝑃, 𝐴⟩)
2 eqid 2610 . . . . 5 {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}
3 fveq2 6103 . . . . . . . . 9 (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
43eleq2d 2673 . . . . . . . 8 (𝑛 = 𝑁 → (𝑃 ∈ (𝔼‘𝑛) ↔ 𝑃 ∈ (𝔼‘𝑁)))
53eleq2d 2673 . . . . . . . 8 (𝑛 = 𝑁 → (𝐴 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑁)))
64, 53anbi12d 1392 . . . . . . 7 (𝑛 = 𝑁 → ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ↔ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)))
7 rabeq 3166 . . . . . . . . 9 ((𝔼‘𝑛) = (𝔼‘𝑁) → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
83, 7syl 17 . . . . . . . 8 (𝑛 = 𝑁 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
98eqeq2d 2620 . . . . . . 7 (𝑛 = 𝑁 → ({𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}))
106, 9anbi12d 743 . . . . . 6 (𝑛 = 𝑁 → (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}) ↔ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
1110rspcev 3282 . . . . 5 ((𝑁 ∈ ℕ ∧ ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})) → ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}))
122, 11mpanr2 716 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}))
13 simpr1 1060 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → 𝑃 ∈ (𝔼‘𝑁))
14 simpr2 1061 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → 𝐴 ∈ (𝔼‘𝑁))
15 fvex 6113 . . . . . . 7 (𝔼‘𝑁) ∈ V
1615rabex 4740 . . . . . 6 {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} ∈ V
17 eleq1 2676 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑝 ∈ (𝔼‘𝑛) ↔ 𝑃 ∈ (𝔼‘𝑛)))
18 neeq1 2844 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑝𝑎𝑃𝑎))
1917, 183anbi13d 1393 . . . . . . . . 9 (𝑝 = 𝑃 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ↔ (𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃𝑎)))
20 breq1 4586 . . . . . . . . . . 11 (𝑝 = 𝑃 → (𝑝OutsideOf⟨𝑎, 𝑥⟩ ↔ 𝑃OutsideOf⟨𝑎, 𝑥⟩))
2120rabbidv 3164 . . . . . . . . . 10 (𝑝 = 𝑃 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩})
2221eqeq2d 2620 . . . . . . . . 9 (𝑝 = 𝑃 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩} ↔ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩}))
2319, 22anbi12d 743 . . . . . . . 8 (𝑝 = 𝑃 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩}) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩})))
2423rexbidv 3034 . . . . . . 7 (𝑝 = 𝑃 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩}) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩})))
25 eleq1 2676 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑎 ∈ (𝔼‘𝑛) ↔ 𝐴 ∈ (𝔼‘𝑛)))
26 neeq2 2845 . . . . . . . . . 10 (𝑎 = 𝐴 → (𝑃𝑎𝑃𝐴))
2725, 263anbi23d 1394 . . . . . . . . 9 (𝑎 = 𝐴 → ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃𝑎) ↔ (𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴)))
28 opeq1 4340 . . . . . . . . . . . 12 (𝑎 = 𝐴 → ⟨𝑎, 𝑥⟩ = ⟨𝐴, 𝑥⟩)
2928breq2d 4595 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑃OutsideOf⟨𝑎, 𝑥⟩ ↔ 𝑃OutsideOf⟨𝐴, 𝑥⟩))
3029rabbidv 3164 . . . . . . . . . 10 (𝑎 = 𝐴 → {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
3130eqeq2d 2620 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩} ↔ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}))
3227, 31anbi12d 743 . . . . . . . 8 (𝑎 = 𝐴 → (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩}) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
3332rexbidv 3034 . . . . . . 7 (𝑎 = 𝐴 → (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑃𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝑎, 𝑥⟩}) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
34 eqeq1 2614 . . . . . . . . 9 (𝑟 = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} → (𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} ↔ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}))
3534anbi2d 736 . . . . . . . 8 (𝑟 = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} → (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
3635rexbidv 3034 . . . . . . 7 (𝑟 = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} → (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
3724, 33, 36eloprabg 6646 . . . . . 6 ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} ∈ V) → (⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
3816, 37mp3an3 1405 . . . . 5 ((𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
3913, 14, 38syl2anc 691 . . . 4 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → (⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝐴 ∈ (𝔼‘𝑛) ∧ 𝑃𝐴) ∧ {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})))
4012, 39mpbird 246 . . 3 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → ⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})})
41 df-br 4584 . . . . 5 (⟨𝑃, 𝐴⟩Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} ↔ ⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ Ray)
42 df-ray 31415 . . . . . 6 Ray = {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})}
4342eleq2i 2680 . . . . 5 (⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ Ray ↔ ⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})})
4441, 43bitri 263 . . . 4 (⟨𝑃, 𝐴⟩Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} ↔ ⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})})
45 funray 31417 . . . . 5 Fun Ray
46 funbrfv 6144 . . . . 5 (Fun Ray → (⟨𝑃, 𝐴⟩Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} → (Ray‘⟨𝑃, 𝐴⟩) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}))
4745, 46ax-mp 5 . . . 4 (⟨𝑃, 𝐴⟩Ray{𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩} → (Ray‘⟨𝑃, 𝐴⟩) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
4844, 47sylbir 224 . . 3 (⟨⟨𝑃, 𝐴⟩, {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩}⟩ ∈ {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})} → (Ray‘⟨𝑃, 𝐴⟩) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
4940, 48syl 17 . 2 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → (Ray‘⟨𝑃, 𝐴⟩) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
501, 49syl5eq 2656 1 ((𝑁 ∈ ℕ ∧ (𝑃 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝑃𝐴)) → (𝑃Ray𝐴) = {𝑥 ∈ (𝔼‘𝑁) ∣ 𝑃OutsideOf⟨𝐴, 𝑥⟩})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  {crab 2900  Vcvv 3173  ⟨cop 4131   class class class wbr 4583  Fun wfun 5798  ‘cfv 5804  (class class class)co 6549  {coprab 6550  ℕcn 10897  𝔼cee 25568  OutsideOfcoutsideof 31396  Raycray 31412 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-z 11255  df-uz 11564  df-fz 12198  df-ee 25571  df-ray 31415 This theorem is referenced by:  lineunray  31424
 Copyright terms: Public domain W3C validator