Metamath Proof Explorer

Theorem lnext

Description: Extend a line with a missing point. Theorem 4.14 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019)

Ref Expression
Hypotheses tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
lnxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
lnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
lnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
lnxfr.d ⊢ − = ( dist ‘ 𝐺 )
lnext.1 ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
lnext.2 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝐴 − 𝐵 ) )
Assertion lnext ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )

Proof

Step Hyp Ref Expression
1 tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 lnxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
9 lnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 lnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
11 lnxfr.d ⊢ − = ( dist ‘ 𝐺 )
12 lnext.1 ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
13 lnext.2 ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝐴 − 𝐵 ) )
14 1 11 3 4 9 10 6 7 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) )
16 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝐺 ∈ TarskiG )
17 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝑋 ∈ 𝑃 )
18 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝑌 ∈ 𝑃 )
19 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝑍 ∈ 𝑃 )
20 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝐴 ∈ 𝑃 )
21 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝐵 ∈ 𝑃 )
22 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝑐 ∈ 𝑃 )
23 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → ( 𝑋 − 𝑌 ) = ( 𝐴 − 𝐵 ) )
24 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) )
25 24 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → ( 𝑌 − 𝑍 ) = ( 𝐵 − 𝑐 ) )
26 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
27 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) )
28 1 11 3 16 17 18 19 20 21 22 26 27 23 25 tgcgrextend ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → ( 𝑋 − 𝑍 ) = ( 𝐴 − 𝑐 ) )
29 1 11 3 16 17 19 20 22 28 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → ( 𝑍 − 𝑋 ) = ( 𝑐 − 𝐴 ) )
30 1 11 8 16 17 18 19 20 21 22 23 25 29 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )
31 30 ex ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) )
32 31 reximdva ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( ∃ 𝑐 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑐 ) ∧ ( 𝐵 − 𝑐 ) = ( 𝑌 − 𝑍 ) ) → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) )
33 15 32 mpd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ) → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )
34 1 11 3 4 10 9 5 7 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑐 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) )
36 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝐺 ∈ TarskiG )
37 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝑋 ∈ 𝑃 )
38 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝑌 ∈ 𝑃 )
39 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝑍 ∈ 𝑃 )
40 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝐴 ∈ 𝑃 )
41 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝐵 ∈ 𝑃 )
42 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝑐 ∈ 𝑃 )
43 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → ( 𝑋 − 𝑌 ) = ( 𝐴 − 𝐵 ) )
44 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) )
45 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) )
46 1 11 3 36 37 38 40 41 43 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → ( 𝑌 − 𝑋 ) = ( 𝐵 − 𝐴 ) )
47 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) )
48 47 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → ( 𝑋 − 𝑍 ) = ( 𝐴 − 𝑐 ) )
49 1 11 3 36 38 37 39 41 40 42 44 45 46 48 tgcgrextend ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → ( 𝑌 − 𝑍 ) = ( 𝐵 − 𝑐 ) )
50 1 11 3 36 37 39 40 42 48 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → ( 𝑍 − 𝑋 ) = ( 𝑐 − 𝐴 ) )
51 1 11 8 36 37 38 39 40 41 42 43 49 50 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )
52 51 ex ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) )
53 52 reximdva ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ( ∃ 𝑐 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑐 ) ∧ ( 𝐴 − 𝑐 ) = ( 𝑋 − 𝑍 ) ) → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) )
54 35 53 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )
55 4 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐺 ∈ TarskiG )
56 5 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑋 ∈ 𝑃 )
57 7 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑍 ∈ 𝑃 )
58 6 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑌 ∈ 𝑃 )
59 9 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐴 ∈ 𝑃 )
60 10 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐵 ∈ 𝑃 )
61 simpr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) )
62 13 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑋 − 𝑌 ) = ( 𝐴 − 𝐵 ) )
63 1 11 3 8 55 56 57 58 59 60 61 62 tgcgrxfr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ∃ 𝑐 ∈ 𝑃 ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) )
64 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → 𝐺 ∈ TarskiG )
65 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → 𝑋 ∈ 𝑃 )
66 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → 𝑍 ∈ 𝑃 )
67 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → 𝑌 ∈ 𝑃 )
68 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → 𝐴 ∈ 𝑃 )
69 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → 𝑐 ∈ 𝑃 )
70 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → 𝐵 ∈ 𝑃 )
71 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ )
72 1 11 3 8 64 65 66 67 68 69 70 71 cgr3swap23 ⊢ ( ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )
73 72 ex ⊢ ( ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) )
74 73 reximdva ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ∃ 𝑐 ∈ 𝑃 ( 𝑐 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ⟨“ 𝑋 𝑍 𝑌 ”⟩ ∼ ⟨“ 𝐴 𝑐 𝐵 ”⟩ ) → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ ) )
75 63 74 mpd ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )
76 1 2 3 4 5 7 6 tgcolg ⊢ ( 𝜑 → ( ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) ↔ ( 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ∨ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ∨ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ) )
77 12 76 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) ∨ 𝑋 ∈ ( 𝑌 𝐼 𝑍 ) ∨ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )
78 33 54 75 77 mpjao3dan ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝐴 𝐵 𝑐 ”⟩ )