Step |
Hyp |
Ref |
Expression |
1 |
|
istrkg.p |
|- P = ( Base ` G ) |
2 |
|
istrkg.d |
|- .- = ( dist ` G ) |
3 |
|
istrkg.i |
|- I = ( Itv ` G ) |
4 |
|
eqidd |
|- ( ( p = P /\ d = .- /\ i = I ) -> f = f ) |
5 |
|
eqidd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( 1 ..^ n ) = ( 1 ..^ n ) ) |
6 |
|
simp1 |
|- ( ( p = P /\ d = .- /\ i = I ) -> p = P ) |
7 |
6
|
eqcomd |
|- ( ( p = P /\ d = .- /\ i = I ) -> P = p ) |
8 |
4 5 7
|
f1eq123d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( f : ( 1 ..^ n ) -1-1-> P <-> f : ( 1 ..^ n ) -1-1-> p ) ) |
9 |
|
simp2 |
|- ( ( p = P /\ d = .- /\ i = I ) -> d = .- ) |
10 |
9
|
eqcomd |
|- ( ( p = P /\ d = .- /\ i = I ) -> .- = d ) |
11 |
10
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( f ` 1 ) .- x ) = ( ( f ` 1 ) d x ) ) |
12 |
10
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( f ` j ) .- x ) = ( ( f ` j ) d x ) ) |
13 |
11 12
|
eqeq12d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) <-> ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) ) ) |
14 |
10
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( f ` 1 ) .- y ) = ( ( f ` 1 ) d y ) ) |
15 |
10
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( f ` j ) .- y ) = ( ( f ` j ) d y ) ) |
16 |
14 15
|
eqeq12d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) <-> ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) ) ) |
17 |
10
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( f ` 1 ) .- z ) = ( ( f ` 1 ) d z ) ) |
18 |
10
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( f ` j ) .- z ) = ( ( f ` j ) d z ) ) |
19 |
17 18
|
eqeq12d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) <-> ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) ) |
20 |
13 16 19
|
3anbi123d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) ) ) |
21 |
20
|
ralbidv |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) ) ) |
22 |
|
simp3 |
|- ( ( p = P /\ d = .- /\ i = I ) -> i = I ) |
23 |
22
|
eqcomd |
|- ( ( p = P /\ d = .- /\ i = I ) -> I = i ) |
24 |
23
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( x I y ) = ( x i y ) ) |
25 |
24
|
eleq2d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( z e. ( x I y ) <-> z e. ( x i y ) ) ) |
26 |
23
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( z I y ) = ( z i y ) ) |
27 |
26
|
eleq2d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( x e. ( z I y ) <-> x e. ( z i y ) ) ) |
28 |
23
|
oveqd |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( x I z ) = ( x i z ) ) |
29 |
28
|
eleq2d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( y e. ( x I z ) <-> y e. ( x i z ) ) ) |
30 |
25 27 29
|
3orbi123d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) |
31 |
30
|
notbid |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) <-> -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) |
32 |
21 31
|
anbi12d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) ) |
33 |
7 32
|
rexeqbidv |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. z e. p ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) ) |
34 |
7 33
|
rexeqbidv |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. y e. p E. z e. p ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) ) |
35 |
7 34
|
rexeqbidv |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. x e. p E. y e. p E. z e. p ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) ) |
36 |
8 35
|
anbi12d |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( ( f : ( 1 ..^ n ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> ( f : ( 1 ..^ n ) -1-1-> p /\ E. x e. p E. y e. p E. z e. p ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) ) ) |
37 |
36
|
exbidv |
|- ( ( p = P /\ d = .- /\ i = I ) -> ( E. f ( f : ( 1 ..^ n ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. f ( f : ( 1 ..^ n ) -1-1-> p /\ E. x e. p E. y e. p E. z e. p ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) ) ) |
38 |
1 2 3 37
|
sbcie3s |
|- ( g = G -> ( [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. f ( f : ( 1 ..^ n ) -1-1-> p /\ E. x e. p E. y e. p E. z e. p ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) <-> E. f ( f : ( 1 ..^ n ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) ) |
39 |
|
eqidd |
|- ( n = N -> f = f ) |
40 |
|
oveq2 |
|- ( n = N -> ( 1 ..^ n ) = ( 1 ..^ N ) ) |
41 |
|
eqidd |
|- ( n = N -> P = P ) |
42 |
39 40 41
|
f1eq123d |
|- ( n = N -> ( f : ( 1 ..^ n ) -1-1-> P <-> f : ( 1 ..^ N ) -1-1-> P ) ) |
43 |
|
oveq2 |
|- ( n = N -> ( 2 ..^ n ) = ( 2 ..^ N ) ) |
44 |
43
|
raleqdv |
|- ( n = N -> ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) <-> A. j e. ( 2 ..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) ) ) |
45 |
44
|
anbi1d |
|- ( n = N -> ( ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> ( A. j e. ( 2 ..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) |
46 |
45
|
rexbidv |
|- ( n = N -> ( E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. z e. P ( A. j e. ( 2 ..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) |
47 |
46
|
2rexbidv |
|- ( n = N -> ( E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) <-> E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) |
48 |
42 47
|
anbi12d |
|- ( n = N -> ( ( f : ( 1 ..^ n ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> ( f : ( 1 ..^ N ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) ) |
49 |
48
|
exbidv |
|- ( n = N -> ( E. f ( f : ( 1 ..^ n ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) <-> E. f ( f : ( 1 ..^ N ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) ) |
50 |
|
df-trkgld |
|- TarskiGDim>= = { <. g , n >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. f ( f : ( 1 ..^ n ) -1-1-> p /\ E. x e. p E. y e. p E. z e. p ( A. j e. ( 2 ..^ n ) ( ( ( f ` 1 ) d x ) = ( ( f ` j ) d x ) /\ ( ( f ` 1 ) d y ) = ( ( f ` j ) d y ) /\ ( ( f ` 1 ) d z ) = ( ( f ` j ) d z ) ) /\ -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) } |
51 |
38 49 50
|
brabg |
|- ( ( G e. V /\ N e. ( ZZ>= ` 2 ) ) -> ( G TarskiGDim>= N <-> E. f ( f : ( 1 ..^ N ) -1-1-> P /\ E. x e. P E. y e. P E. z e. P ( A. j e. ( 2 ..^ N ) ( ( ( f ` 1 ) .- x ) = ( ( f ` j ) .- x ) /\ ( ( f ` 1 ) .- y ) = ( ( f ` j ) .- y ) /\ ( ( f ` 1 ) .- z ) = ( ( f ` j ) .- z ) ) /\ -. ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) ) ) ) |