Metamath Proof Explorer

Theorem funray

Description: Show that the Ray relationship is a function. (Contributed by Scott Fenton, 21-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion funray Fun Ray

Proof

Step Hyp Ref Expression
1 reeanv ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) ↔ ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
2 simp1 ⊢ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) → 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) )
3 simp1 ⊢ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) → 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) )
4 axdimuniq ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ) ) → 𝑛 = 𝑚 )
5 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑚 ) )
6 rabeq ⊢ ( ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑚 ) → { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } )
7 5 6 syl ⊢ ( 𝑛 = 𝑚 → { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } )
8 7 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ↔ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) )
9 8 anbi1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
10 eqtr3 ⊢ ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) → 𝑟 = 𝑠 )
11 9 10 biimtrdi ⊢ ( 𝑛 = 𝑚 → ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) → 𝑟 = 𝑠 ) )
12 4 11 syl ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ) ) → ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) → 𝑟 = 𝑠 ) )
13 12 an4s ⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ) ) → ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) → 𝑟 = 𝑠 ) )
14 13 ex ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ) → ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) → 𝑟 = 𝑠 ) ) )
15 14 com3l ⊢ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ) → ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) → ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → 𝑟 = 𝑠 ) ) )
16 2 3 15 syl2an ⊢ ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ) → ( ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) → ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → 𝑟 = 𝑠 ) ) )
17 16 imp ⊢ ( ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ) ∧ ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) → ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → 𝑟 = 𝑠 ) )
18 17 an4s ⊢ ( ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) → ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → 𝑟 = 𝑠 ) )
19 18 com12 ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) → 𝑟 = 𝑠 ) )
20 19 rexlimivv ⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) → 𝑟 = 𝑠 )
21 1 20 sylbir ⊢ ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) → 𝑟 = 𝑠 )
22 21 gen2 ⊢ ∀ 𝑟 ∀ 𝑠 ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) → 𝑟 = 𝑠 )
23 eqeq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ↔ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) )
24 23 anbi2d ⊢ ( 𝑟 = 𝑠 → ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
25 24 rexbidv ⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
26 5 eleq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ) )
27 5 eleq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ) )
28 26 27 3anbi12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ↔ ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ) )
29 7 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ↔ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) )
30 28 29 anbi12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
31 30 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) )
32 25 31 bitrdi ⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) )
33 32 mo4 ⊢ ( ∃* 𝑟 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ↔ ∀ 𝑟 ∀ 𝑠 ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑠 = { 𝑥 ∈ ( 𝔼 ‘ 𝑚 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) ) → 𝑟 = 𝑠 ) )
34 22 33 mpbir ⊢ ∃* 𝑟 ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } )
35 34 funoprab ⊢ Fun { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) }
36 df-ray ⊢ Ray = { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) }
37 36 funeqi ⊢ ( Fun Ray ↔ Fun { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) } )
38 35 37 mpbir ⊢ Fun Ray