MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtgbtwnid Structured version   Visualization version   GIF version

Theorem axtgbtwnid 25082
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.
StepHypRef Expression
1 df-trkg 25069 . . . . 5 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss1 3794 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3 inss2 3795 . . . . . 6 (TarskiGC ∩ TarskiGB) ⊆ TarskiGB
42, 3sstri 3576 . . . . 5 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGB
51, 4eqsstri 3597 . . . 4 TarskiG ⊆ TarskiGB
6 axtrkg.g . . . 4 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3565 . . 3 (𝜑𝐺 ∈ TarskiGB)
8 axtrkg.p . . . . . 6 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . 6 = (dist‘𝐺)
10 axtrkg.i . . . . . 6 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgb 25071 . . . . 5 (𝐺 ∈ TarskiGB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))))
1211simprbi 478 . . . 4 (𝐺 ∈ TarskiGB → (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦))))
1312simp1d 1065 . . 3 (𝐺 ∈ TarskiGB → ∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦))
147, 13syl 17 . 2 (𝜑 → ∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦))
15 axtgbtwnid.3 . 2 (𝜑𝑌 ∈ (𝑋𝐼𝑋))
16 axtgbtwnid.1 . . 3 (𝜑𝑋𝑃)
17 axtgbtwnid.2 . . 3 (𝜑𝑌𝑃)
18 id 22 . . . . . . 7 (𝑥 = 𝑋𝑥 = 𝑋)
1918, 18oveq12d 6545 . . . . . 6 (𝑥 = 𝑋 → (𝑥𝐼𝑥) = (𝑋𝐼𝑋))
2019eleq2d 2672 . . . . 5 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑥) ↔ 𝑦 ∈ (𝑋𝐼𝑋)))
21 eqeq1 2613 . . . . 5 (𝑥 = 𝑋 → (𝑥 = 𝑦𝑋 = 𝑦))
2220, 21imbi12d 332 . . . 4 (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ↔ (𝑦 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑦)))
23 eleq1 2675 . . . . 5 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑋) ↔ 𝑌 ∈ (𝑋𝐼𝑋)))
24 eqeq2 2620 . . . . 5 (𝑦 = 𝑌 → (𝑋 = 𝑦𝑋 = 𝑌))
2523, 24imbi12d 332 . . . 4 (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑦) ↔ (𝑌 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑌)))
2622, 25rspc2v 3292 . . 3 ((𝑋𝑃𝑌𝑃) → (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) → (𝑌 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑌)))
2716, 17, 26syl2anc 690 . 2 (𝜑 → (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) → (𝑌 ∈ (𝑋𝐼𝑋) → 𝑋 = 𝑌)))
2814, 15, 27mp2d 46 1 (𝜑𝑋 = 𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3o 1029  w3a 1030   = wceq 1474  wcel 1976  {cab 2595  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  [wsbc 3401  cdif 3536  cin 3538  𝒫 cpw 4107  {csn 4124  cfv 5790  (class class class)co 6527  cmpt2 6529  Basecbs 15641  distcds 15723  TarskiGcstrkg 25046  TarskiGCcstrkgc 25047  TarskiGBcstrkgb 25048  TarskiGCBcstrkgcb 25049  Itvcitv 25052  LineGclng 25053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-nul 4712
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-trkgb 25065  df-trkg 25069
This theorem is referenced by:  tgbtwncom  25100  tgbtwnne  25102  tgbtwnswapid  25104  tgbtwnintr  25105  tgifscgr  25121  tgidinside  25184  tgbtwnconn1lem3  25187  coltr3  25261  mirinv  25279  miriso  25283  krippenlem  25303  midexlem  25305  colperpexlem3  25342  oppne3  25353  oppnid  25356  opphllem1  25357  hlpasch  25366  midid  25391  lmiisolem  25406  f1otrg  25469
  Copyright terms: Public domain W3C validator