istrkg3ld

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

	Ref	Expression
Hypotheses	istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	istrkg3ld	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 Dim_TarskiG≥ 3 ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		3z	⊢ 3 ∈ ℤ
5		2re	⊢ 2 ∈ ℝ
6		3re	⊢ 3 ∈ ℝ
7		2lt3	⊢ 2 < 3
8	5 6 7	ltleii	⊢ 2 ≤ 3
9		2z	⊢ 2 ∈ ℤ
10	9	eluz1i	⊢ ( 3 ∈ ( ℤ_≥ ‘ 2 ) ↔ ( 3 ∈ ℤ ∧ 2 ≤ 3 ) )
11	4 8 10	mpbir2an	⊢ 3 ∈ ( ℤ_≥ ‘ 2 )
12	1 2 3	istrkgld	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 3 ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝐺 Dim_TarskiG≥ 3 ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 3 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
13	11 12	mpan2	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 Dim_TarskiG≥ 3 ↔ ∃ 𝑓 ( 𝑓 : ( 1 ..^ 3 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
14		fzo13pr	⊢ ( 1 ..^ 3 ) = { 1 , 2 }
15		f1eq2	⊢ ( ( 1 ..^ 3 ) = { 1 , 2 } → ( 𝑓 : ( 1 ..^ 3 ) –1-1→ 𝑃 ↔ 𝑓 : { 1 , 2 } –1-1→ 𝑃 ) )
16	14 15	ax-mp	⊢ ( 𝑓 : ( 1 ..^ 3 ) –1-1→ 𝑃 ↔ 𝑓 : { 1 , 2 } –1-1→ 𝑃 )
17	16	anbi1i	⊢ ( ( 𝑓 : ( 1 ..^ 3 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ( 𝑓 : { 1 , 2 } –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
18	17	exbii	⊢ ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 3 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : { 1 , 2 } –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
19	18	a1i	⊢ ( 𝐺 ∈ 𝑉 → ( ∃ 𝑓 ( 𝑓 : ( 1 ..^ 3 ) –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : { 1 , 2 } –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
20		1z	⊢ 1 ∈ ℤ
21		1ne2	⊢ 1 ≠ 2
22		oveq1	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( 𝑢 − 𝑥 ) = ( ( 𝑓 ‘ 1 ) − 𝑥 ) )
23	22	eqeq1d	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ) )
24		oveq1	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( 𝑢 − 𝑦 ) = ( ( 𝑓 ‘ 1 ) − 𝑦 ) )
25	24	eqeq1d	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ) )
26		oveq1	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( 𝑢 − 𝑧 ) = ( ( 𝑓 ‘ 1 ) − 𝑧 ) )
27	26	eqeq1d	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) )
28	23 25 27	3anbi123d	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ↔ ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ) )
29	28	anbi1d	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
30	29	rexbidv	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
31	30	2rexbidv	⊢ ( 𝑢 = ( 𝑓 ‘ 1 ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
32		oveq1	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( 𝑣 − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) )
33	32	eqeq2d	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) ) )
34		oveq1	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( 𝑣 − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) )
35	34	eqeq2d	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) ) )
36		oveq1	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( 𝑣 − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) )
37	36	eqeq2d	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) ) )
38	33 35 37	3anbi123d	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ↔ ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) ) ) )
39		2p1e3	⊢ ( 2 + 1 ) = 3
40	39	oveq2i	⊢ ( 2 ..^ ( 2 + 1 ) ) = ( 2 ..^ 3 )
41		fzosn	⊢ ( 2 ∈ ℤ → ( 2 ..^ ( 2 + 1 ) ) = { 2 } )
42	9 41	ax-mp	⊢ ( 2 ..^ ( 2 + 1 ) ) = { 2 }
43	40 42	eqtr3i	⊢ ( 2 ..^ 3 ) = { 2 }
44	43	raleqi	⊢ ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ∀ 𝑗 ∈ { 2 } ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) )
45		fveq2	⊢ ( 𝑗 = 2 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 2 ) )
46	45	oveq1d	⊢ ( 𝑗 = 2 → ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) )
47	46	eqeq2d	⊢ ( 𝑗 = 2 → ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) ) )
48	45	oveq1d	⊢ ( 𝑗 = 2 → ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) )
49	48	eqeq2d	⊢ ( 𝑗 = 2 → ( ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) ) )
50	45	oveq1d	⊢ ( 𝑗 = 2 → ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) )
51	50	eqeq2d	⊢ ( 𝑗 = 2 → ( ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ↔ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) ) )
52	47 49 51	3anbi123d	⊢ ( 𝑗 = 2 → ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) ) ) )
53	52	ralsng	⊢ ( 2 ∈ ℤ → ( ∀ 𝑗 ∈ { 2 } ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) ) ) )
54	9 53	ax-mp	⊢ ( ∀ 𝑗 ∈ { 2 } ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) ) )
55	44 54	bitri	⊢ ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ↔ ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 2 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 2 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 2 ) − 𝑧 ) ) )
56	38 55	bitr4di	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ↔ ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ) )
57	56	anbi1d	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
58	57	rexbidv	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ∃ 𝑧 ∈ 𝑃 ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
59	58	2rexbidv	⊢ ( 𝑣 = ( 𝑓 ‘ 2 ) → ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
60	31 59	f1prex	⊢ ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ≠ 2 ) → ( ∃ 𝑓 ( 𝑓 : { 1 , 2 } –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
61	20 9 21 60	mp3an	⊢ ( ∃ 𝑓 ( 𝑓 : { 1 , 2 } –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) )
62	61	a1i	⊢ ( 𝐺 ∈ 𝑉 → ( ∃ 𝑓 ( 𝑓 : { 1 , 2 } –1-1→ 𝑃 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ∀ 𝑗 ∈ ( 2 ..^ 3 ) ( ( ( 𝑓 ‘ 1 ) − 𝑥 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑥 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑦 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑦 ) ∧ ( ( 𝑓 ‘ 1 ) − 𝑧 ) = ( ( 𝑓 ‘ 𝑗 ) − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )
63	13 19 62	3bitrd	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 Dim_TarskiG≥ 3 ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )

Metamath Proof Explorer

Theorem istrkg3ld

Proof