Metamath Proof Explorer

Theorem axtgpasch

Description: Axiom of (Inner) Pasch, Axiom A7 of Schwabhauser p. 12. Given triangle X Y Z , point U in segment X Z , and point V in segment Y Z , there exists a point a on both the segment U Y and the segment V X . 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)

Ref Expression
Hypotheses axtrkg.p 
|- P = ( Base ` G )
axtrkg.d 
|- .- = ( dist ` G )
axtrkg.i 
|- I = ( Itv ` G )
axtrkg.g 
|- ( ph -> G e. TarskiG )
axtgpasch.1 
|- ( ph -> X e. P )
axtgpasch.2 
|- ( ph -> Y e. P )
axtgpasch.3 
|- ( ph -> Z e. P )
axtgpasch.4 
|- ( ph -> U e. P )
axtgpasch.5 
|- ( ph -> V e. P )
axtgpasch.6 
|- ( ph -> U e. ( X I Z ) )
axtgpasch.7 
|- ( ph -> V e. ( Y I Z ) )
Assertion axtgpasch 
|- ( ph -> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) )

Proof

Step Hyp Ref Expression
1 axtrkg.p 
 |-  P = ( Base ` G )
2 axtrkg.d 
 |-  .- = ( dist ` G )
3 axtrkg.i 
 |-  I = ( Itv ` G )
4 axtrkg.g 
 |-  ( ph -> G e. TarskiG )
5 axtgpasch.1 
 |-  ( ph -> X e. P )
6 axtgpasch.2 
 |-  ( ph -> Y e. P )
7 axtgpasch.3 
 |-  ( ph -> Z e. P )
8 axtgpasch.4 
 |-  ( ph -> U e. P )
9 axtgpasch.5 
 |-  ( ph -> V e. P )
10 axtgpasch.6 
 |-  ( ph -> U e. ( X I Z ) )
11 axtgpasch.7 
 |-  ( ph -> V e. ( Y I Z ) )
12 df-trkg 
 |-  TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
13 inss1 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ ( TarskiGC i^i TarskiGB )
14 inss2 
 |-  ( TarskiGC i^i TarskiGB ) C_ TarskiGB
15 13 14 sstri 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ TarskiGB
16 12 15 eqsstri 
 |-  TarskiG C_ TarskiGB
17 16 4 sselid 
 |-  ( ph -> G e. TarskiGB )
18 1 2 3 istrkgb 
 |-  ( G e. TarskiGB <-> ( G e. _V /\ ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) )
19 18 simprbi 
 |-  ( G e. TarskiGB -> ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) )
20 19 simp2d 
 |-  ( G e. TarskiGB -> A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) )
21 17 20 syl 
 |-  ( ph -> A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) )
22 oveq1 
 |-  ( x = X -> ( x I z ) = ( X I z ) )
23 22 eleq2d 
 |-  ( x = X -> ( u e. ( x I z ) <-> u e. ( X I z ) ) )
24 23 anbi1d 
 |-  ( x = X -> ( ( u e. ( x I z ) /\ v e. ( y I z ) ) <-> ( u e. ( X I z ) /\ v e. ( y I z ) ) ) )
25 oveq2 
 |-  ( x = X -> ( v I x ) = ( v I X ) )
26 25 eleq2d 
 |-  ( x = X -> ( a e. ( v I x ) <-> a e. ( v I X ) ) )
27 26 anbi2d 
 |-  ( x = X -> ( ( a e. ( u I y ) /\ a e. ( v I x ) ) <-> ( a e. ( u I y ) /\ a e. ( v I X ) ) ) )
28 27 rexbidv 
 |-  ( x = X -> ( E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) <-> E. a e. P ( a e. ( u I y ) /\ a e. ( v I X ) ) ) )
29 24 28 imbi12d 
 |-  ( x = X -> ( ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> ( ( u e. ( X I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I X ) ) ) ) )
30 29 2ralbidv 
 |-  ( x = X -> ( A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> A. u e. P A. v e. P ( ( u e. ( X I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I X ) ) ) ) )
31 oveq1 
 |-  ( y = Y -> ( y I z ) = ( Y I z ) )
32 31 eleq2d 
 |-  ( y = Y -> ( v e. ( y I z ) <-> v e. ( Y I z ) ) )
33 32 anbi2d 
 |-  ( y = Y -> ( ( u e. ( X I z ) /\ v e. ( y I z ) ) <-> ( u e. ( X I z ) /\ v e. ( Y I z ) ) ) )
34 oveq2 
 |-  ( y = Y -> ( u I y ) = ( u I Y ) )
35 34 eleq2d 
 |-  ( y = Y -> ( a e. ( u I y ) <-> a e. ( u I Y ) ) )
36 35 anbi1d 
 |-  ( y = Y -> ( ( a e. ( u I y ) /\ a e. ( v I X ) ) <-> ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) )
37 36 rexbidv 
 |-  ( y = Y -> ( E. a e. P ( a e. ( u I y ) /\ a e. ( v I X ) ) <-> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) )
