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

Theorem axtgsegcon 25815
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 25804 . . . . . 6 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 4053 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 4052 . . . . . . 7 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3829 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3853 . . . . 5 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3818 . . . 4 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . 7 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . 7 = (dist‘𝐺)
10 axtrkg.i . . . . . . 7 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 25807 . . . . . 6 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 492 . . . . 5 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simprd 491 . . . 4 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
147, 13syl 17 . . 3 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
15 axtgsegcon.1 . . . 4 (𝜑𝑋𝑃)
16 axtgsegcon.2 . . . 4 (𝜑𝑌𝑃)
17 oveq1 6929 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
1817eleq2d 2844 . . . . . . . 8 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
1918anbi1d 623 . . . . . . 7 (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
2019rexbidv 3236 . . . . . 6 (𝑥 = 𝑋 → (∃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
21202ralbidv 3170 . . . . 5 (𝑥 = 𝑋 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
22 eleq1 2846 . . . . . . . 8 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
23 oveq1 6929 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
2423eqeq1d 2779 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝑎 𝑏)))
2522, 24anbi12d 624 . . . . . . 7 (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2625rexbidv 3236 . . . . . 6 (𝑦 = 𝑌 → (∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
27262ralbidv 3170 . . . . 5 (𝑦 = 𝑌 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2821, 27rspc2v 3523 . . . 4 ((𝑋𝑃𝑌𝑃) → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2915, 16, 28syl2anc 579 . . 3 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
3014, 29mpd 15 . 2 (𝜑 → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)))
31 axtgsegcon.3 . . 3 (𝜑𝐴𝑃)
32 axtgsegcon.4 . . 3 (𝜑𝐵𝑃)
33 oveq1 6929 . . . . . . 7 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
3433eqeq2d 2787 . . . . . 6 (𝑎 = 𝐴 → ((𝑌 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝑏)))
3534anbi2d 622 . . . . 5 (𝑎 = 𝐴 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
3635rexbidv 3236 . . . 4 (𝑎 = 𝐴 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
37 oveq2 6930 . . . . . . 7 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
3837eqeq2d 2787 . . . . . 6 (𝑏 = 𝐵 → ((𝑌 𝑧) = (𝐴 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝐵)))
3938anbi2d 622 . . . . 5 (𝑏 = 𝐵 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4039rexbidv 3236 . . . 4 (𝑏 = 𝐵 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4136, 40rspc2v 3523 . . 3 ((𝐴𝑃𝐵𝑃) → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4231, 32, 41syl2anc 579 . 2 (𝜑 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4330, 42mpd 15 1 (𝜑 → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3o 1070  w3a 1071   = wceq 1601  wcel 2106  {cab 2762  wne 2968  wral 3089  wrex 3090  {crab 3093  Vcvv 3397  [wsbc 3651  cdif 3788  cin 3790  {csn 4397  cfv 6135  (class class class)co 6922  cmpt2 6924  Basecbs 16255  distcds 16347  TarskiGcstrkg 25781  TarskiGCcstrkgc 25782  TarskiGBcstrkgb 25783  TarskiGCBcstrkgcb 25784  Itvcitv 25787  LineGclng 25788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-nul 5025
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-trkgcb 25801  df-trkg 25804
This theorem is referenced by:  tgcgrtriv  25835  tgbtwntriv2  25838  tgbtwnouttr2  25846  tgbtwndiff  25857  tgifscgr  25859  tgcgrxfr  25869  lnext  25918  tgbtwnconn1lem3  25925  tgbtwnconn1  25926  legtrid  25942  hlcgrex  25967  mirreu3  26005  miriso  26021  midexlem  26043  footex  26069  opphllem  26083  flatcgra  26172  dfcgra2  26178  f1otrg  26220
  Copyright terms: Public domain W3C validator