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

Theorem axtgsegcon 25408
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 25397 . . . . . 6 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 3867 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 3866 . . . . . . 7 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3645 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3668 . . . . 5 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3634 . . . 4 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . 7 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . 7 = (dist‘𝐺)
10 axtrkg.i . . . . . . 7 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 25400 . . . . . 6 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 479 . . . . 5 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simprd 478 . . . 4 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
147, 13syl 17 . . 3 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
15 axtgsegcon.1 . . . 4 (𝜑𝑋𝑃)
16 axtgsegcon.2 . . . 4 (𝜑𝑌𝑃)
17 oveq1 6697 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
1817eleq2d 2716 . . . . . . . 8 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
1918anbi1d 741 . . . . . . 7 (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
2019rexbidv 3081 . . . . . 6 (𝑥 = 𝑋 → (∃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
21202ralbidv 3018 . . . . 5 (𝑥 = 𝑋 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
22 eleq1 2718 . . . . . . . 8 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
23 oveq1 6697 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
2423eqeq1d 2653 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝑎 𝑏)))
2522, 24anbi12d 747 . . . . . . 7 (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2625rexbidv 3081 . . . . . 6 (𝑦 = 𝑌 → (∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
27262ralbidv 3018 . . . . 5 (𝑦 = 𝑌 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2821, 27rspc2v 3353 . . . 4 ((𝑋𝑃𝑌𝑃) → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2915, 16, 28syl2anc 694 . . 3 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
3014, 29mpd 15 . 2 (𝜑 → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)))
31 axtgsegcon.3 . . 3 (𝜑𝐴𝑃)
32 axtgsegcon.4 . . 3 (𝜑𝐵𝑃)
33 oveq1 6697 . . . . . . 7 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
3433eqeq2d 2661 . . . . . 6 (𝑎 = 𝐴 → ((𝑌 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝑏)))
3534anbi2d 740 . . . . 5 (𝑎 = 𝐴 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
3635rexbidv 3081 . . . 4 (𝑎 = 𝐴 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
37 oveq2 6698 . . . . . . 7 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
3837eqeq2d 2661 . . . . . 6 (𝑏 = 𝐵 → ((𝑌 𝑧) = (𝐴 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝐵)))
3938anbi2d 740 . . . . 5 (𝑏 = 𝐵 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4039rexbidv 3081 . . . 4 (𝑏 = 𝐵 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4136, 40rspc2v 3353 . . 3 ((𝐴𝑃𝐵𝑃) → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4231, 32, 41syl2anc 694 . 2 (𝜑 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4330, 42mpd 15 1 (𝜑 → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3o 1053  w3a 1054   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  [wsbc 3468  cdif 3604  cin 3606  {csn 4210  cfv 5926  (class class class)co 6690  cmpt2 6692  Basecbs 15904  distcds 15997  TarskiGcstrkg 25374  TarskiGCcstrkgc 25375  TarskiGBcstrkgb 25376  TarskiGCBcstrkgcb 25377  Itvcitv 25380  LineGclng 25381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-trkgcb 25394  df-trkg 25397
This theorem is referenced by:  tgcgrtriv  25424  tgbtwntriv2  25427  tgbtwnouttr2  25435  tgbtwndiff  25446  tgifscgr  25448  tgcgrxfr  25458  lnext  25507  tgbtwnconn1lem3  25514  tgbtwnconn1  25515  legtrid  25531  hlcgrex  25556  mirreu3  25594  miriso  25610  midexlem  25632  footex  25658  opphllem  25672  dfcgra2  25766  f1otrg  25796
  Copyright terms: Public domain W3C validator