Metamath Proof Explorer

Theorem 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 ( 𝐺 ∈ 𝑉 → ( 𝐺 DimTarskiG≥ 3 ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( 𝑢 ≠ 𝑣 ∧ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ∃ 𝑧 ∈ 𝑃 ( ( ( 𝑢 − 𝑥 ) = ( 𝑣 − 𝑥 ) ∧ ( 𝑢 − 𝑦 ) = ( 𝑣 − 𝑦 ) ∧ ( 𝑢 − 𝑧 ) = ( 𝑣 − 𝑧 ) ) ∧ ¬ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) ) ) )

Proof

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