38 33 37 imbi12d 
 |-  ( y = Y -> ( ( ( u e. ( X I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I X ) ) ) <-> ( ( u e. ( X I z ) /\ v e. ( Y I z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) ) )
39 38 2ralbidv 
 |-  ( y = Y -> ( A. u e. P A. v e. P ( ( u e. ( X I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I X ) ) ) <-> A. u e. P A. v e. P ( ( u e. ( X I z ) /\ v e. ( Y I z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) ) )
40 oveq2 
 |-  ( z = Z -> ( X I z ) = ( X I Z ) )
41 40 eleq2d 
 |-  ( z = Z -> ( u e. ( X I z ) <-> u e. ( X I Z ) ) )
42 oveq2 
 |-  ( z = Z -> ( Y I z ) = ( Y I Z ) )
43 42 eleq2d 
 |-  ( z = Z -> ( v e. ( Y I z ) <-> v e. ( Y I Z ) ) )
44 41 43 anbi12d 
 |-  ( z = Z -> ( ( u e. ( X I z ) /\ v e. ( Y I z ) ) <-> ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) ) )
45 44 imbi1d 
 |-  ( z = Z -> ( ( ( u e. ( X I z ) /\ v e. ( Y I z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) <-> ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) ) )
46 45 2ralbidv 
 |-  ( z = Z -> ( A. u e. P A. v e. P ( ( u e. ( X I z ) /\ v e. ( Y I z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) <-> A. u e. P A. v e. P ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) ) )
47 30 39 46 rspc3v 
 |-  ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) -> A. u e. P A. v e. P ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) ) )
48 5 6 7 47 syl3anc 
 |-  ( ph -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) -> A. u e. P A. v e. P ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) ) )
49 21 48 mpd 
 |-  ( ph -> A. u e. P A. v e. P ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) )
50 eleq1 
 |-  ( u = U -> ( u e. ( X I Z ) <-> U e. ( X I Z ) ) )
51 50 anbi1d 
 |-  ( u = U -> ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) <-> ( U e. ( X I Z ) /\ v e. ( Y I Z ) ) ) )
52 oveq1 
 |-  ( u = U -> ( u I Y ) = ( U I Y ) )
53 52 eleq2d 
 |-  ( u = U -> ( a e. ( u I Y ) <-> a e. ( U I Y ) ) )
54 53 anbi1d 
 |-  ( u = U -> ( ( a e. ( u I Y ) /\ a e. ( v I X ) ) <-> ( a e. ( U I Y ) /\ a e. ( v I X ) ) ) )
55 54 rexbidv 
 |-  ( u = U -> ( E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) <-> E. a e. P ( a e. ( U I Y ) /\ a e. ( v I X ) ) ) )
56 51 55 imbi12d 
 |-  ( u = U -> ( ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) <-> ( ( U e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( U I Y ) /\ a e. ( v I X ) ) ) ) )
57 eleq1 
 |-  ( v = V -> ( v e. ( Y I Z ) <-> V e. ( Y I Z ) ) )
58 57 anbi2d 
 |-  ( v = V -> ( ( U e. ( X I Z ) /\ v e. ( Y I Z ) ) <-> ( U e. ( X I Z ) /\ V e. ( Y I Z ) ) ) )
59 oveq1 
 |-  ( v = V -> ( v I X ) = ( V I X ) )
60 59 eleq2d 
 |-  ( v = V -> ( a e. ( v I X ) <-> a e. ( V I X ) ) )
61 60 anbi2d 
 |-  ( v = V -> ( ( a e. ( U I Y ) /\ a e. ( v I X ) ) <-> ( a e. ( U I Y ) /\ a e. ( V I X ) ) ) )
62 61 rexbidv 
 |-  ( v = V -> ( E. a e. P ( a e. ( U I Y ) /\ a e. ( v I X ) ) <-> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) ) )
63 58 62 imbi12d 
 |-  ( v = V -> ( ( ( U e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( U I Y ) /\ a e. ( v I X ) ) ) <-> ( ( U e. ( X I Z ) /\ V e. ( Y I Z ) ) -> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) ) ) )
64 56 63 rspc2v 
 |-  ( ( U e. P /\ V e. P ) -> ( A. u e. P A. v e. P ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) -> ( ( U e. ( X I Z ) /\ V e. ( Y I Z ) ) -> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) ) ) )
65 8 9 64 syl2anc 
 |-  ( ph -> ( A. u e. P A. v e. P ( ( u e. ( X I Z ) /\ v e. ( Y I Z ) ) -> E. a e. P ( a e. ( u I Y ) /\ a e. ( v I X ) ) ) -> ( ( U e. ( X I Z ) /\ V e. ( Y I Z ) ) -> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) ) ) )
66 49 65 mpd 
 |-  ( ph -> ( ( U e. ( X I Z ) /\ V e. ( Y I Z ) ) -> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) ) )
67 10 11 66 mp2and 
 |-  ( ph -> E. a e. P ( a e. ( U I Y ) /\ a e. ( V I X ) ) )