Theorem axtgbtwnid

Description: Identity of Betweenness. Axiom A6 of Schwabhauser p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	axtrkg.d	⊢ − = ( dist ‘ 𝐺 )
	axtrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	axtrkg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	axtgbtwnid.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	axtgbtwnid.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	axtgbtwnid.3	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) )
Assertion	axtgbtwnid	⊢ ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		axtrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		axtrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		axtrkg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		axtgbtwnid.1	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6		axtgbtwnid.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7		axtgbtwnid.3	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) )
8		df-trkg	⊢ TarskiG = ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) )
9		inss1	⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ ( TarskiGC ∩ TarskiGB )
10		inss2	⊢ ( TarskiGC ∩ TarskiGB ) ⊆ TarskiGB
11	9 10	sstri	⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ TarskiGB
12	8 11	eqsstri	⊢ TarskiG ⊆ TarskiGB
13	12 4	sselid	⊢ ( 𝜑 → 𝐺 ∈ TarskiGB )
14	1 2 3	istrkgb	⊢ ( 𝐺 ∈ TarskiGB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )
15	14	simprbi	⊢ ( 𝐺 ∈ TarskiGB → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
16	15	simp1d	⊢ ( 𝐺 ∈ TarskiGB → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) )
17	13 16	syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) )
18		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
19	18 18	oveq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑥 ) = ( 𝑋 𝐼 𝑋 ) )
20	19	eleq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) ↔ 𝑦 ∈ ( 𝑋 𝐼 𝑋 ) ) )
21		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑦 ) )
22	20 21	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( 𝑦 ∈ ( 𝑋 𝐼 𝑋 ) → 𝑋 = 𝑦 ) ) )
23		eleq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ ( 𝑋 𝐼 𝑋 ) ↔ 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) ) )
24		eqeq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑌 ) )
25	23 24	imbi12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 ∈ ( 𝑋 𝐼 𝑋 ) → 𝑋 = 𝑦 ) ↔ ( 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) → 𝑋 = 𝑌 ) ) )
26	22 25	rspc2v	⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) → ( 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) → 𝑋 = 𝑌 ) ) )
27	5 6 26	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) → ( 𝑌 ∈ ( 𝑋 𝐼 𝑋 ) → 𝑋 = 𝑌 ) ) )
28	17 7 27	mp2d	⊢ ( 𝜑 → 𝑋 = 𝑌 )