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	$⊢ \underset{˙}{-} = dist (G)$
	axtrkg.i	$⊢ I = Itv (G)$
	axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	axtgpasch.1	$⊢ φ \to X \in P$
	axtgpasch.2	$⊢ φ \to Y \in P$
	axtgpasch.3	$⊢ φ \to Z \in P$
	axtgpasch.4	$⊢ φ \to U \in P$
	axtgpasch.5	$⊢ φ \to V \in P$
	axtgpasch.6	$⊢ φ \to U \in (X I Z)$
	axtgpasch.7	$⊢ φ \to V \in (Y I Z)$
Assertion	axtgpasch	$⊢ φ \to \exists a \in P (a \in (U I Y) \land a \in (V I X))$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$⊢ P = {Base}_{G}$
2		axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		axtrkg.i	$⊢ I = Itv (G)$
4		axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		axtgpasch.1	$⊢ φ \to X \in P$
6		axtgpasch.2	$⊢ φ \to Y \in P$
7		axtgpasch.3	$⊢ φ \to Z \in P$
8		axtgpasch.4	$⊢ φ \to U \in P$
9		axtgpasch.5	$⊢ φ \to V \in P$
10		axtgpasch.6	$⊢ φ \to U \in (X I Z)$
11		axtgpasch.7	$⊢ φ \to V \in (Y I Z)$
12		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
13		inss1	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}$
14		inss2	$⊢ 𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B} \subseteq 𝒢_{Tarski}^{B}$
15	13 14	sstri	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{B}$
16	12 15	eqsstri	$⊢ 𝒢_{Tarski} \subseteq 𝒢_{Tarski}^{B}$
17	16 4	sseldi	$⊢ φ \to G \in 𝒢_{Tarski}^{B}$
18	1 2 3	istrkgb	$⊢ G \in 𝒢_{Tarski}^{B} \leftrightarrow (G \in V \land (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \land \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y))))$
19	18	simprbi	$⊢ G \in 𝒢_{Tarski}^{B} \to (\forall x \in P \forall y \in P (y \in (x I x) \to x = y) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \land \forall s \in 𝒫 P \forall t \in 𝒫 P (\exists a \in P \forall x \in s \forall y \in t x \in (a I y) \to \exists b \in P \forall x \in s \forall y \in t b \in (x I y)))$
20	19	simp2d	$⊢ G \in 𝒢_{Tarski}^{B} \to \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x)))$
21	17 20	syl	$⊢ φ \to \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x)))$
22		oveq1	$⊢ x = X \to x I z = X I z$
23	22	eleq2d	$⊢ x = X \to (u \in (x I z) \leftrightarrow u \in (X I z))$
24	23	anbi1d	$⊢ x = X \to ((u \in (x I z) \land v \in (y I z)) \leftrightarrow (u \in (X I z) \land v \in (y I z)))$
25		oveq2	$⊢ x = X \to v I x = v I X$
26	25	eleq2d	$⊢ x = X \to (a \in (v I x) \leftrightarrow a \in (v I X))$
27	26	anbi2d	$⊢ x = X \to ((a \in (u I y) \land a \in (v I x)) \leftrightarrow (a \in (u I y) \land a \in (v I X)))$
28	27	rexbidv	$⊢ x = X \to (\exists a \in P (a \in (u I y) \land a \in (v I x)) \leftrightarrow \exists a \in P (a \in (u I y) \land a \in (v I X)))$
29	24 28	imbi12d	$⊢ x = X \to (((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \leftrightarrow ((u \in (X I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I X))))$
30	29	2ralbidv	$⊢ x = X \to (\forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \leftrightarrow \forall u \in P \forall v \in P ((u \in (X I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I X))))$
31		oveq1	$⊢ y = Y \to y I z = Y I z$
32	31	eleq2d	$⊢ y = Y \to (v \in (y I z) \leftrightarrow v \in (Y I z))$
33	32	anbi2d	$⊢ y = Y \to ((u \in (X I z) \land v \in (y I z)) \leftrightarrow (u \in (X I z) \land v \in (Y I z)))$
34		oveq2	$⊢ y = Y \to u I y = u I Y$
35	34	eleq2d	$⊢ y = Y \to (a \in (u I y) \leftrightarrow a \in (u I Y))$
36	35	anbi1d	$⊢ y = Y \to ((a \in (u I y) \land a \in (v I X)) \leftrightarrow (a \in (u I Y) \land a \in (v I X)))$
37	36	rexbidv	$⊢ y = Y \to (\exists a \in P (a \in (u I y) \land a \in (v I X)) \leftrightarrow \exists a \in P (a \in (u I Y) \land a \in (v I X)))$
38	33 37	imbi12d	$⊢ y = Y \to (((u \in (X I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I X))) \leftrightarrow ((u \in (X I z) \land v \in (Y I z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))))$
39	38	2ralbidv	$⊢ y = Y \to (\forall u \in P \forall v \in P ((u \in (X I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I X))) \leftrightarrow \forall u \in P \forall v \in P ((u \in (X I z) \land v \in (Y I z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))))$
40		oveq2	$⊢ z = Z \to X I z = X I Z$
41	40	eleq2d	$⊢ z = Z \to (u \in (X I z) \leftrightarrow u \in (X I Z))$
42		oveq2	$⊢ z = Z \to Y I z = Y I Z$
43	42	eleq2d	$⊢ z = Z \to (v \in (Y I z) \leftrightarrow v \in (Y I Z))$
44	41 43	anbi12d	$⊢ z = Z \to ((u \in (X I z) \land v \in (Y I z)) \leftrightarrow (u \in (X I Z) \land v \in (Y I Z)))$
45	44	imbi1d	$⊢ z = Z \to (((u \in (X I z) \land v \in (Y I z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))) \leftrightarrow ((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))))$
46	45	2ralbidv	$⊢ z = Z \to (\forall u \in P \forall v \in P ((u \in (X I z) \land v \in (Y I z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))) \leftrightarrow \forall u \in P \forall v \in P ((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))))$
47	30 39 46	rspc3v	$⊢ (X \in P \land Y \in P \land Z \in P) \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \to \forall u \in P \forall v \in P ((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))))$
48	5 6 7 47	syl3anc	$⊢ φ \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P ((u \in (x I z) \land v \in (y I z)) \to \exists a \in P (a \in (u I y) \land a \in (v I x))) \to \forall u \in P \forall v \in P ((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))))$
49	21 48	mpd	$⊢ φ \to \forall u \in P \forall v \in P ((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X)))$
50		eleq1	$⊢ u = U \to (u \in (X I Z) \leftrightarrow U \in (X I Z))$
51	50	anbi1d	$⊢ u = U \to ((u \in (X I Z) \land v \in (Y I Z)) \leftrightarrow (U \in (X I Z) \land v \in (Y I Z)))$
52		oveq1	$⊢ u = U \to u I Y = U I Y$
53	52	eleq2d	$⊢ u = U \to (a \in (u I Y) \leftrightarrow a \in (U I Y))$
54	53	anbi1d	$⊢ u = U \to ((a \in (u I Y) \land a \in (v I X)) \leftrightarrow (a \in (U I Y) \land a \in (v I X)))$
55	54	rexbidv	$⊢ u = U \to (\exists a \in P (a \in (u I Y) \land a \in (v I X)) \leftrightarrow \exists a \in P (a \in (U I Y) \land a \in (v I X)))$
56	51 55	imbi12d	$⊢ u = U \to (((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))) \leftrightarrow ((U \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (U I Y) \land a \in (v I X))))$
57		eleq1	$⊢ v = V \to (v \in (Y I Z) \leftrightarrow V \in (Y I Z))$
58	57	anbi2d	$⊢ v = V \to ((U \in (X I Z) \land v \in (Y I Z)) \leftrightarrow (U \in (X I Z) \land V \in (Y I Z)))$
59		oveq1	$⊢ v = V \to v I X = V I X$
60	59	eleq2d	$⊢ v = V \to (a \in (v I X) \leftrightarrow a \in (V I X))$
61	60	anbi2d	$⊢ v = V \to ((a \in (U I Y) \land a \in (v I X)) \leftrightarrow (a \in (U I Y) \land a \in (V I X)))$
62	61	rexbidv	$⊢ v = V \to (\exists a \in P (a \in (U I Y) \land a \in (v I X)) \leftrightarrow \exists a \in P (a \in (U I Y) \land a \in (V I X)))$
63	58 62	imbi12d	$⊢ v = V \to (((U \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (U I Y) \land a \in (v I X))) \leftrightarrow ((U \in (X I Z) \land V \in (Y I Z)) \to \exists a \in P (a \in (U I Y) \land a \in (V I X))))$
64	56 63	rspc2v	$⊢ (U \in P \land V \in P) \to (\forall u \in P \forall v \in P ((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))) \to ((U \in (X I Z) \land V \in (Y I Z)) \to \exists a \in P (a \in (U I Y) \land a \in (V I X))))$
65	8 9 64	syl2anc	$⊢ φ \to (\forall u \in P \forall v \in P ((u \in (X I Z) \land v \in (Y I Z)) \to \exists a \in P (a \in (u I Y) \land a \in (v I X))) \to ((U \in (X I Z) \land V \in (Y I Z)) \to \exists a \in P (a \in (U I Y) \land a \in (V I X))))$
66	49 65	mpd	$⊢ φ \to ((U \in (X I Z) \land V \in (Y I Z)) \to \exists a \in P (a \in (U I Y) \land a \in (V I X)))$
67	10 11 66	mp2and	$⊢ φ \to \exists a \in P (a \in (U I Y) \land a \in (V I X))$

Metamath Proof Explorer

Theorem axtgpasch

Proof