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

Theorem axtgsegcon 28187
Description: Axiom of segment construction, Axiom A4 of [Schwabhauser] p. 11. As discussed in Axiom 4 of [Tarski1999] p. 178, "The intuitive content [is that] given any line segment 𝐴𝐵, one can construct a line segment congruent to it, starting at any point 𝑌 and going in the direction of any ray containing 𝑌. The ray is determined by the point 𝑌 and a second point 𝑋, the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point 𝑧 whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p 𝑃 = (Base‘𝐺)
axtrkg.d = (dist‘𝐺)
axtrkg.i 𝐼 = (Itv‘𝐺)
axtrkg.g (𝜑𝐺 ∈ TarskiG)
axtgsegcon.1 (𝜑𝑋𝑃)
axtgsegcon.2 (𝜑𝑌𝑃)
axtgsegcon.3 (𝜑𝐴𝑃)
axtgsegcon.4 (𝜑𝐵𝑃)
Assertion
Ref Expression
axtgsegcon (𝜑 → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵)))
Distinct variable groups:   𝑧,𝐴   𝑧,𝐵   𝑧,𝐼   𝑧,𝑃   𝑧,𝑋   𝑧,𝑌   𝑧,
Allowed substitution hints:   𝜑(𝑧)   𝐺(𝑧)

Proof of Theorem axtgsegcon
Dummy variables 𝑓 𝑖 𝑝 𝑥 𝑦 𝑎 𝑏 𝑐 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 28176 . . . . . 6 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 4222 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 4221 . . . . . . 7 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3984 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 4009 . . . . 5 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
75, 6sselid 3973 . . . 4 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . 7 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . 7 = (dist‘𝐺)
10 axtrkg.i . . . . . . 7 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 28179 . . . . . 6 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 496 . . . . 5 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simprd 495 . . . 4 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
147, 13syl 17 . . 3 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
15 axtgsegcon.1 . . . 4 (𝜑𝑋𝑃)
16 axtgsegcon.2 . . . 4 (𝜑𝑌𝑃)
17 oveq1 7409 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
1817eleq2d 2811 . . . . . . . 8 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
1918anbi1d 629 . . . . . . 7 (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
2019rexbidv 3170 . . . . . 6 (𝑥 = 𝑋 → (∃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
21202ralbidv 3210 . . . . 5 (𝑥 = 𝑋 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
22 eleq1 2813 . . . . . . . 8 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
23 oveq1 7409 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
2423eqeq1d 2726 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝑎 𝑏)))
2522, 24anbi12d 630 . . . . . . 7 (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2625rexbidv 3170 . . . . . 6 (𝑦 = 𝑌 → (∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
27262ralbidv 3210 . . . . 5 (𝑦 = 𝑌 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2821, 27rspc2v 3615 . . . 4 ((𝑋𝑃𝑌𝑃) → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2915, 16, 28syl2anc 583 . . 3 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
3014, 29mpd 15 . 2 (𝜑 → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)))
31 axtgsegcon.3 . . 3 (𝜑𝐴𝑃)
32 axtgsegcon.4 . . 3 (𝜑𝐵𝑃)
33 oveq1 7409 . . . . . . 7 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
3433eqeq2d 2735 . . . . . 6 (𝑎 = 𝐴 → ((𝑌 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝑏)))
3534anbi2d 628 . . . . 5 (𝑎 = 𝐴 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
3635rexbidv 3170 . . . 4 (𝑎 = 𝐴 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
37 oveq2 7410 . . . . . . 7 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
3837eqeq2d 2735 . . . . . 6 (𝑏 = 𝐵 → ((𝑌 𝑧) = (𝐴 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝐵)))
3938anbi2d 628 . . . . 5 (𝑏 = 𝐵 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4039rexbidv 3170 . . . 4 (𝑏 = 𝐵 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4136, 40rspc2v 3615 . . 3 ((𝐴𝑃𝐵𝑃) → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4231, 32, 41syl2anc 583 . 2 (𝜑 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4330, 42mpd 15 1 (𝜑 → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3o 1083  w3a 1084   = wceq 1533  wcel 2098  {cab 2701  wne 2932  wral 3053  wrex 3062  {crab 3424  Vcvv 3466  [wsbc 3770  cdif 3938  cin 3940  {csn 4621  cfv 6534  (class class class)co 7402  cmpo 7404  Basecbs 17145  distcds 17207  TarskiGcstrkg 28150  TarskiGCcstrkgc 28151  TarskiGBcstrkgb 28152  TarskiGCBcstrkgcb 28153  Itvcitv 28156  LineGclng 28157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5297
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-iota 6486  df-fv 6542  df-ov 7405  df-trkgcb 28173  df-trkg 28176
This theorem is referenced by:  tgcgrtriv  28207  tgbtwntriv2  28210  tgbtwnouttr2  28218  tgbtwndiff  28229  tgifscgr  28231  tgcgrxfr  28241  lnext  28290  tgbtwnconn1lem3  28297  tgbtwnconn1  28298  legtrid  28314  hlcgrex  28339  mirreu3  28377  miriso  28393  midexlem  28415  footexALT  28441  footex  28444  opphllem  28458  flatcgra  28547  dfcgra2  28553  f1otrg  28594
  Copyright terms: Public domain W3C validator