Theorem axtgupdim2

Description: Upper dimension axiom for dimension 2, Axiom A9 of Schwabhauser p. 13. Three points X , Y and Z equidistant to two given two points U and V must be colinear. (Contributed by Thierry Arnoux, 29-May-2019) (Revised by Thierry Arnoux, 11-Jul-2020)

	Ref	Expression
Hypotheses	axtrkge.p	$$⊢P={\mathrm{Base}}_G$$
	axtrkge.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	axtrkge.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	axtgupdim2.x	$$⊢\phi \to X\in P$$
	axtgupdim2.y	$$⊢\phi \to Y\in P$$
	axtgupdim2.z	$$⊢\phi \to Z\in P$$
	axtgupdim2.u	$$⊢\phi \to U\in P$$
	axtgupdim2.v	$$⊢\phi \to V\in P$$
	axtgupdim2.0	$$⊢\phi \to U\ne V$$
	axtgupdim2.1	$$⊢\phi \to U\underset{\dot{}}{-}X=V\underset{\dot{}}{-}X$$
	axtgupdim2.2	$$⊢\phi \to U\underset{\dot{}}{-}Y=V\underset{\dot{}}{-}Y$$
	axtgupdim2.3	$$⊢\phi \to U\underset{\dot{}}{-}Z=V\underset{\dot{}}{-}Z$$
	axtgupdim2.w	$$⊢\phi \to G\in V$$
	axtgupdim2.g	$$⊢\phi \to \neg G{\mathrm{Dim}}_{𝒢}\ge 3$$
