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

Theorem axtgsegcon 25080
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 25069 . . . . . 6 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss2 3795 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3 inss1 3794 . . . . . . 7 (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
42, 3sstri 3576 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
51, 4eqsstri 3597 . . . . 5 TarskiG ⊆ TarskiGCB
6 axtrkg.g . . . . 5 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3565 . . . 4 (𝜑𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . 7 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . . 7 = (dist‘𝐺)
10 axtrkg.i . . . . . . 7 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgcb 25072 . . . . . 6 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))))
1211simprbi 478 . . . . 5 (𝐺 ∈ TarskiGCB → (∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑎𝑃𝑏𝑃𝑐𝑃𝑣𝑃 (((𝑥𝑦𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 𝑦) = (𝑎 𝑏) ∧ (𝑦 𝑧) = (𝑏 𝑐)) ∧ ((𝑥 𝑢) = (𝑎 𝑣) ∧ (𝑦 𝑢) = (𝑏 𝑣)))) → (𝑧 𝑢) = (𝑐 𝑣)) ∧ ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
1312simprd 477 . . . 4 (𝐺 ∈ TarskiGCB → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
147, 13syl 17 . . 3 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)))
15 axtgsegcon.1 . . . 4 (𝜑𝑋𝑃)
16 axtgsegcon.2 . . . 4 (𝜑𝑌𝑃)
17 oveq1 6534 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
1817eleq2d 2672 . . . . . . . 8 (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
1918anbi1d 736 . . . . . . 7 (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
2019rexbidv 3033 . . . . . 6 (𝑥 = 𝑋 → (∃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
21202ralbidv 2971 . . . . 5 (𝑥 = 𝑋 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏))))
22 eleq1 2675 . . . . . . . 8 (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
23 oveq1 6534 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 𝑧) = (𝑌 𝑧))
2423eqeq1d 2611 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑦 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝑎 𝑏)))
2522, 24anbi12d 742 . . . . . . 7 (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2625rexbidv 3033 . . . . . 6 (𝑦 = 𝑌 → (∃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
27262ralbidv 2971 . . . . 5 (𝑦 = 𝑌 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) ↔ ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2821, 27rspc2v 3292 . . . 4 ((𝑋𝑃𝑌𝑃) → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
2915, 16, 28syl2anc 690 . . 3 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑎𝑃𝑏𝑃𝑧𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 𝑧) = (𝑎 𝑏)) → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏))))
3014, 29mpd 15 . 2 (𝜑 → ∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)))
31 axtgsegcon.3 . . 3 (𝜑𝐴𝑃)
32 axtgsegcon.4 . . 3 (𝜑𝐵𝑃)
33 oveq1 6534 . . . . . . 7 (𝑎 = 𝐴 → (𝑎 𝑏) = (𝐴 𝑏))
3433eqeq2d 2619 . . . . . 6 (𝑎 = 𝐴 → ((𝑌 𝑧) = (𝑎 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝑏)))
3534anbi2d 735 . . . . 5 (𝑎 = 𝐴 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
3635rexbidv 3033 . . . 4 (𝑎 = 𝐴 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏))))
37 oveq2 6535 . . . . . . 7 (𝑏 = 𝐵 → (𝐴 𝑏) = (𝐴 𝐵))
3837eqeq2d 2619 . . . . . 6 (𝑏 = 𝐵 → ((𝑌 𝑧) = (𝐴 𝑏) ↔ (𝑌 𝑧) = (𝐴 𝐵)))
3938anbi2d 735 . . . . 5 (𝑏 = 𝐵 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4039rexbidv 3033 . . . 4 (𝑏 = 𝐵 → (∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝑏)) ↔ ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4136, 40rspc2v 3292 . . 3 ((𝐴𝑃𝐵𝑃) → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4231, 32, 41syl2anc 690 . 2 (𝜑 → (∀𝑎𝑃𝑏𝑃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝑎 𝑏)) → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵))))
4330, 42mpd 15 1 (𝜑 → ∃𝑧𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 𝑧) = (𝐴 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3o 1029  w3a 1030   = wceq 1474  wcel 1976  {cab 2595  wne 2779  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  [wsbc 3401  cdif 3536  cin 3538  {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 2032  ax-13 2232  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-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-trkgcb 25066  df-trkg 25069
This theorem is referenced by:  tgcgrtriv  25096  tgbtwntriv2  25099  tgbtwnouttr2  25107  tgbtwndiff  25118  tgifscgr  25121  tgcgrxfr  25131  lnext  25180  tgbtwnconn1lem3  25187  tgbtwnconn1  25188  legtrid  25204  hlcgrex  25229  mirreu3  25267  miriso  25283  midexlem  25305  footex  25331  opphllem  25345  dfcgra2  25439  f1otrg  25469
  Copyright terms: Public domain W3C validator