istrkg2d

Description: Property of fulfilling dimension 2 axiom. (Contributed by Thierry Arnoux, 29-May-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	istrkg2d.p	$⊢ P = {Base}_{G}$
	istrkg2d.d	$⊢ \underset{˙}{-} = dist (G)$
	istrkg2d.i	$⊢ I = Itv (G)$
Assertion	istrkg2d	$⊢ G \in 𝒢_{Tarski}^{2D} \leftrightarrow (G \in V \land (\exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$

Proof

Step	Hyp	Ref	Expression
1		istrkg2d.p	$⊢ P = {Base}_{G}$
2		istrkg2d.d	$⊢ \underset{˙}{-} = dist (G)$
3		istrkg2d.i	$⊢ I = Itv (G)$
4		simp1	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to p = P$
5	4	eqcomd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to P = p$
6		simp3	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to i = I$
7	6	eqcomd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to I = i$
8	7	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to x I y = x i y$
9	8	eleq2d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (z \in (x I y) \leftrightarrow z \in (x i y))$
10	7	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to z I y = z i y$
11	10	eleq2d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (x \in (z I y) \leftrightarrow x \in (z i y))$
12	7	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to x I z = x i z$
13	12	eleq2d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (y \in (x I z) \leftrightarrow y \in (x i z))$
14	9 11 13	3orbi123d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to ((z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
15	14	notbid	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
16	5 15	rexeqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
17	5 16	rexeqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
18	5 17	rexeqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow \exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
19		simp2	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to d = \underset{˙}{-}$
20	19	eqcomd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to \underset{˙}{-} = d$
21	20	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to x \underset{˙}{-} u = x d u$
22	20	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to x \underset{˙}{-} v = x d v$
23	21 22	eqeq12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (x \underset{˙}{-} u = x \underset{˙}{-} v \leftrightarrow x d u = x d v)$
24	20	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to y \underset{˙}{-} u = y d u$
25	20	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to y \underset{˙}{-} v = y d v$
26	24 25	eqeq12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (y \underset{˙}{-} u = y \underset{˙}{-} v \leftrightarrow y d u = y d v)$
27	20	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to z \underset{˙}{-} u = z d u$
28	20	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to z \underset{˙}{-} v = z d v$
29	27 28	eqeq12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (z \underset{˙}{-} u = z \underset{˙}{-} v \leftrightarrow z d u = z d v)$
30	23 26 29	3anbi123d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to ((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \leftrightarrow (x d u = x d v \land y d u = y d v \land z d u = z d v))$
31	30	anbi1d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \leftrightarrow ((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v))$
32	31 14	imbi12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to ((((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
33	5 32	raleqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
34	5 33	raleqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
35	5 34	raleqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
36	5 35	raleqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
37	5 36	raleqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
38	18 37	anbi12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to ((\exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \leftrightarrow (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))))$
39	1 2 3 38	sbcie3s	$⊢ f = G \to (\underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))) \leftrightarrow (\exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$
40		df-trkg2d	$⊢ 𝒢_{Tarski}^{2D} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))\}$
41	39 40	elab4g	$⊢ G \in 𝒢_{Tarski}^{2D} \leftrightarrow (G \in V \land (\exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$

Metamath Proof Explorer

Theorem istrkg2d

Proof