Assertion	axtgupdim2	$$⊢\phi \to \left(Z\in \left(XIY\right)\vee X\in \left(ZIY\right)\vee Y\in \left(XIZ\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axtrkge.p	$$⊢P={\mathrm{Base}}_G$$
2		axtrkge.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		axtrkge.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		axtgupdim2.x	$$⊢\phi \to X\in P$$
5		axtgupdim2.y	$$⊢\phi \to Y\in P$$
6		axtgupdim2.z	$$⊢\phi \to Z\in P$$
7		axtgupdim2.u	$$⊢\phi \to U\in P$$
8		axtgupdim2.v	$$⊢\phi \to V\in P$$
9		axtgupdim2.0	$$⊢\phi \to U\ne V$$
10		axtgupdim2.1	$$⊢\phi \to U\underset{\dot{}}{-}X=V\underset{\dot{}}{-}X$$
11		axtgupdim2.2	$$⊢\phi \to U\underset{\dot{}}{-}Y=V\underset{\dot{}}{-}Y$$
12		axtgupdim2.3	$$⊢\phi \to U\underset{\dot{}}{-}Z=V\underset{\dot{}}{-}Z$$
13		axtgupdim2.w	$$⊢\phi \to G\in V$$
14		axtgupdim2.g	$$⊢\phi \to \neg G{\mathrm{Dim}}_{𝒢}\ge 3$$
15	1 2 3	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)$$
16	13 15	syl	$$⊢\phi \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)$$
17	14 16	mtbid	$$⊢\phi \to \neg \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)$$
18		ralnex2	$$⊢\forall u\in P\forall v\in P\neg \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)\leftrightarrow \neg \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)$$
19	17 18	sylibr	$$⊢\phi \to \forall u\in P\forall v\in P\neg \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)$$
20		neeq1	$$⊢u=U\to \left(u\ne v\leftrightarrow U\ne v\right)$$
21		oveq1	$$⊢u=U\to u\underset{\dot{}}{-}x=U\underset{\dot{}}{-}x$$
22	21	eqeq1d	$$⊢u=U\to \left(u\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\leftrightarrow U\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\right)$$
23		oveq1	$$⊢u=U\to u\underset{\dot{}}{-}y=U\underset{\dot{}}{-}y$$
24	23	eqeq1d	$$⊢u=U\to \left(u\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\leftrightarrow U\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\right)$$
25		oveq1	$$⊢u=U\to u\underset{\dot{}}{-}z=U\underset{\dot{}}{-}z$$
26	25	eqeq1d	$$⊢u=U\to \left(u\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\leftrightarrow U\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\right)$$
27	22 24 26	3anbi123d	$$⊢u=U\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(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)\right)$$
28	27	anbi1d	$$⊢u=U\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(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)$$
29	28	rexbidv	$$⊢u=U\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(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)$$
30	29	2rexbidv	$$⊢u=U\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(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)$$
31	20 30	anbi12d	$$⊢u=U\to \left(\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)\leftrightarrow \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)$$
32	31	notbid	$$⊢u=U\to \left(\neg \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)\leftrightarrow \neg \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)$$
33		neeq2	$$⊢v=V\to \left(U\ne v\leftrightarrow U\ne V\right)$$
34		oveq1	$$⊢v=V\to v\underset{\dot{}}{-}x=V\underset{\dot{}}{-}x$$
35	34	eqeq2d	$$⊢v=V\to \left(U\underset{\dot{}}{-}x=v\underset{\dot{}}{-}x\leftrightarrow U\underset{\dot{}}{-}x=V\underset{\dot{}}{-}x\right)$$
36		oveq1	$$⊢v=V\to v\underset{\dot{}}{-}y=V\underset{\dot{}}{-}y$$
37	36	eqeq2d	$$⊢v=V\to \left(U\underset{\dot{}}{-}y=v\underset{\dot{}}{-}y\leftrightarrow U\underset{\dot{}}{-}y=V\underset{\dot{}}{-}y\right)$$
38		oveq1	$$⊢v=V\to v\underset{\dot{}}{-}z=V\underset{\dot{}}{-}z$$
39	38	eqeq2d	$$⊢v=V\to \left(U\underset{\dot{}}{-}z=v\underset{\dot{}}{-}z\leftrightarrow U\underset{\dot{}}{-}z=V\underset{\dot{}}{-}z\right)$$
40	35 37 39	3anbi123d	$$⊢v=V\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(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)\right)$$
41	40	anbi1d	$$⊢v=V\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(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)$$
42	41	rexbidv	$$⊢v=V\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(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)$$
43	42	2rexbidv	$$⊢v=V\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(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)$$
44	33 43	anbi12d	$$⊢v=V\to \left(\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)\leftrightarrow \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)$$
45	44	notbid	$$⊢v=V\to \left(\neg \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)\leftrightarrow \neg \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)$$
46	32 45	rspc2v	$$⊢\left(U\in P\wedge V\in P\right)\to \left(\forall u\in P\forall v\in P\neg \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)\to \neg \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)$$
47	7 8 46	syl2anc	$$⊢\phi \to \left(\forall u\in P\forall v\in P\neg \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)\to \neg \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)$$
48	19 47	mpd	$$⊢\phi \to \neg \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)$$
49		imnan	$$⊢\left(U\ne V\to \neg \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)\leftrightarrow \neg \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)$$
50	48 49	sylibr	$$⊢\phi \to \left(U\ne V\to \neg \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)$$
51	9 50	mpd	$$⊢\phi \to \neg \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)$$
52		ralnex3	$$⊢\forall x\in P\forall y\in P\forall z\in P\neg \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 \neg \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)$$
53	51 52	sylibr	$$⊢\phi \to \forall x\in P\forall y\in P\forall z\in P\neg \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)$$
54		oveq2	$$⊢x=X\to U\underset{\dot{}}{-}x=U\underset{\dot{}}{-}X$$
55		oveq2	$$⊢x=X\to V\underset{\dot{}}{-}x=V\underset{\dot{}}{-}X$$
56	54 55	eqeq12d	$$⊢x=X\to \left(U\underset{\dot{}}{-}x=V\underset{\dot{}}{-}x\leftrightarrow U\underset{\dot{}}{-}X=V\underset{\dot{}}{-}X\right)$$
57	56	3anbi1d	$$⊢x=X\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(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)\right)$$
58		oveq1	$$⊢x=X\to xIy=XIy$$
59	58	eleq2d	$$⊢x=X\to \left(z\in \left(xIy\right)\leftrightarrow z\in \left(XIy\right)\right)$$
60		eleq1	$$⊢x=X\to \left(x\in \left(zIy\right)\leftrightarrow X\in \left(zIy\right)\right)$$
61		oveq1	$$⊢x=X\to xIz=XIz$$
62	61	eleq2d	$$⊢x=X\to \left(y\in \left(xIz\right)\leftrightarrow y\in \left(XIz\right)\right)$$
63	59 60 62	3orbi123d	$$⊢x=X\to \left(\left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\leftrightarrow \left(z\in \left(XIy\right)\vee X\in \left(zIy\right)\vee y\in \left(XIz\right)\right)\right)$$
64	63	notbid	$$⊢x=X\to \left(\neg \left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\leftrightarrow \neg \left(z\in \left(XIy\right)\vee X\in \left(zIy\right)\vee y\in \left(XIz\right)\right)\right)$$
65	57 64	anbi12d	$$⊢x=X\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(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)$$
66	65	notbid	$$⊢x=X\to \left(\neg \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 \neg \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)$$
67		oveq2	$$⊢y=Y\to U\underset{\dot{}}{-}y=U\underset{\dot{}}{-}Y$$
68		oveq2	$$⊢y=Y\to V\underset{\dot{}}{-}y=V\underset{\dot{}}{-}Y$$
69	67 68	eqeq12d	$$⊢y=Y\to \left(U\underset{\dot{}}{-}y=V\underset{\dot{}}{-}y\leftrightarrow U\underset{\dot{}}{-}Y=V\underset{\dot{}}{-}Y\right)$$
70	69	3anbi2d	$$⊢y=Y\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(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)\right)$$
71		oveq2	$$⊢y=Y\to XIy=XIY$$
72	71	eleq2d	$$⊢y=Y\to \left(z\in \left(XIy\right)\leftrightarrow z\in \left(XIY\right)\right)$$
73		oveq2	$$⊢y=Y\to zIy=zIY$$
74	73	eleq2d	$$⊢y=Y\to \left(X\in \left(zIy\right)\leftrightarrow X\in \left(zIY\right)\right)$$
75		eleq1	$$⊢y=Y\to \left(y\in \left(XIz\right)\leftrightarrow Y\in \left(XIz\right)\right)$$
76	72 74 75	3orbi123d	$$⊢y=Y\to \left(\left(z\in \left(XIy\right)\vee X\in \left(zIy\right)\vee y\in \left(XIz\right)\right)\leftrightarrow \left(z\in \left(XIY\right)\vee X\in \left(zIY\right)\vee Y\in \left(XIz\right)\right)\right)$$
77	76	notbid	$$⊢y=Y\to \left(\neg \left(z\in \left(XIy\right)\vee X\in \left(zIy\right)\vee y\in \left(XIz\right)\right)\leftrightarrow \neg \left(z\in \left(XIY\right)\vee X\in \left(zIY\right)\vee Y\in \left(XIz\right)\right)\right)$$
78	70 77	anbi12d	$$⊢y=Y\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(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)$$
79	78	notbid	$$⊢y=Y\to \left(\neg \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 \neg \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)$$
80		oveq2	$$⊢z=Z\to U\underset{\dot{}}{-}z=U\underset{\dot{}}{-}Z$$
81		oveq2	$$⊢z=Z\to V\underset{\dot{}}{-}z=V\underset{\dot{}}{-}Z$$
82	80 81	eqeq12d	$$⊢z=Z\to \left(U\underset{\dot{}}{-}z=V\underset{\dot{}}{-}z\leftrightarrow U\underset{\dot{}}{-}Z=V\underset{\dot{}}{-}Z\right)$$
83	82	3anbi3d	$$⊢z=Z\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(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)\right)$$
84		eleq1	$$⊢z=Z\to \left(z\in \left(XIY\right)\leftrightarrow Z\in \left(XIY\right)\right)$$
85		oveq1	$$⊢z=Z\to zIY=ZIY$$
86	85	eleq2d	$$⊢z=Z\to \left(X\in \left(zIY\right)\leftrightarrow X\in \left(ZIY\right)\right)$$
87		oveq2	$$⊢z=Z\to XIz=XIZ$$
88	87	eleq2d	$$⊢z=Z\to \left(Y\in \left(XIz\right)\leftrightarrow Y\in \left(XIZ\right)\right)$$
89	84 86 88	3orbi123d	$$⊢z=Z\to \left(\left(z\in \left(XIY\right)\vee X\in \left(zIY\right)\vee Y\in \left(XIz\right)\right)\leftrightarrow \left(Z\in \left(XIY\right)\vee X\in \left(ZIY\right)\vee Y\in \left(XIZ\right)\right)\right)$$
90	89	notbid	$$⊢z=Z\to \left(\neg \left(z\in \left(XIY\right)\vee X\in \left(zIY\right)\vee Y\in \left(XIz\right)\right)\leftrightarrow \neg \left(Z\in \left(XIY\right)\vee X\in \left(ZIY\right)\vee Y\in \left(XIZ\right)\right)\right)$$
91	83 90	anbi12d	$$⊢z=Z\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(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)$$
92	91	notbid	$$⊢z=Z\to \left(\neg \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 \neg \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)$$
93	66 79 92	rspc3v	$$⊢\left(X\in P\wedge Y\in P\wedge Z\in P\right)\to \left(\forall x\in P\forall y\in P\forall z\in P\neg \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)\to \neg \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)$$
94	4 5 6 93	syl3anc	$$⊢\phi \to \left(\forall x\in P\forall y\in P\forall z\in P\neg \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)\to \neg \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)$$
95	53 94	mpd	$$⊢\phi \to \neg \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)$$
96		imnan	$$⊢\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)\to \neg \neg \left(Z\in \left(XIY\right)\vee X\in \left(ZIY\right)\vee Y\in \left(XIZ\right)\right)\right)\leftrightarrow \neg \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)$$
97	95 96	sylibr	$$⊢\phi \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)\to \neg \neg \left(Z\in \left(XIY\right)\vee X\in \left(ZIY\right)\vee Y\in \left(XIZ\right)\right)\right)$$
98	10 11 12 97	mp3and	$$⊢\phi \to \neg \neg \left(Z\in \left(XIY\right)\vee X\in \left(ZIY\right)\vee Y\in \left(XIZ\right)\right)$$
99	98	notnotrd	$$⊢\phi \to \left(Z\in \left(XIY\right)\vee X\in \left(ZIY\right)\vee Y\in \left(XIZ\right)\right)$$