Theorem axtgbtwnid 28548

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

Hypotheses

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

Assertion

Ref	Expression
axtgbtwnid	⊢ (𝜑 → 𝑋 = 𝑌)

Proof of Theorem axtgbtwnid

Dummy variables 𝑓 𝑖 𝑝 𝑥 𝑦 𝑧 𝑎 𝑏 𝑣 𝑠 𝑡 𝑢 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3062  {crab 3390  Vcvv 3430  [wsbc 3729   ∖ cdif 3887   ∩ cin 3889  𝒫 cpw 4542  {csn 4568  ‘cfv 6492  (class class class)co 7360   ∈ cmpo 7362  Basecbs 17170  distcds 17220  TarskiGcstrkg 28509  TarskiG_Ccstrkgc 28510  TarskiG_Bcstrkgb 28511  TarskiG_CBcstrkgcb 28512  Itvcitv 28515  LineGclng 28516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-trkgb 28531  df-trkg 28535

This theorem is referenced by:  tgbtwncom  28570  tgbtwnne  28572  tgbtwnswapid  28574  tgbtwnintr  28575  tgifscgr  28590  tgidinside  28653  tgbtwnconn1lem3  28656  coltr3  28730  mirinv  28748  miriso  28752  krippenlem  28772  midexlem  28774  colperpexlem3  28814  oppne3  28825  oppnid  28828  opphllem1  28829  hlpasch  28838  midid  28863  lmiisolem  28878  f1otrg  28953