Theorem istrkg3ld

Description: Property of fulfilling the lower dimension 3 axiom. (Contributed by Thierry Arnoux, 12-Jul-2020)

	Ref	Expression
Hypotheses	istrkg.p	$$⊢P={\mathrm{Base}}_G$$
	istrkg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	istrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
Assertion	istrkg3ld	$$⊢G\in V\to \left(G{\mathrm{Dim}}_{𝒢}\ge 3\leftrightarrow \exists u\in P\exists v\in P\left(u\ne v\wedge \exists x\in P\exists y\in P\exists z\in P\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	$$⊢P={\mathrm{Base}}_G$$
2		istrkg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		istrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		3z	$$⊢3\in \mathbb{Z}$$
5		2le3	$$⊢2\le 3$$
6		2z	$$⊢2\in \mathbb{Z}$$
7	6	eluz1i	$$⊢3\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(3\in \mathbb{Z}\wedge 2\le 3\right)$$
8	4 5 7	mpbir2an	$$⊢3\in {\mathbb{Z}}_{\ge 2}$$
9	1 2 3	istrkgld	$$⊢\left(G\in V\wedge 3\in {\mathbb{Z}}_{\ge 2}\right)\to \left(G{\mathrm{Dim}}_{𝒢}\ge 3\leftrightarrow \exists f\left(f:\left(1..^3\right)\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\right)$$
10	8 9	mpan2	$$⊢G\in V\to \left(G{\mathrm{Dim}}_{𝒢}\ge 3\leftrightarrow \exists f\left(f:\left(1..^3\right)\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\right)$$
11		fzo13pr	$$⊢\left(1..^3\right)=\left\{1,2\right\}$$
12		f1eq2	$$⊢\left(1..^3\right)=\left\{1,2\right\}\to \left(f:\left(1..^3\right)\underset{1-1}{⟶}P\leftrightarrow f:\left\{1,2\right\}\underset{1-1}{⟶}P\right)$$
13	11 12	ax-mp	$$⊢f:\left(1..^3\right)\underset{1-1}{⟶}P\leftrightarrow f:\left\{1,2\right\}\underset{1-1}{⟶}P$$
14	13	anbi1i	$$⊢\left(f:\left(1..^3\right)\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\leftrightarrow \left(f:\left\{1,2\right\}\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
15	14	exbii	$$⊢\exists f\left(f:\left(1..^3\right)\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\leftrightarrow \exists f\left(f:\left\{1,2\right\}\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
16	15	a1i	$$⊢G\in V\to \left(\exists f\left(f:\left(1..^3\right)\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\leftrightarrow \exists f\left(f:\left\{1,2\right\}\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\right)$$
17		1z	$$⊢1\in \mathbb{Z}$$
18		1ne2	$$⊢1\ne 2$$
19		oveq1	$$⊢u=f\left(1\right)\to u\underset{\dot{}}{-}x=f\left(1\right)\underset{\dot{}}{-}x$$
20	19	eqeq1d	$$⊢u=f\left(1\right)\to \left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\leftrightarrow f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\right)$$
21		oveq1	$$⊢u=f\left(1\right)\to u\underset{\dot{}}{-}y=f\left(1\right)\underset{\dot{}}{-}y$$
22	21	eqeq1d	$$⊢u=f\left(1\right)\to \left(u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\leftrightarrow f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\right)$$
23		oveq1	$$⊢u=f\left(1\right)\to u\underset{\dot{}}{-}z=f\left(1\right)\underset{\dot{}}{-}z$$
24	23	eqeq1d	$$⊢u=f\left(1\right)\to \left(u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\leftrightarrow f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)$$
25	20 22 24	3anbi123d	$$⊢u=f\left(1\right)\to \left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\leftrightarrow \left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\right)$$
26	25	anbi1d	$$⊢u=f\left(1\right)\to \left(\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\leftrightarrow \left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
27	26	rexbidv	$$⊢u=f\left(1\right)\to \left(\exists z\in P\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\leftrightarrow \exists z\in P\left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
28	27	2rexbidv	$$⊢u=f\left(1\right)\to \left(\exists x\in P\exists y\in P\exists z\in P\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\leftrightarrow \exists x\in P\exists y\in P\exists z\in P\left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
29		oveq1	$$⊢v=f\left(2\right)\to v\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x$$
30	29	eqeq2d	$$⊢v=f\left(2\right)\to \left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\leftrightarrow f\left(1\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x\right)$$
31		oveq1	$$⊢v=f\left(2\right)\to v\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y$$
32	31	eqeq2d	$$⊢v=f\left(2\right)\to \left(f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\leftrightarrow f\left(1\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y\right)$$
33		oveq1	$$⊢v=f\left(2\right)\to v\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z$$
34	33	eqeq2d	$$⊢v=f\left(2\right)\to \left(f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\leftrightarrow f\left(1\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z\right)$$
35	30 32 34	3anbi123d	$$⊢v=f\left(2\right)\to \left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\leftrightarrow \left(f\left(1\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z\right)\right)$$
36		2p1e3	$$⊢2+1=3$$
37	36	oveq2i	$$⊢\left(2..^2+1\right)=\left(2..^3\right)$$
38		fzosn	$$⊢2\in \mathbb{Z}\to \left(2..^2+1\right)=\left\{2\right\}$$
39	6 38	ax-mp	$$⊢\left(2..^2+1\right)=\left\{2\right\}$$
40	37 39	eqtr3i	$$⊢\left(2..^3\right)=\left\{2\right\}$$
41	40	raleqi	$$⊢\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\leftrightarrow \forall j\in \left\{2\right\}\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)$$
42		fveq2	$$⊢j=2\to f\left(j\right)=f\left(2\right)$$
43	42	oveq1d	$$⊢j=2\to f\left(j\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x$$
44	43	eqeq2d	$$⊢j=2\to \left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\leftrightarrow f\left(1\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x\right)$$
45	42	oveq1d	$$⊢j=2\to f\left(j\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y$$
46	45	eqeq2d	$$⊢j=2\to \left(f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\leftrightarrow f\left(1\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y\right)$$
47	42	oveq1d	$$⊢j=2\to f\left(j\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z$$
48	47	eqeq2d	$$⊢j=2\to \left(f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\leftrightarrow f\left(1\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z\right)$$
49	44 46 48	3anbi123d	$$⊢j=2\to \left(\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\leftrightarrow \left(f\left(1\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z\right)\right)$$
50	49	ralsng	$$⊢2\in \mathbb{Z}\to \left(\forall j\in \left\{2\right\}\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\leftrightarrow \left(f\left(1\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z\right)\right)$$
51	6 50	ax-mp	$$⊢\forall j\in \left\{2\right\}\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\leftrightarrow \left(f\left(1\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z\right)$$
52	41 51	bitri	$$⊢\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\leftrightarrow \left(f\left(1\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z\right)$$
53	35 52	bitr4di	$$⊢v=f\left(2\right)\to \left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\leftrightarrow \forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\right)$$
54	53	anbi1d	$$⊢v=f\left(2\right)\to \left(\left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\leftrightarrow \left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
55	54	rexbidv	$$⊢v=f\left(2\right)\to \left(\exists z\in P\left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\leftrightarrow \exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
56	55	2rexbidv	$$⊢v=f\left(2\right)\to \left(\exists x\in P\exists y\in P\exists z\in P\left(\left(f\left(1\right)\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\leftrightarrow \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
57	28 56	f1prex	$$⊢\left(1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\wedge 1\ne 2\right)\to \left(\exists f\left(f:\left\{1,2\right\}\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\leftrightarrow \exists u\in P\exists v\in P\left(u\ne v\wedge \exists x\in P\exists y\in P\exists z\in P\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\right)$$
58	17 6 18 57	mp3an	$$⊢\exists f\left(f:\left\{1,2\right\}\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\leftrightarrow \exists u\in P\exists v\in P\left(u\ne v\wedge \exists x\in P\exists y\in P\exists z\in P\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)$$
59	58	a1i	$$⊢G\in V\to \left(\exists f\left(f:\left\{1,2\right\}\underset{1-1}{⟶}P\wedge \exists x\in P\exists y\in P\exists z\in P\left(\forall j\in \left(2..^3\right)\left(f\left(1\right)\underset{\dot{}}{-}x=f\left(j\right)\underset{\dot{}}{-}x\wedge f\left(1\right)\underset{\dot{}}{-}y=f\left(j\right)\underset{\dot{}}{-}y\wedge f\left(1\right)\underset{\dot{}}{-}z=f\left(j\right)\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\leftrightarrow \exists u\in P\exists v\in P\left(u\ne v\wedge \exists x\in P\exists y\in P\exists z\in P\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\right)$$
60	10 16 59	3bitrd	$$⊢G\in V\to \left(G{\mathrm{Dim}}_{𝒢}\ge 3\leftrightarrow \exists u\in P\exists v\in P\left(u\ne v\wedge \exists x\in P\exists y\in P\exists z\in P\left(\left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\wedge u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\wedge u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)\wedge \neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right)\right)\right)$$