Step |
Hyp |
Ref |
Expression |
1 |
|
axtrkg.p |
|- P = ( Base ` G ) |
2 |
|
axtrkg.d |
|- .- = ( dist ` G ) |
3 |
|
axtrkg.i |
|- I = ( Itv ` G ) |
4 |
|
axtrkg.g |
|- ( ph -> G e. TarskiG ) |
5 |
|
axtgcont.1 |
|- ( ph -> S C_ P ) |
6 |
|
axtgcont.2 |
|- ( ph -> T C_ P ) |
7 |
|
df-trkg |
|- TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) |
8 |
|
inss1 |
|- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ ( TarskiGC i^i TarskiGB ) |
9 |
|
inss2 |
|- ( TarskiGC i^i TarskiGB ) C_ TarskiGB |
10 |
8 9
|
sstri |
|- ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ TarskiGB |
11 |
7 10
|
eqsstri |
|- TarskiG C_ TarskiGB |
12 |
11 4
|
sselid |
|- ( ph -> G e. TarskiGB ) |
13 |
1 2 3
|
istrkgb |
|- ( 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 ) ) ) ) ) |
14 |
13
|
simprbi |
|- ( G e. TarskiGB -> ( 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 ) ) ) ) |
15 |
14
|
simp3d |
|- ( G e. TarskiGB -> 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 ) ) ) |
16 |
12 15
|
syl |
|- ( ph -> 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 ) ) ) |
17 |
1
|
fvexi |
|- P e. _V |
18 |
17
|
ssex |
|- ( S C_ P -> S e. _V ) |
19 |
|
elpwg |
|- ( S e. _V -> ( S e. ~P P <-> S C_ P ) ) |
20 |
5 18 19
|
3syl |
|- ( ph -> ( S e. ~P P <-> S C_ P ) ) |
21 |
5 20
|
mpbird |
|- ( ph -> S e. ~P P ) |
22 |
17
|
ssex |
|- ( T C_ P -> T e. _V ) |
23 |
|
elpwg |
|- ( T e. _V -> ( T e. ~P P <-> T C_ P ) ) |
24 |
6 22 23
|
3syl |
|- ( ph -> ( T e. ~P P <-> T C_ P ) ) |
25 |
6 24
|
mpbird |
|- ( ph -> T e. ~P P ) |
26 |
|
raleq |
|- ( s = S -> ( 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 ) ) ) |
27 |
26
|
rexbidv |
|- ( s = S -> ( 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 ) ) ) |
28 |
|
raleq |
|- ( s = S -> ( 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 ) ) ) |
29 |
28
|
rexbidv |
|- ( s = S -> ( 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 ) ) ) |
30 |
27 29
|
imbi12d |
|- ( s = S -> ( ( 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 ) ) ) ) |
31 |
|
raleq |
|- ( t = T -> ( A. y e. t x e. ( a I y ) <-> A. y e. T x e. ( a I y ) ) ) |
32 |
31
|
rexralbidv |
|- ( t = T -> ( 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 |
|
raleq |
|- ( t = T -> ( A. y e. t b e. ( x I y ) <-> A. y e. T b e. ( x I y ) ) ) |
34 |
33
|
rexralbidv |
|- ( t = T -> ( 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 ) ) ) |
35 |
32 34
|
imbi12d |
|- ( t = T -> ( ( 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 ) ) ) ) |
36 |
30 35
|
rspc2v |
|- ( ( S e. ~P P /\ T e. ~P P ) -> ( 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 ) ) -> ( 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 ) ) ) ) |
37 |
21 25 36
|
syl2anc |
|- ( ph -> ( 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 ) ) -> ( 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 |
16 37
|
mpd |
|- ( ph -> ( 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 ) ) ) |