Metamath Proof Explorer

Theorem fvray

Description: Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fvray ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → ( 𝑃 Ray 𝐴 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )

Proof

Step Hyp Ref Expression
1 df-ov ⊢ ( 𝑃 Ray 𝐴 ) = ( Ray ‘ ⟨ 𝑃 , 𝐴 ⟩ )
2 eqid ⊢ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ }
3 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
4 3 eleq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ) )
5 3 eleq2d ⊢ ( 𝑛 = 𝑁 → ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
6 4 5 3anbi12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) )
7 rabeq ⊢ ( ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) → { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )
8 3 7 syl ⊢ ( 𝑛 = 𝑁 → { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )
9 8 eqeq2d ⊢ ( 𝑛 = 𝑁 → ( { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ↔ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) )
10 6 9 anbi12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ↔ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
11 10 rspcev ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) )
12 2 11 mpanr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) )
13 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
14 simpr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
15 fvex ⊢ ( 𝔼 ‘ 𝑁 ) ∈ V
16 15 rabex ⊢ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ∈ V
17 eleq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ) )
18 neeq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≠ 𝑎 ↔ 𝑃 ≠ 𝑎 ) )
19 17 18 3anbi13d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝑎 ) ) )
20 breq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ ) )
21 20 rabbidv ⊢ ( 𝑝 = 𝑃 → { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } )
22 21 eqeq2d ⊢ ( 𝑝 = 𝑃 → ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ↔ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) )
23 19 22 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
24 23 rexbidv ⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
25 eleq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) )
26 neeq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑃 ≠ 𝑎 ↔ 𝑃 ≠ 𝐴 ) )
27 25 26 3anbi23d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝑎 ) ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ) )
28 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑥 ⟩ = ⟨ 𝐴 , 𝑥 ⟩ )
29 28 breq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ ↔ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ ) )
30 29 rabbidv ⊢ ( 𝑎 = 𝐴 → { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )
31 30 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ↔ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) )
32 27 31 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
33 32 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
34 eqeq1 ⊢ ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } → ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ↔ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) )
35 34 anbi2d ⊢ ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } → ( ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ↔ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
36 35 rexbidv ⊢ ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } → ( ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
37 24 33 36 eloprabg ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ∈ V ) → ( ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
38 16 37 mp3an3 ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
39 13 14 38 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → ( ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑃 ≠ 𝐴 ) ∧ { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) ) )
40 12 39 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } )
41 df-br ⊢ ( ⟨ 𝑃 , 𝐴 ⟩ Ray { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ↔ ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ Ray )
42 df-ray ⊢ Ray = { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) }
43 42 eleq2i ⊢ ( ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ Ray ↔ ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } )
44 41 43 bitri ⊢ ( ⟨ 𝑃 , 𝐴 ⟩ Ray { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ↔ ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } )
45 funray ⊢ Fun Ray
46 funbrfv ⊢ ( Fun Ray → ( ⟨ 𝑃 , 𝐴 ⟩ Ray { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } → ( Ray ‘ ⟨ 𝑃 , 𝐴 ⟩ ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ) )
47 45 46 ax-mp ⊢ ( ⟨ 𝑃 , 𝐴 ⟩ Ray { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } → ( Ray ‘ ⟨ 𝑃 , 𝐴 ⟩ ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )
48 44 47 sylbir ⊢ ( ⟨ ⟨ 𝑃 , 𝐴 ⟩ , { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } ⟩ ∈ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } → ( Ray ‘ ⟨ 𝑃 , 𝐴 ⟩ ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )
49 40 48 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → ( Ray ‘ ⟨ 𝑃 , 𝐴 ⟩ ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )
50 1 49 syl5eq ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝐴 ) ) → ( 𝑃 Ray 𝐴 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑃 OutsideOf ⟨ 𝐴 , 𝑥 ⟩ } )