Metamath Proof Explorer

Theorem segconeu

Description: Existential uniqueness version of segconeq . (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion segconeu ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ∃! 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → 𝑁 ∈ ℕ )
2 simpr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) )
3 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
4 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
5 1 2 3 4 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
6 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → 𝐶 ≠ 𝐷 )
7 simprl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
8 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
9 6 7 8 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) → ( 𝐶 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
10 9 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝐶 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
11 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
12 simp22r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
13 simp21l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
14 simp21r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
15 simp22l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
16 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) )
18 segconeq ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝑟 = 𝑠 ) )
19 11 12 13 14 15 16 17 18 syl133anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐶 ≠ 𝐷 ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝑟 = 𝑠 ) )
20 10 19 syld ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝑟 = 𝑠 ) )
21 20 3expa ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) ∧ ( 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝑟 = 𝑠 ) )
22 21 ralrimivva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ∀ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ( ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝑟 = 𝑠 ) )
23 opeq2 ⊢ ( 𝑟 = 𝑠 → ⟨ 𝐶 , 𝑟 ⟩ = ⟨ 𝐶 , 𝑠 ⟩ )
24 23 breq2d ⊢ ( 𝑟 = 𝑠 → ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ↔ 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ) )
25 opeq2 ⊢ ( 𝑟 = 𝑠 → ⟨ 𝐷 , 𝑟 ⟩ = ⟨ 𝐷 , 𝑠 ⟩ )
26 25 breq1d ⊢ ( 𝑟 = 𝑠 → ( ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )
27 24 26 anbi12d ⊢ ( 𝑟 = 𝑠 → ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) )
28 27 reu4 ⊢ ( ∃! 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( ∃ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ∀ 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑠 ∈ ( 𝔼 ‘ 𝑁 ) ( ( ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐷 Btwn ⟨ 𝐶 , 𝑠 ⟩ ∧ ⟨ 𝐷 , 𝑠 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝑟 = 𝑠 ) ) )
29 5 22 28 sylanbrc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝐶 ≠ 𝐷 ) ) → ∃! 𝑟 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐷 Btwn ⟨ 𝐶 , 𝑟 ⟩ ∧ ⟨ 𝐷 , 𝑟 ⟩ Cgr ⟨ 𝐴 , 𝐵 ⟩ ) )