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	4	eqcomd	$⊢ (p = P \land i = I) \to P = p$
6	5	adantr	$⊢ ((p = P \land i = I) \land x \in P) \to P = p$
7		simpllr	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \to i = I$
8	7	eqcomd	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \to I = i$
9	8	oveqd	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \to x I x = x i x$
10	9	eleq2d	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \to (y \in (x I x) \leftrightarrow y \in (x i x))$
11	10	imbi1d	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \to ((y \in (x I x) \to x = y) \leftrightarrow (y \in (x i x) \to x = y))$
12	6 11	raleqbidva	$⊢ ((p = P \land i = I) \land x \in P) \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))$
13	5 12	raleqbidva	$⊢ (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))$
14	6	adantr	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \to P = p$
15	14	adantr	$⊢ ((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \to P = p$
16	15	adantr	$⊢ (((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \to P = p$
17		simp-6r	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to i = I$
18	17	eqcomd	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to I = i$
19	18	oveqd	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to x I z = x i z$
20	19	eleq2d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to (u \in (x I z) \leftrightarrow u \in (x i z))$
21	18	oveqd	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to y I z = y i z$
22	21	eleq2d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to (v \in (y I z) \leftrightarrow v \in (y i z))$
23	20 22	anbi12d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to ((u \in (x I z) \land v \in (y I z)) \leftrightarrow (u \in (x i z) \land v \in (y i z)))$
24	16	adantr	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \to P = p$
25	18	oveqdr	$⊢ (((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \to u I y = u i y$
26	25	eleq2d	$⊢ (((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \to (a \in (u I y) \leftrightarrow a \in (u i y))$
27	18	oveqdr	$⊢ (((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \to v I x = v i x$
28	27	eleq2d	$⊢ (((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \to (a \in (v I x) \leftrightarrow a \in (v i x))$
29	26 28	anbi12d	$⊢ (((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \land a \in P) \to ((a \in (u I y) \land a \in (v I x)) \leftrightarrow (a \in (u i y) \land a \in (v i x)))$
30	24 29	rexeqbidva	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \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)))$
31	23 30	imbi12d	$⊢ ((((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \land v \in P) \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))))$
32	16 31	raleqbidva	$⊢ (((((p = P \land i = I) \land x \in P) \land y \in P) \land z \in P) \land u \in P) \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))))$
33	15 32	raleqbidva	$⊢ ((((p = P \land i = I) \land x \in P) \land y \in P) \land z \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))) \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))))$
34	14 33	raleqbidva	$⊢ (((p = P \land i = I) \land x \in P) \land y \in P) \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))))$
35	6 34	raleqbidva	$⊢ ((p = P \land i = I) \land x \in P) \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))))$
36	5 35	raleqbidva	$⊢ (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))))$
37	5	pweqd	$⊢ (p = P \land i = I) \to 𝒫 P = 𝒫 p$
38	37	adantr	$⊢ ((p = P \land i = I) \land s \in 𝒫 P) \to 𝒫 P = 𝒫 p$
39	5	ad2antrr	$⊢ (((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \to P = p$
40		simp-4r	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land a \in P) \to i = I$
41	40	eqcomd	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land a \in P) \to I = i$
42	41	oveqd	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land a \in P) \to a I y = a i y$
43	42	eleq2d	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land a \in P) \to (x \in (a I y) \leftrightarrow x \in (a i y))$
44	43	2ralbidv	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land a \in P) \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))$
45	39 44	rexeqbidva	$⊢ (((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \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))$
46		simp-4r	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land b \in P) \to i = I$
47	46	eqcomd	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land b \in P) \to I = i$
48	47	oveqd	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land b \in P) \to x I y = x i y$
49	48	eleq2d	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land b \in P) \to (b \in (x I y) \leftrightarrow b \in (x i y))$
50	49	2ralbidv	$⊢ ((((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \land b \in P) \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))$
51	39 50	rexeqbidva	$⊢ (((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \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))$
52	45 51	imbi12d	$⊢ (((p = P \land i = I) \land s \in 𝒫 P) \land t \in 𝒫 P) \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)))$
53	38 52	raleqbidva	$⊢ ((p = P \land i = I) \land s \in 𝒫 P) \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)))$
54	37 53	raleqbidva	$⊢ (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)))$
55	13 36 54	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))))$
56	1 3 55	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))))$
57		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)))\}$
58	56 57	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