Metamath Proof Explorer

Theorem btwnouttr2

Description: Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwnouttr2 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
5 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
6 1 2 3 3 4 5 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
8 simprrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ )
9 simprl1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → 𝐵 ≠ 𝐶 )
10 simpl2 ⊢ ( ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ )
11 simprl ⊢ ( ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ )
12 10 11 jca ⊢ ( ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
13 12 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
14 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
15 simpl2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
16 simpl2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
18 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
19 btwnexch3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ ) )
20 14 15 16 17 18 19 syl122anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ ) )
21 20 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) → 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ ) )
22 13 21 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ )
23 simprrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
24 22 23 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
25 simprl3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ )
26 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
27 14 17 26 cgrrflxd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
28 27 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ )
29 25 28 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ( 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
30 segconeq ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ ( 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝑥 = 𝐷 ) )
31 14 17 17 26 16 18 26 30 syl133anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 ≠ 𝐶 ∧ ( 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝑥 = 𝐷 ) )
32 31 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ ( 𝐶 Btwn ⟨ 𝐵 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) → 𝑥 = 𝐷 ) )
33 9 24 29 32 mp3and ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → 𝑥 = 𝐷 )
34 33 opeq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → ⟨ 𝐴 , 𝑥 ⟩ = ⟨ 𝐴 , 𝐷 ⟩ )
35 8 34 breqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ∧ ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
36 35 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
37 36 an32s ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
38 37 rexlimdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐶 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐶 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
39 7 38 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
40 39 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐵 , 𝐷 ⟩ ) → 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )