MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtgupdim2 Structured version   Unicode version

Theorem axtgupdim2 22907
Description: Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 29-May-2019.)
Hypotheses
Ref Expression
axtrkge.p  |-  P  =  ( Base `  G
)
axtrkge.d  |-  .-  =  ( dist `  G )
axtrkge.i  |-  I  =  (Itv `  G )
axtgupdim2.g  |-  ( ph  ->  G  e. TarskiG2D )
axtgupdim2.x  |-  ( ph  ->  X  e.  P )
axtgupdim2.y  |-  ( ph  ->  Y  e.  P )
axtgupdim2.z  |-  ( ph  ->  Z  e.  P )
axtgupdim2.u  |-  ( ph  ->  U  e.  P )
axtgupdim2.v  |-  ( ph  ->  V  e.  P )
axtgupdim2.0  |-  ( ph  ->  U  =/=  V )
axtgupdim2.1  |-  ( ph  ->  ( X  .-  U
)  =  ( X 
.-  V ) )
axtgupdim2.2  |-  ( ph  ->  ( Y  .-  U
)  =  ( Y 
.-  V ) )
axtgupdim2.3  |-  ( ph  ->  ( Z  .-  U
)  =  ( Z 
.-  V ) )
Assertion
Ref Expression
axtgupdim2  |-  ( ph  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )

Proof of Theorem axtgupdim2
Dummy variables  v  u  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgupdim2.1 . . 3  |-  ( ph  ->  ( X  .-  U
)  =  ( X 
.-  V ) )
2 axtgupdim2.2 . . 3  |-  ( ph  ->  ( Y  .-  U
)  =  ( Y 
.-  V ) )
3 axtgupdim2.3 . . 3  |-  ( ph  ->  ( Z  .-  U
)  =  ( Z 
.-  V ) )
41, 2, 33jca 1168 . 2  |-  ( ph  ->  ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V ) ) )
5 axtgupdim2.0 . 2  |-  ( ph  ->  U  =/=  V )
6 axtgupdim2.g . . . . . . 7  |-  ( ph  ->  G  e. TarskiG2D )
7 axtrkge.p . . . . . . . 8  |-  P  =  ( Base `  G
)
8 axtrkge.d . . . . . . . 8  |-  .-  =  ( dist `  G )
9 axtrkge.i . . . . . . . 8  |-  I  =  (Itv `  G )
107, 8, 9istrkg2d 22897 . . . . . . 7  |-  ( G  e. TarskiG2D  <->  ( G  e.  _V  /\  ( E. x  e.  P  E. y  e.  P  E. z  e.  P  -.  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( (
( ( x  .-  u )  =  ( x  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) ) ) ) )
116, 10sylib 196 . . . . . 6  |-  ( ph  ->  ( G  e.  _V  /\  ( E. x  e.  P  E. y  e.  P  E. z  e.  P  -.  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  (
( ( ( x 
.-  u )  =  ( x  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) ) ) ) )
1211simprd 463 . . . . 5  |-  ( ph  ->  ( E. x  e.  P  E. y  e.  P  E. z  e.  P  -.  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  (
( ( ( x 
.-  u )  =  ( x  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) ) ) )
1312simprd 463 . . . 4  |-  ( ph  ->  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( ( ( x  .-  u )  =  ( x  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) ) )
14 axtgupdim2.x . . . . 5  |-  ( ph  ->  X  e.  P )
15 axtgupdim2.y . . . . 5  |-  ( ph  ->  Y  e.  P )
16 axtgupdim2.z . . . . 5  |-  ( ph  ->  Z  e.  P )
17 oveq1 6093 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  .-  u )  =  ( X  .-  u ) )
18 oveq1 6093 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  .-  v )  =  ( X  .-  v ) )
1917, 18eqeq12d 2452 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( x  .-  u
)  =  ( x 
.-  v )  <->  ( X  .-  u )  =  ( X  .-  v ) ) )
20193anbi1d 1293 . . . . . . . . 9  |-  ( x  =  X  ->  (
( ( x  .-  u )  =  ( x  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  <->  ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) ) ) )
2120anbi1d 704 . . . . . . . 8  |-  ( x  =  X  ->  (
( ( ( x 
.-  u )  =  ( x  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  u
)  =  ( X 
.-  v )  /\  ( y  .-  u
)  =  ( y 
.-  v )  /\  ( z  .-  u
)  =  ( z 
.-  v ) )  /\  u  =/=  v
) ) )
22 oveq1 6093 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I y )  =  ( X I y ) )
2322eleq2d 2505 . . . . . . . . 9  |-  ( x  =  X  ->  (
z  e.  ( x I y )  <->  z  e.  ( X I y ) ) )
24 eleq1 2498 . . . . . . . . 9  |-  ( x  =  X  ->  (
x  e.  ( z I y )  <->  X  e.  ( z I y ) ) )
25 oveq1 6093 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
2625eleq2d 2505 . . . . . . . . 9  |-  ( x  =  X  ->  (
y  e.  ( x I z )  <->  y  e.  ( X I z ) ) )
2723, 24, 263orbi123d 1288 . . . . . . . 8  |-  ( x  =  X  ->  (
( 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 ) ) ) )
2821, 27imbi12d 320 . . . . . . 7  |-  ( x  =  X  ->  (
( ( ( ( x  .-  u )  =  ( x  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  <->  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) ) ) )
29282ralbidv 2752 . . . . . 6  |-  ( x  =  X  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( x  .-  u )  =  ( x  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) ) ) )
30 oveq1 6093 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
y  .-  u )  =  ( Y  .-  u ) )
31 oveq1 6093 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
y  .-  v )  =  ( Y  .-  v ) )
3230, 31eqeq12d 2452 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
( y  .-  u
)  =  ( y 
.-  v )  <->  ( Y  .-  u )  =  ( Y  .-  v ) ) )
33323anbi2d 1294 . . . . . . . . 9  |-  ( y  =  Y  ->  (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  <->  ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) ) ) )
3433anbi1d 704 . . . . . . . 8  |-  ( y  =  Y  ->  (
( ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v ) ) )
35 oveq2 6094 . . . . . . . . . 10  |-  ( y  =  Y  ->  ( X I y )  =  ( X I Y ) )
3635eleq2d 2505 . . . . . . . . 9  |-  ( y  =  Y  ->  (
z  e.  ( X I y )  <->  z  e.  ( X I Y ) ) )
37 oveq2 6094 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
z I y )  =  ( z I Y ) )
3837eleq2d 2505 . . . . . . . . 9  |-  ( y  =  Y  ->  ( X  e.  ( z
I y )  <->  X  e.  ( z I Y ) ) )
39 eleq1 2498 . . . . . . . . 9  |-  ( y  =  Y  ->  (
y  e.  ( X I z )  <->  Y  e.  ( X I z ) ) )
4036, 38, 393orbi123d 1288 . . . . . . . 8  |-  ( y  =  Y  ->  (
( 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 ) ) ) )
4134, 40imbi12d 320 . . . . . . 7  |-  ( y  =  Y  ->  (
( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) )  <->  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) ) ) )
42412ralbidv 2752 . . . . . 6  |-  ( y  =  Y  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) ) ) )
43 oveq1 6093 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
z  .-  u )  =  ( Z  .-  u ) )
44 oveq1 6093 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
z  .-  v )  =  ( Z  .-  v ) )
4543, 44eqeq12d 2452 . . . . . . . . . 10  |-  ( z  =  Z  ->  (
( z  .-  u
)  =  ( z 
.-  v )  <->  ( Z  .-  u )  =  ( Z  .-  v ) ) )
46453anbi3d 1295 . . . . . . . . 9  |-  ( z  =  Z  ->  (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  <->  ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v ) ) ) )
4746anbi1d 704 . . . . . . . 8  |-  ( z  =  Z  ->  (
( ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v ) ) )
48 eleq1 2498 . . . . . . . . 9  |-  ( z  =  Z  ->  (
z  e.  ( X I Y )  <->  Z  e.  ( X I Y ) ) )
49 oveq1 6093 . . . . . . . . . 10  |-  ( z  =  Z  ->  (
z I Y )  =  ( Z I Y ) )
5049eleq2d 2505 . . . . . . . . 9  |-  ( z  =  Z  ->  ( X  e.  ( z
I Y )  <->  X  e.  ( Z I Y ) ) )
51 oveq2 6094 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( X I z )  =  ( X I Z ) )
5251eleq2d 2505 . . . . . . . . 9  |-  ( z  =  Z  ->  ( Y  e.  ( X I z )  <->  Y  e.  ( X I Z ) ) )
5348, 50, 523orbi123d 1288 . . . . . . . 8  |-  ( z  =  Z  ->  (
( 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 ) ) ) )
5447, 53imbi12d 320 . . . . . . 7  |-  ( z  =  Z  ->  (
( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) )  <->  ( ( ( ( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
55542ralbidv 2752 . . . . . 6  |-  ( z  =  Z  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) )  <->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
5629, 42, 55rspc3v 3077 . . . . 5  |-  ( ( X  e.  P  /\  Y  e.  P  /\  Z  e.  P )  ->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( ( ( x  .-  u
)  =  ( x 
.-  v )  /\  ( y  .-  u
)  =  ( y 
.-  v )  /\  ( z  .-  u
)  =  ( z 
.-  v ) )  /\  u  =/=  v
)  ->  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
5714, 15, 16, 56syl3anc 1218 . . . 4  |-  ( ph  ->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( ( ( x  .-  u
)  =  ( x 
.-  v )  /\  ( y  .-  u
)  =  ( y 
.-  v )  /\  ( z  .-  u
)  =  ( z 
.-  v ) )  /\  u  =/=  v
)  ->  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
5813, 57mpd 15 . . 3  |-  ( ph  ->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) )
59 axtgupdim2.u . . . 4  |-  ( ph  ->  U  e.  P )
60 axtgupdim2.v . . . 4  |-  ( ph  ->  V  e.  P )
61 oveq2 6094 . . . . . . . . 9  |-  ( u  =  U  ->  ( X  .-  u )  =  ( X  .-  U
) )
6261eqeq1d 2446 . . . . . . . 8  |-  ( u  =  U  ->  (
( X  .-  u
)  =  ( X 
.-  v )  <->  ( X  .-  U )  =  ( X  .-  v ) ) )
63 oveq2 6094 . . . . . . . . 9  |-  ( u  =  U  ->  ( Y  .-  u )  =  ( Y  .-  U
) )
6463eqeq1d 2446 . . . . . . . 8  |-  ( u  =  U  ->  (
( Y  .-  u
)  =  ( Y 
.-  v )  <->  ( Y  .-  U )  =  ( Y  .-  v ) ) )
65 oveq2 6094 . . . . . . . . 9  |-  ( u  =  U  ->  ( Z  .-  u )  =  ( Z  .-  U
) )
6665eqeq1d 2446 . . . . . . . 8  |-  ( u  =  U  ->  (
( Z  .-  u
)  =  ( Z 
.-  v )  <->  ( Z  .-  U )  =  ( Z  .-  v ) ) )
6762, 64, 663anbi123d 1289 . . . . . . 7  |-  ( u  =  U  ->  (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  <->  ( ( X 
.-  U )  =  ( X  .-  v
)  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) ) ) )
68 neeq1 2611 . . . . . . 7  |-  ( u  =  U  ->  (
u  =/=  v  <->  U  =/=  v ) )
6967, 68anbi12d 710 . . . . . 6  |-  ( u  =  U  ->  (
( ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  U
)  =  ( X 
.-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v
) )  /\  U  =/=  v ) ) )
7069imbi1d 317 . . . . 5  |-  ( u  =  U  ->  (
( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  <->  ( (
( ( X  .-  U )  =  ( X  .-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  /\  U  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
71 oveq2 6094 . . . . . . . . 9  |-  ( v  =  V  ->  ( X  .-  v )  =  ( X  .-  V
) )
7271eqeq2d 2449 . . . . . . . 8  |-  ( v  =  V  ->  (
( X  .-  U
)  =  ( X 
.-  v )  <->  ( X  .-  U )  =  ( X  .-  V ) ) )
73 oveq2 6094 . . . . . . . . 9  |-  ( v  =  V  ->  ( Y  .-  v )  =  ( Y  .-  V
) )
7473eqeq2d 2449 . . . . . . . 8  |-  ( v  =  V  ->  (
( Y  .-  U
)  =  ( Y 
.-  v )  <->  ( Y  .-  U )  =  ( Y  .-  V ) ) )
75 oveq2 6094 . . . . . . . . 9  |-  ( v  =  V  ->  ( Z  .-  v )  =  ( Z  .-  V
) )
7675eqeq2d 2449 . . . . . . . 8  |-  ( v  =  V  ->  (
( Z  .-  U
)  =  ( Z 
.-  v )  <->  ( Z  .-  U )  =  ( Z  .-  V ) ) )
7772, 74, 763anbi123d 1289 . . . . . . 7  |-  ( v  =  V  ->  (
( ( X  .-  U )  =  ( X  .-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  <->  ( ( X 
.-  U )  =  ( X  .-  V
)  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V ) ) ) )
78 neeq2 2612 . . . . . . 7  |-  ( v  =  V  ->  ( U  =/=  v  <->  U  =/=  V ) )
7977, 78anbi12d 710 . . . . . 6  |-  ( v  =  V  ->  (
( ( ( X 
.-  U )  =  ( X  .-  v
)  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  /\  U  =/=  v )  <->  ( (
( X  .-  U
)  =  ( X 
.-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V
) )  /\  U  =/=  V ) ) )
8079imbi1d 317 . . . . 5  |-  ( v  =  V  ->  (
( ( ( ( X  .-  U )  =  ( X  .-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v
)  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  /\  U  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  <->  ( (
( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
8170, 80rspc2v 3074 . . . 4  |-  ( ( U  e.  P  /\  V  e.  P )  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  -> 
( ( ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V
)  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
8259, 60, 81syl2anc 661 . . 3  |-  ( ph  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  -> 
( ( ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V
)  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
8358, 82mpd 15 . 2  |-  ( ph  ->  ( ( ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V
)  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) )
844, 5, 83mp2and 679 1  |-  ( ph  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    \/ w3o 964    /\ w3a 965    = wceq 1369    e. wcel 1756    =/= wne 2601   A.wral 2710   E.wrex 2711   _Vcvv 2967   ` cfv 5413  (class class class)co 6086   Basecbs 14166   distcds 14239  TarskiG2Dcstrkg2d 22870  Itvcitv 22872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-trkg2d 22890
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator