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

Theorem axtgpasch 23990
 Description: Axiom of (Inner) Pasch, Axiom A7 of [Schwabhauser] p. 12. Given triangle , point in segment , and point in segment , there exists a point on both the segment and the segment . This axiom is essentially a subset of the general Pasch axiom. The general Pasch axiom asserts that on a plane "a line intersecting a triangle in one of its sides, and not intersecting any of the vertices, must intersect one of the other two sides" (per the discussion about Axiom 7 of [Tarski1999] p. 179). The (general) Pasch axiom was used implicitly by Euclid, but never stated; Moritz Pasch discovered its omission in 1882. As noted in the Metamath book, this means that the omission of Pasch's axiom from Euclid went unnoticed for 2000 years. Only the inner Pasch algorithm is included as an axiom; the "outer" form of the Pasch axiom can be proved using the inner form (see theorem 9.6 of [Schwabhauser] p. 69 and the brief discussion in axiom 7.1 of [Tarski1999] p. 180). (Contributed by Thierry Arnoux, 15-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p
axtrkg.d
axtrkg.i Itv
axtrkg.g TarskiG
axtgpasch.1
axtgpasch.2
axtgpasch.3
axtgpasch.4
axtgpasch.5
axtgpasch.6
axtgpasch.7
Assertion
Ref Expression
axtgpasch
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem axtgpasch
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgpasch.6 . 2
2 axtgpasch.7 . 2
3 df-trkg 23976 . . . . . . 7 TarskiG TarskiGC TarskiGB TarskiGCB Itv LineG
4 inss1 3714 . . . . . . . 8 TarskiGC TarskiGB TarskiGCB Itv LineG TarskiGC TarskiGB
5 inss2 3715 . . . . . . . 8 TarskiGC TarskiGB TarskiGB
64, 5sstri 3508 . . . . . . 7 TarskiGC TarskiGB TarskiGCB Itv LineG TarskiGB
73, 6eqsstri 3529 . . . . . 6 TarskiG TarskiGB
8 axtrkg.g . . . . . 6 TarskiG
97, 8sseldi 3497 . . . . 5 TarskiGB
10 axtrkg.p . . . . . . . 8
11 axtrkg.d . . . . . . . 8
12 axtrkg.i . . . . . . . 8 Itv
1310, 11, 12istrkgb 23978 . . . . . . 7 TarskiGB
1413simprbi 464 . . . . . 6 TarskiGB
1514simp2d 1009 . . . . 5 TarskiGB
169, 15syl 16 . . . 4
17 axtgpasch.1 . . . . 5
18 axtgpasch.2 . . . . 5
19 axtgpasch.3 . . . . 5
20 oveq1 6303 . . . . . . . . . 10
2120eleq2d 2527 . . . . . . . . 9
2221anbi1d 704 . . . . . . . 8
23 oveq2 6304 . . . . . . . . . . 11
2423eleq2d 2527 . . . . . . . . . 10
2524anbi2d 703 . . . . . . . . 9
2625rexbidv 2968 . . . . . . . 8
2722, 26imbi12d 320 . . . . . . 7
28272ralbidv 2901 . . . . . 6
29 oveq1 6303 . . . . . . . . . 10
3029eleq2d 2527 . . . . . . . . 9
3130anbi2d 703 . . . . . . . 8
32 oveq2 6304 . . . . . . . . . . 11
3332eleq2d 2527 . . . . . . . . . 10
3433anbi1d 704 . . . . . . . . 9
3534rexbidv 2968 . . . . . . . 8
3631, 35imbi12d 320 . . . . . . 7
37362ralbidv 2901 . . . . . 6
38 oveq2 6304 . . . . . . . . . 10
3938eleq2d 2527 . . . . . . . . 9
40 oveq2 6304 . . . . . . . . . 10
4140eleq2d 2527 . . . . . . . . 9
4239, 41anbi12d 710 . . . . . . . 8
4342imbi1d 317 . . . . . . 7
44432ralbidv 2901 . . . . . 6
4528, 37, 44rspc3v 3222 . . . . 5
4617, 18, 19, 45syl3anc 1228 . . . 4
4716, 46mpd 15 . . 3
48 axtgpasch.4 . . . 4
49 axtgpasch.5 . . . 4
50 eleq1 2529 . . . . . . 7
5150anbi1d 704 . . . . . 6
52 oveq1 6303 . . . . . . . . 9
5352eleq2d 2527 . . . . . . . 8
5453anbi1d 704 . . . . . . 7
5554rexbidv 2968 . . . . . 6
5651, 55imbi12d 320 . . . . 5
57 eleq1 2529 . . . . . . 7
5857anbi2d 703 . . . . . 6
59 oveq1 6303 . . . . . . . . 9
6059eleq2d 2527 . . . . . . . 8
6160anbi2d 703 . . . . . . 7
6261rexbidv 2968 . . . . . 6
6358, 62imbi12d 320 . . . . 5
6456, 63rspc2v 3219 . . . 4
6548, 49, 64syl2anc 661 . . 3
6647, 65mpd 15 . 2
671, 2, 66mp2and 679 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3o 972   w3a 973   wceq 1395   wcel 1819  cab 2442  wral 2807  wrex 2808  crab 2811  cvv 3109  wsbc 3327   cdif 3468   cin 3470  cpw 4015  csn 4032  cfv 5594  (class class class)co 6296   cmpt2 6298  cbs 14644  cds 14721  TarskiGcstrkg 23951  TarskiGCcstrkgc 23952  TarskiGBcstrkgb 23953  TarskiGCBcstrkgcb 23954  Itvcitv 23958  LineGclng 23959 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-nul 4586 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299  df-trkgb 23971  df-trkg 23976 This theorem is referenced by:  tgbtwncom  24005  tgbtwnswapid  24009  tgbtwnintr  24010  tgtrisegint  24016  tgbtwnconn1  24088  midexlem  24195  opphllem  24235  opphllem1  24245  lnopp2hpgb  24258  f1otrg  24301
 Copyright terms: Public domain W3C validator