istrkg2ld

Description: Property of fulfilling the lower dimension 2 axiom. (Contributed by Thierry Arnoux, 20-Nov-2019)

	Ref	Expression
Hypotheses	istrkg.p	$⊢ P = {Base}_{G}$
	istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
	istrkg.i	$⊢ I = Itv (G)$
Assertion	istrkg2ld	$⊢ G \in V \to (G {Dim}_{𝒢} \geq 2 \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)))$

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	$⊢ P = {Base}_{G}$
2		istrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		istrkg.i	$⊢ I = Itv (G)$
4		2z	$⊢ 2 \in ℤ$
5		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
6	4 5	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
7	1 2 3	istrkgld	$⊢ (G \in V \land 2 \in ℤ_{\geq 2}) \to (G {Dim}_{𝒢} \geq 2 \leftrightarrow \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$
8	6 7	mpan2	$⊢ G \in V \to (G {Dim}_{𝒢} \geq 2 \leftrightarrow \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$
9		r19.41v	$⊢ \exists x \in P (\exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \land f : (1 ..^2) \underset{1-1}{⟶} P) \leftrightarrow (\exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \land f : (1 ..^2) \underset{1-1}{⟶} P)$
10		ancom	$⊢ (\exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \land f : (1 ..^2) \underset{1-1}{⟶} P) \leftrightarrow (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
11	10	rexbii	$⊢ \exists x \in P (\exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \land f : (1 ..^2) \underset{1-1}{⟶} P) \leftrightarrow \exists x \in P (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
12		ancom	$⊢ (\exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \land f : (1 ..^2) \underset{1-1}{⟶} P) \leftrightarrow (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
13	9 11 12	3bitr3ri	$⊢ (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \leftrightarrow \exists x \in P (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
14	13	exbii	$⊢ \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \leftrightarrow \exists f \exists x \in P (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
15		rexcom4	$⊢ \exists x \in P \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \leftrightarrow \exists f \exists x \in P (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
16		simpr	$⊢ (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \to \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))$
17	16	reximi	$⊢ \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \to \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))$
18	17	reximi	$⊢ \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \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))$
19	18	adantl	$⊢ (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \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))$
20	19	exlimiv	$⊢ \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \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))$
21	20	adantl	$⊢ (x \in P \land \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))) \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))$
22		1ex	$⊢ 1 \in V$
23		vex	$⊢ x \in V$
24	22 23	f1osn	$⊢ \{⟨1, x⟩\} : \{1\} \underset{1-1 onto}{⟶} \{x\}$
25		f1of1	$⊢ \{⟨1, x⟩\} : \{1\} \underset{1-1 onto}{⟶} \{x\} \to \{⟨1, x⟩\} : \{1\} \underset{1-1}{⟶} \{x\}$
26	24 25	mp1i	$⊢ x \in P \to \{⟨1, x⟩\} : \{1\} \underset{1-1}{⟶} \{x\}$
27		snssi	$⊢ x \in P \to \{x\} \subseteq P$
28		f1ss	$⊢ (\{⟨1, x⟩\} : \{1\} \underset{1-1}{⟶} \{x\} \land \{x\} \subseteq P) \to \{⟨1, x⟩\} : \{1\} \underset{1-1}{⟶} P$
29	26 27 28	syl2anc	$⊢ x \in P \to \{⟨1, x⟩\} : \{1\} \underset{1-1}{⟶} P$
30		fzo12sn	$⊢ (1 ..^2) = \{1\}$
31	30	mpteq1i	$⊢ (j \in (1 ..^2) ⟼ x) = (j \in \{1\} ⟼ x)$
32		fmptsn	$⊢ (1 \in V \land x \in V) \to \{⟨1, x⟩\} = (j \in \{1\} ⟼ x)$
33	22 23 32	mp2an	$⊢ \{⟨1, x⟩\} = (j \in \{1\} ⟼ x)$
34	31 33	eqtr4i	$⊢ (j \in (1 ..^2) ⟼ x) = \{⟨1, x⟩\}$
35	34	a1i	$⊢ ⊤ \to (j \in (1 ..^2) ⟼ x) = \{⟨1, x⟩\}$
36	30	a1i	$⊢ ⊤ \to (1 ..^2) = \{1\}$
37		eqidd	$⊢ ⊤ \to P = P$
38	35 36 37	f1eq123d	$⊢ ⊤ \to ((j \in (1 ..^2) ⟼ x) : (1 ..^2) \underset{1-1}{⟶} P \leftrightarrow \{⟨1, x⟩\} : \{1\} \underset{1-1}{⟶} P)$
39	38	mptru	$⊢ (j \in (1 ..^2) ⟼ x) : (1 ..^2) \underset{1-1}{⟶} P \leftrightarrow \{⟨1, x⟩\} : \{1\} \underset{1-1}{⟶} P$
40	29 39	sylibr	$⊢ x \in P \to (j \in (1 ..^2) ⟼ x) : (1 ..^2) \underset{1-1}{⟶} P$
41		ral0	$⊢ \forall j \in \emptyset ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z)$
42		fzo0	$⊢ (2 ..^2) = \emptyset$
43	42	raleqi	$⊢ \forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \leftrightarrow \forall j \in \emptyset ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z)$
44	41 43	mpbir	$⊢ \forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z)$
45	44	jctl	$⊢ \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \to (\forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))$
46	45	reximi	$⊢ \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \to \exists z \in P (\forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))$
47	46	reximi	$⊢ \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)) \to \exists y \in P \exists z \in P (\forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))$
48		ovex	$⊢ (1 ..^2) \in V$
49	48	mptex	$⊢ (j \in (1 ..^2) ⟼ x) \in V$
50		f1eq1	$⊢ f = (j \in (1 ..^2) ⟼ x) \to (f : (1 ..^2) \underset{1-1}{⟶} P \leftrightarrow (j \in (1 ..^2) ⟼ x) : (1 ..^2) \underset{1-1}{⟶} P)$
51		nfmpt1	$⊢ \underline{Ⅎ} j (j \in (1 ..^2) ⟼ x)$
52	51	nfeq2	$⊢ Ⅎ j f = (j \in (1 ..^2) ⟼ x)$
53		nfv	$⊢ Ⅎ j (y \in P \land z \in P)$
54	52 53	nfan	$⊢ Ⅎ j (f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P))$
55		simpll	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f = (j \in (1 ..^2) ⟼ x)$
56	55	fveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (1) = (j \in (1 ..^2) ⟼ x) (1)$
57	56	oveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x$
58	55	fveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (j) = (j \in (1 ..^2) ⟼ x) (j)$
59	58	oveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (j) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x$
60	57 59	eqeq12d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \leftrightarrow (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x)$
61	56	oveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y$
62	58	oveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (j) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y$
63	61 62	eqeq12d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to (f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \leftrightarrow (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y)$
64	56	oveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z$
65	58	oveq1d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to f (j) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z$
66	64 65	eqeq12d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to (f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z \leftrightarrow (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z)$
67	60 63 66	3anbi123d	$⊢ ((f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \land j \in (2 ..^2)) \to ((f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \leftrightarrow ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z))$
68	54 67	ralbida	$⊢ (f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \to (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \leftrightarrow \forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z))$
69	68	anbi1d	$⊢ (f = (j \in (1 ..^2) ⟼ x) \land (y \in P \land z \in P)) \to ((\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow (\forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
70	69	2rexbidva	$⊢ f = (j \in (1 ..^2) ⟼ x) \to (\exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \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 (\forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
71	50 70	anbi12d	$⊢ f = (j \in (1 ..^2) ⟼ x) \to ((f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \leftrightarrow ((j \in (1 ..^2) ⟼ x) : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$
72	49 71	spcev	$⊢ ((j \in (1 ..^2) ⟼ x) : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) ((j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} x = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} x \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} y = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} y \land (j \in (1 ..^2) ⟼ x) (1) \underset{˙}{-} z = (j \in (1 ..^2) ⟼ x) (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))) \to \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
73	40 47 72	syl2an	$⊢ (x \in P \land \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))) \to \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))))$
74	21 73	impbida	$⊢ x \in P \to (\exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \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)))$
75	74	rexbiia	$⊢ \exists x \in P \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \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))$
76	14 15 75	3bitr2i	$⊢ \exists f (f : (1 ..^2) \underset{1-1}{⟶} P \land \exists x \in P \exists y \in P \exists z \in P (\forall j \in (2 ..^2) (f (1) \underset{˙}{-} x = f (j) \underset{˙}{-} x \land f (1) \underset{˙}{-} y = f (j) \underset{˙}{-} y \land f (1) \underset{˙}{-} z = f (j) \underset{˙}{-} z) \land \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))$
77	8 76	bitrdi	$⊢ G \in V \to (G {Dim}_{𝒢} \geq 2 \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)))$

Metamath Proof Explorer

Theorem istrkg2ld

Proof