Metamath Proof Explorer

Theorem btwnxfr

Description: A condition for extending betweenness to a new set of points based on congruence with another set of points. Theorem 4.6 of Schwabhauser p. 36. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion btwnxfr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B C Cgr3 D E F → E Btwn D F

Proof

Step Hyp Ref Expression
1 brcgr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ↔ A B Cgr D E ∧ A C Cgr D F ∧ B C Cgr E F
2 simp2 ⊢ A B Cgr D E ∧ A C Cgr D F ∧ B C Cgr E F → A C Cgr D F
3 1 2 biimtrdi ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D E F → A C Cgr D F
4 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → N ∈ ℕ
5 simp21 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
6 simp22 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
7 simp23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
8 simp31 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
9 simp33 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → F ∈ 𝔼 ⁡ N
10 cgrxfr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ A C Cgr D F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
11 4 5 6 7 8 9 10 syl132anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ A C Cgr D F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
12 3 11 sylan2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B C Cgr3 D E F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
13 12 imp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F
14 simprrl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → e Btwn D F
15 14 14 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → e Btwn D F ∧ e Btwn D F
16 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → N ∈ ℕ
17 simpl31 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
18 simpl33 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → F ∈ 𝔼 ⁡ N
19 16 17 18 cgrrflxd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D F Cgr D F
20 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → e ∈ 𝔼 ⁡ N
21 16 20 18 cgrrflxd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → e F Cgr e F
22 19 21 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D F Cgr D F ∧ e F Cgr e F
23 22 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → D F Cgr D F ∧ e F Cgr e F
24 simpr ⊢ B Btwn A C ∧ A B C Cgr3 D E F → A B C Cgr3 D E F
25 simpr ⊢ e Btwn D F ∧ A B C Cgr3 D e F → A B C Cgr3 D e F
26 simpl2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N
27 simpl3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N
28 17 20 18 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N
29 cgr3tr4 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ∧ A B C Cgr3 D e F → D E F Cgr3 D e F
30 16 26 27 28 29 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ∧ A B C Cgr3 D e F → D E F Cgr3 D e F
31 cgr3com ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → D E F Cgr3 D e F ↔ D e F Cgr3 D E F
32 16 27 17 20 18 31 syl113anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D E F Cgr3 D e F ↔ D e F Cgr3 D E F
33 simpl32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → E ∈ 𝔼 ⁡ N
34 brcgr3 ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → D e F Cgr3 D E F ↔ D e Cgr D E ∧ D F Cgr D F ∧ e F Cgr E F
35 16 17 20 18 17 33 18 34 syl133anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D e F Cgr3 D E F ↔ D e Cgr D E ∧ D F Cgr D F ∧ e F Cgr E F
36 simpr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ D e Cgr D E ∧ D F Cgr D F ∧ e F Cgr E F → D e Cgr D E
37 simpr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ D e Cgr D E ∧ D F Cgr D F ∧ e F Cgr E F → e F Cgr E F
38 16 20 18 33 18 37 cgrcomlrand ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ D e Cgr D E ∧ D F Cgr D F ∧ e F Cgr E F → F e Cgr F E
39 36 38 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ D e Cgr D E ∧ D F Cgr D F ∧ e F Cgr E F → D e Cgr D E ∧ F e Cgr F E
40 39 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D e Cgr D E ∧ D F Cgr D F ∧ e F Cgr E F → D e Cgr D E ∧ F e Cgr F E
41 35 40 sylbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D e F Cgr3 D E F → D e Cgr D E ∧ F e Cgr F E
42 32 41 sylbid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → D E F Cgr3 D e F → D e Cgr D E ∧ F e Cgr F E
43 30 42 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → A B C Cgr3 D E F ∧ A B C Cgr3 D e F → D e Cgr D E ∧ F e Cgr F E
44 24 25 43 syl2ani ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → D e Cgr D E ∧ F e Cgr F E
45 44 imp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → D e Cgr D E ∧ F e Cgr F E
46 15 23 45 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → e Btwn D F ∧ e Btwn D F ∧ D F Cgr D F ∧ e F Cgr e F ∧ D e Cgr D E ∧ F e Cgr F E
47 46 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → e Btwn D F ∧ e Btwn D F ∧ D F Cgr D F ∧ e F Cgr e F ∧ D e Cgr D E ∧ F e Cgr F E
48 brifs ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → D e F e InnerFiveSeg D e F E ↔ e Btwn D F ∧ e Btwn D F ∧ D F Cgr D F ∧ e F Cgr e F ∧ D e Cgr D E ∧ F e Cgr F E
49 ifscgr ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → D e F e InnerFiveSeg D e F E → e e Cgr e E
50 48 49 sylbird ⊢ N ∈ ℕ ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → e Btwn D F ∧ e Btwn D F ∧ D F Cgr D F ∧ e F Cgr e F ∧ D e Cgr D E ∧ F e Cgr F E → e e Cgr e E
51 16 17 20 18 20 17 20 18 33 50 syl333anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → e Btwn D F ∧ e Btwn D F ∧ D F Cgr D F ∧ e F Cgr e F ∧ D e Cgr D E ∧ F e Cgr F E → e e Cgr e E
52 47 51 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → e e Cgr e E
53 cgrid2 ⊢ N ∈ ℕ ∧ e ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N → e e Cgr e E → e = E
54 16 20 20 33 53 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → e e Cgr e E → e = E
55 52 54 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → e = E
56 55 imp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → e = E
57 56 14 eqbrtrrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e Btwn D F ∧ A B C Cgr3 D e F → E Btwn D F
58 57 expr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ e ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F → e Btwn D F ∧ A B C Cgr3 D e F → E Btwn D F
59 58 an32s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F ∧ e ∈ 𝔼 ⁡ N → e Btwn D F ∧ A B C Cgr3 D e F → E Btwn D F
60 59 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F → ∃ e ∈ 𝔼 ⁡ N e Btwn D F ∧ A B C Cgr3 D e F → E Btwn D F
61 13 60 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N ∧ B Btwn A C ∧ A B C Cgr3 D E F → E Btwn D F
62 61 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ E ∈ 𝔼 ⁡ N ∧ F ∈ 𝔼 ⁡ N → B Btwn A C ∧ A B C Cgr3 D E F → E Btwn D F