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

Theorem axtgsegcon 24375
 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
axtrkg.d
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 24364 . . . . . 6 TarskiG TarskiGC TarskiGB TarskiGCB Itv LineG
2 inss2 3689 . . . . . . 7 TarskiGC TarskiGB TarskiGCB Itv LineG TarskiGCB Itv LineG
3 inss1 3688 . . . . . . 7 TarskiGCB Itv LineG TarskiGCB
42, 3sstri 3479 . . . . . 6 TarskiGC TarskiGB TarskiGCB Itv LineG TarskiGCB
51, 4eqsstri 3500 . . . . 5 TarskiG TarskiGCB
6 axtrkg.g . . . . 5 TarskiG
75, 6sseldi 3468 . . . 4 TarskiGCB
8 axtrkg.p . . . . . . 7
9 axtrkg.d . . . . . . 7
10 axtrkg.i . . . . . . 7 Itv
118, 9, 10istrkgcb 24367 . . . . . 6 TarskiGCB
1211simprbi 465 . . . . 5 TarskiGCB
1312simprd 464 . . . 4 TarskiGCB
147, 13syl 17 . . 3
15 axtgsegcon.1 . . . 4
16 axtgsegcon.2 . . . 4
17 oveq1 6312 . . . . . . . . 9
1817eleq2d 2499 . . . . . . . 8
1918anbi1d 709 . . . . . . 7
2019rexbidv 2946 . . . . . 6
21202ralbidv 2876 . . . . 5
22 eleq1 2501 . . . . . . . 8
23 oveq1 6312 . . . . . . . . 9
2423eqeq1d 2431 . . . . . . . 8
2522, 24anbi12d 715 . . . . . . 7
2625rexbidv 2946 . . . . . 6
27262ralbidv 2876 . . . . 5
2821, 27rspc2v 3197 . . . 4
2915, 16, 28syl2anc 665 . . 3
3014, 29mpd 15 . 2
31 axtgsegcon.3 . . 3
32 axtgsegcon.4 . . 3
33 oveq1 6312 . . . . . . 7
3433eqeq2d 2443 . . . . . 6
3534anbi2d 708 . . . . 5
3635rexbidv 2946 . . . 4
37 oveq2 6313 . . . . . . 7
3837eqeq2d 2443 . . . . . 6
3938anbi2d 708 . . . . 5
4039rexbidv 2946 . . . 4
4136, 40rspc2v 3197 . . 3
4231, 32, 41syl2anc 665 . 2
4330, 42mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3o 981   w3a 982   wceq 1437   wcel 1870  cab 2414   wne 2625  wral 2782  wrex 2783  crab 2786  cvv 3087  wsbc 3305   cdif 3439   cin 3441  csn 4002  cfv 5601  (class class class)co 6305   cmpt2 6307  cbs 15084  cds 15161  TarskiGcstrkg 24341  TarskiGCcstrkgc 24342  TarskiGBcstrkgb 24343  TarskiGCBcstrkgcb 24344  Itvcitv 24347  LineGclng 24348 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-trkgcb 24361  df-trkg 24364 This theorem is referenced by:  tgcgrtriv  24391  tgbtwntriv2  24394  tgbtwnouttr2  24402  tgbtwndiff  24413  tgifscgr  24416  tgcgrxfr  24425  lnext  24472  tgbtwnconn1lem3  24479  tgbtwnconn1  24480  legtrid  24496  hlcgrex  24520  mirreu3  24559  miriso  24574  midexlem  24594  footex  24620  opphllem  24634  dfcgra2  24726  f1otrg  24747
 Copyright terms: Public domain W3C validator