istrkgb

Description: Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	istrkg.p	$⊢ P = {Base}_{G}$
	istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
	istrkg.i	$⊢ I = Itv (G)$
Assertion	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))))$

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	$⊢ P = {Base}_{G}$
2		istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		istrkg.i	$⊢ I = Itv (G)$
4		simpl	$⊢ (p = P \land i = I) \to p = P$
5		simpr	$⊢ (p = P \land i = I) \to i = I$
6	5	oveqd	$⊢ (p = P \land i = I) \to x i x = x I x$
7	6	eleq2d	$⊢ (p = P \land i = I) \to (y \in (x i x) \leftrightarrow y \in (x I x))$
8	7	imbi1d	$⊢ (p = P \land i = I) \to ((y \in (x i x) \to x = y) \leftrightarrow (y \in (x I x) \to x = y))$
9	4 8	raleqbidv	$⊢ (p = P \land i = I) \to (\forall y \in p (y \in (x i x) \to x = y) \leftrightarrow \forall y \in P (y \in (x I x) \to x = y))$
10	4 9	raleqbidv	$⊢ (p = P \land i = I) \to (\forall x \in p \forall y \in p (y \in (x i x) \to x = y) \leftrightarrow \forall x \in P \forall y \in P (y \in (x I x) \to x = y))$
11	5	oveqd	$⊢ (p = P \land i = I) \to x i z = x I z$
12	11	eleq2d	$⊢ (p = P \land i = I) \to (u \in (x i z) \leftrightarrow u \in (x I z))$
13	5	oveqd	$⊢ (p = P \land i = I) \to y i z = y I z$
14	13	eleq2d	$⊢ (p = P \land i = I) \to (v \in (y i z) \leftrightarrow v \in (y I z))$
15	12 14	anbi12d	$⊢ (p = P \land i = I) \to ((u \in (x i z) \land v \in (y i z)) \leftrightarrow (u \in (x I z) \land v \in (y I z)))$
16	5	oveqd	$⊢ (p = P \land i = I) \to u i y = u I y$
17	16	eleq2d	$⊢ (p = P \land i = I) \to (a \in (u i y) \leftrightarrow a \in (u I y))$
18	5	oveqd	$⊢ (p = P \land i = I) \to v i x = v I x$
19	18	eleq2d	$⊢ (p = P \land i = I) \to (a \in (v i x) \leftrightarrow a \in (v I x))$
20	17 19	anbi12d	$⊢ (p = P \land i = I) \to ((a \in (u i y) \land a \in (v i x)) \leftrightarrow (a \in (u I y) \land a \in (v I x)))$
21	4 20	rexeqbidv	$⊢ (p = P \land i = I) \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)))$
22	15 21	imbi12d	$⊢ (p = P \land i = I) \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))))$
23	4 22	raleqbidv	$⊢ (p = P \land i = I) \to (\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 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))))$
24	4 23	raleqbidv	$⊢ (p = P \land i = I) \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))))$
25	4 24	raleqbidv	$⊢ (p = P \land i = I) \to (\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))) \leftrightarrow \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))))$
26	4 25	raleqbidv	$⊢ (p = P \land i = I) \to (\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))) \leftrightarrow \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))))$
27	4 26	raleqbidv	$⊢ (p = P \land i = I) \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))) \leftrightarrow \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))))$
28	4	pweqd	$⊢ (p = P \land i = I) \to 𝒫 p = 𝒫 P$
29	5	oveqd	$⊢ (p = P \land i = I) \to a i y = a I y$
30	29	eleq2d	$⊢ (p = P \land i = I) \to (x \in (a i y) \leftrightarrow x \in (a I y))$
31	30	2ralbidv	$⊢ (p = P \land i = I) \to (\forall x \in s \forall y \in t x \in (a i y) \leftrightarrow \forall x \in s \forall y \in t x \in (a I y))$
32	4 31	rexeqbidv	$⊢ (p = P \land i = I) \to (\exists a \in p \forall x \in s \forall y \in t x \in (a i y) \leftrightarrow \exists a \in P \forall x \in s \forall y \in t x \in (a I y))$
33	5	oveqd	$⊢ (p = P \land i = I) \to x i y = x I y$
34	33	eleq2d	$⊢ (p = P \land i = I) \to (b \in (x i y) \leftrightarrow b \in (x I y))$
35	34	2ralbidv	$⊢ (p = P \land i = I) \to (\forall x \in s \forall y \in t b \in (x i y) \leftrightarrow \forall x \in s \forall y \in t b \in (x I y))$
36	4 35	rexeqbidv	$⊢ (p = P \land i = I) \to (\exists b \in p \forall x \in s \forall y \in t b \in (x i y) \leftrightarrow \exists b \in P \forall x \in s \forall y \in t b \in (x I y))$
37	32 36	imbi12d	$⊢ (p = P \land i = I) \to ((\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)) \leftrightarrow (\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)))$
38	28 37	raleqbidv	$⊢ (p = P \land i = I) \to (\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)) \leftrightarrow \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)))$
39	28 38	raleqbidv	$⊢ (p = P \land i = I) \to (\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)) \leftrightarrow \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)))$
40	10 27 39	3anbi123d	$⊢ (p = P \land i = I) \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))) \leftrightarrow (\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))))$
41	1 3 40	sbcie2s	$⊢ f = G \to (\underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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))) \leftrightarrow (\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))))$
42		df-trkgb	$⊢ 𝒢_{Tarski}^{B} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\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)))\}$
43	41 42	elab4g	$⊢ 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))))$

Metamath Proof Explorer

Theorem istrkgb

Proof