Step |
Hyp |
Ref |
Expression |
1 |
|
istrkg.p |
|- P = ( Base ` G ) |
2 |
|
istrkg.d |
|- .- = ( dist ` G ) |
3 |
|
istrkg.i |
|- I = ( Itv ` G ) |
4 |
|
simpl |
|- ( ( p = P /\ i = I ) -> p = P ) |
5 |
|
simpr |
|- ( ( p = P /\ i = I ) -> i = I ) |
6 |
5
|
oveqd |
|- ( ( p = P /\ i = I ) -> ( x i x ) = ( x I x ) ) |
7 |
6
|
eleq2d |
|- ( ( p = P /\ i = I ) -> ( y e. ( x i x ) <-> y e. ( x I x ) ) ) |
8 |
7
|
imbi1d |
|- ( ( p = P /\ i = I ) -> ( ( y e. ( x i x ) -> x = y ) <-> ( y e. ( x I x ) -> x = y ) ) ) |
9 |
4 8
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. y e. p ( y e. ( x i x ) -> x = y ) <-> A. y e. P ( y e. ( x I x ) -> x = y ) ) ) |
10 |
4 9
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) <-> A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) ) ) |
11 |
5
|
oveqd |
|- ( ( p = P /\ i = I ) -> ( x i z ) = ( x I z ) ) |
12 |
11
|
eleq2d |
|- ( ( p = P /\ i = I ) -> ( u e. ( x i z ) <-> u e. ( x I z ) ) ) |
13 |
5
|
oveqd |
|- ( ( p = P /\ i = I ) -> ( y i z ) = ( y I z ) ) |
14 |
13
|
eleq2d |
|- ( ( p = P /\ i = I ) -> ( v e. ( y i z ) <-> v e. ( y I z ) ) ) |
15 |
12 14
|
anbi12d |
|- ( ( p = P /\ i = I ) -> ( ( u e. ( x i z ) /\ v e. ( y i z ) ) <-> ( u e. ( x I z ) /\ v e. ( y I z ) ) ) ) |
16 |
5
|
oveqd |
|- ( ( p = P /\ i = I ) -> ( u i y ) = ( u I y ) ) |
17 |
16
|
eleq2d |
|- ( ( p = P /\ i = I ) -> ( a e. ( u i y ) <-> a e. ( u I y ) ) ) |
18 |
5
|
oveqd |
|- ( ( p = P /\ i = I ) -> ( v i x ) = ( v I x ) ) |
19 |
18
|
eleq2d |
|- ( ( p = P /\ i = I ) -> ( a e. ( v i x ) <-> a e. ( v I x ) ) ) |
20 |
17 19
|
anbi12d |
|- ( ( p = P /\ i = I ) -> ( ( a e. ( u i y ) /\ a e. ( v i x ) ) <-> ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) |
21 |
4 20
|
rexeqbidv |
|- ( ( p = P /\ i = I ) -> ( E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) <-> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) |
22 |
15 21
|
imbi12d |
|- ( ( p = P /\ i = I ) -> ( ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) <-> ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) ) |
23 |
4 22
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) <-> A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) ) |
24 |
4 23
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) <-> A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) ) |
25 |
4 24
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) <-> A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) ) |
26 |
4 25
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) <-> A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) ) |
27 |
4 26
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) <-> A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) ) ) |
28 |
4
|
pweqd |
|- ( ( p = P /\ i = I ) -> ~P p = ~P P ) |
29 |
5
|
oveqd |
|- ( ( p = P /\ i = I ) -> ( a i y ) = ( a I y ) ) |
30 |
29
|
eleq2d |
|- ( ( p = P /\ i = I ) -> ( x e. ( a i y ) <-> x e. ( a I y ) ) ) |
31 |
30
|
2ralbidv |
|- ( ( p = P /\ i = I ) -> ( A. x e. s A. y e. t x e. ( a i y ) <-> A. x e. s A. y e. t x e. ( a I y ) ) ) |
32 |
4 31
|
rexeqbidv |
|- ( ( p = P /\ i = I ) -> ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) <-> E. a e. P A. x e. s A. y e. t x e. ( a I y ) ) ) |
33 |
5
|
oveqd |
|- ( ( p = P /\ i = I ) -> ( x i y ) = ( x I y ) ) |
34 |
33
|
eleq2d |
|- ( ( p = P /\ i = I ) -> ( b e. ( x i y ) <-> b e. ( x I y ) ) ) |
35 |
34
|
2ralbidv |
|- ( ( p = P /\ i = I ) -> ( A. x e. s A. y e. t b e. ( x i y ) <-> A. x e. s A. y e. t b e. ( x I y ) ) ) |
36 |
4 35
|
rexeqbidv |
|- ( ( p = P /\ i = I ) -> ( E. b e. p A. x e. s A. y e. t b e. ( x i y ) <-> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) |
37 |
32 36
|
imbi12d |
|- ( ( p = P /\ i = I ) -> ( ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) <-> ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) |
38 |
28 37
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) <-> A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) |
39 |
28 38
|
raleqbidv |
|- ( ( p = P /\ i = I ) -> ( A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) <-> A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) |
40 |
10 27 39
|
3anbi123d |
|- ( ( p = P /\ i = I ) -> ( ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) <-> ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) ) |
41 |
1 3 40
|
sbcie2s |
|- ( f = G -> ( [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) <-> ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) ) |
42 |
|
df-trkgb |
|- TarskiGB = { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) } |
43 |
41 42
|
elab4g |
|- ( G e. TarskiGB <-> ( G e. _V /\ ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) ) |