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		2re	$$⊢2\in ℝ$$
6		3re	$$⊢3\in ℝ$$
7		2lt3	$$⊢2<3$$
8	5 6 7	ltleii	$$⊢2\le 3$$
9		2z	$$⊢2\in \mathbb{Z}$$
10	9	eluz1i	$$⊢3\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(3\in \mathbb{Z}\wedge 2\le 3\right)$$
11	4 8 10	mpbir2an	$$⊢3\in {\mathbb{Z}}_{\ge 2}$$
12	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)$$
13	11 12	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)$$
14		fzo13pr	$$⊢\left(1..^3\right)=\left\{1,2\right\}$$
15		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)$$
16	14 15	ax-mp	$$⊢f:\left(1..^3\right)\underset{1-1}{⟶}P\leftrightarrow f:\left\{1,2\right\}\underset{1-1}{⟶}P$$
17	16	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)$$
18	17	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)$$
19	18	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)$$
20		1z	$$⊢1\in \mathbb{Z}$$
21		1ne2	$$⊢1\ne 2$$
22		oveq1	$$⊢u=f\left(1\right)\to u\underset{\dot{}}{-}x=f\left(1\right)\underset{\dot{}}{-}x$$
23	22	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)$$
24		oveq1	$$⊢u=f\left(1\right)\to u\underset{\dot{}}{-}y=f\left(1\right)\underset{\dot{}}{-}y$$
25	24	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)$$
26		oveq1	$$⊢u=f\left(1\right)\to u\underset{\dot{}}{-}z=f\left(1\right)\underset{\dot{}}{-}z$$
27	26	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)$$
28	23 25 27	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)$$
29	28	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)$$
30	29	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)$$
31	30	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)$$
32		oveq1	$$⊢v=f\left(2\right)\to v\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x$$
33	32	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)$$
34		oveq1	$$⊢v=f\left(2\right)\to v\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y$$
35	34	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)$$
36		oveq1	$$⊢v=f\left(2\right)\to v\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z$$
37	36	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)$$
38	33 35 37	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)$$
39		2p1e3	$$⊢2+1=3$$
40	39	oveq2i	$$⊢\left(2..^2+1\right)=\left(2..^3\right)$$
41		fzosn	$$⊢2\in \mathbb{Z}\to \left(2..^2+1\right)=\left\{2\right\}$$
42	9 41	ax-mp	$$⊢\left(2..^2+1\right)=\left\{2\right\}$$
43	40 42	eqtr3i	$$⊢\left(2..^3\right)=\left\{2\right\}$$
44	43	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)$$
45		fveq2	$$⊢j=2\to f\left(j\right)=f\left(2\right)$$
46	45	oveq1d	$$⊢j=2\to f\left(j\right)\underset{\dot{}}{-}x=f\left(2\right)\underset{\dot{}}{-}x$$
47	46	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)$$
48	45	oveq1d	$$⊢j=2\to f\left(j\right)\underset{\dot{}}{-}y=f\left(2\right)\underset{\dot{}}{-}y$$
49	48	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)$$
50	45	oveq1d	$$⊢j=2\to f\left(j\right)\underset{\dot{}}{-}z=f\left(2\right)\underset{\dot{}}{-}z$$
51	50	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)$$
52	47 49 51	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)$$
53	52	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)$$
54	9 53	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)$$
55	44 54	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)$$
56	38 55	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)$$
57	56	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)$$
58	57	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)$$
59	58	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)$$
60	31 59	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)$$
61	20 9 21 60	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)$$
62	61	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)$$
63	13 19 62	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)$$