Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brafs Structured version   Unicode version

Theorem brafs 26996
Description: Binary relationship form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013.)
Hypotheses
Ref Expression
brafs.p  |-  P  =  ( Base `  G
)
brafs.d  |-  .-  =  ( dist `  G )
brafs.i  |-  I  =  (Itv `  G )
brafs.g  |-  ( ph  ->  G  e. TarskiG )
brafs.o  |-  O  =  (AFS `  G )
brafs.1  |-  ( ph  ->  A  e.  P )
brafs.2  |-  ( ph  ->  B  e.  P )
brafs.3  |-  ( ph  ->  C  e.  P )
brafs.4  |-  ( ph  ->  D  e.  P )
brafs.5  |-  ( ph  ->  X  e.  P )
brafs.6  |-  ( ph  ->  Y  e.  P )
brafs.7  |-  ( ph  ->  Z  e.  P )
brafs.8  |-  ( ph  ->  W  e.  P )
Assertion
Ref Expression
brafs  |-  ( ph  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >. O <. <. X ,  Y >. ,  <. Z ,  W >. >. 
<->  ( ( B  e.  ( A I C )  /\  Y  e.  ( X I Z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  Y )  /\  ( B  .-  C )  =  ( Y  .-  Z ) )  /\  ( ( A  .-  D )  =  ( X  .-  W )  /\  ( B  .-  D )  =  ( Y  .-  W ) ) ) ) )

Proof of Theorem brafs
Dummy variables  a 
b  c  d  e  f  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6098 . . . . 5  |-  ( a  =  A  ->  (
a I c )  =  ( A I c ) )
21eleq2d 2510 . . . 4  |-  ( a  =  A  ->  (
b  e.  ( a I c )  <->  b  e.  ( A I c ) ) )
32anbi1d 704 . . 3  |-  ( a  =  A  ->  (
( b  e.  ( a I c )  /\  y  e.  ( x I z ) )  <->  ( b  e.  ( A I c )  /\  y  e.  ( x I z ) ) ) )
4 oveq1 6098 . . . . 5  |-  ( a  =  A  ->  (
a  .-  b )  =  ( A  .-  b ) )
54eqeq1d 2451 . . . 4  |-  ( a  =  A  ->  (
( a  .-  b
)  =  ( x 
.-  y )  <->  ( A  .-  b )  =  ( x  .-  y ) ) )
65anbi1d 704 . . 3  |-  ( a  =  A  ->  (
( ( a  .-  b )  =  ( x  .-  y )  /\  ( b  .-  c )  =  ( y  .-  z ) )  <->  ( ( A 
.-  b )  =  ( x  .-  y
)  /\  ( b  .-  c )  =  ( y  .-  z ) ) ) )
7 oveq1 6098 . . . . 5  |-  ( a  =  A  ->  (
a  .-  d )  =  ( A  .-  d ) )
87eqeq1d 2451 . . . 4  |-  ( a  =  A  ->  (
( a  .-  d
)  =  ( x 
.-  w )  <->  ( A  .-  d )  =  ( x  .-  w ) ) )
98anbi1d 704 . . 3  |-  ( a  =  A  ->  (
( ( a  .-  d )  =  ( x  .-  w )  /\  ( b  .-  d )  =  ( y  .-  w ) )  <->  ( ( A 
.-  d )  =  ( x  .-  w
)  /\  ( b  .-  d )  =  ( y  .-  w ) ) ) )
103, 6, 93anbi123d 1289 . 2  |-  ( a  =  A  ->  (
( ( b  e.  ( a I c )  /\  y  e.  ( x I z ) )  /\  (
( a  .-  b
)  =  ( x 
.-  y )  /\  ( b  .-  c
)  =  ( y 
.-  z ) )  /\  ( ( a 
.-  d )  =  ( x  .-  w
)  /\  ( b  .-  d )  =  ( y  .-  w ) ) )  <->  ( (
b  e.  ( A I c )  /\  y  e.  ( x I z ) )  /\  ( ( A 
.-  b )  =  ( x  .-  y
)  /\  ( b  .-  c )  =  ( y  .-  z ) )  /\  ( ( A  .-  d )  =  ( x  .-  w )  /\  (
b  .-  d )  =  ( y  .-  w ) ) ) ) )
11 eleq1 2503 . . . 4  |-  ( b  =  B  ->  (
b  e.  ( A I c )  <->  B  e.  ( A I c ) ) )
1211anbi1d 704 . . 3  |-  ( b  =  B  ->  (
( b  e.  ( A I c )  /\  y  e.  ( x I z ) )  <->  ( B  e.  ( A I c )  /\  y  e.  ( x I z ) ) ) )
13 oveq2 6099 . . . . 5  |-  ( b  =  B  ->  ( A  .-  b )  =  ( A  .-  B
) )
1413eqeq1d 2451 . . . 4  |-  ( b  =  B  ->  (
( A  .-  b
)  =  ( x 
.-  y )  <->  ( A  .-  B )  =  ( x  .-  y ) ) )
15 oveq1 6098 . . . . 5  |-  ( b  =  B  ->  (
b  .-  c )  =  ( B  .-  c ) )
1615eqeq1d 2451 . . . 4  |-  ( b  =  B  ->  (
( b  .-  c
)  =  ( y 
.-  z )  <->  ( B  .-  c )  =  ( y  .-  z ) ) )
1714, 16anbi12d 710 . . 3  |-  ( b  =  B  ->  (
( ( A  .-  b )  =  ( x  .-  y )  /\  ( b  .-  c )  =  ( y  .-  z ) )  <->  ( ( A 
.-  B )  =  ( x  .-  y
)  /\  ( B  .-  c )  =  ( y  .-  z ) ) ) )
18 oveq1 6098 . . . . 5  |-  ( b  =  B  ->  (
b  .-  d )  =  ( B  .-  d ) )
1918eqeq1d 2451 . . . 4  |-  ( b  =  B  ->  (
( b  .-  d
)  =  ( y 
.-  w )  <->  ( B  .-  d )  =  ( y  .-  w ) ) )
2019anbi2d 703 . . 3  |-  ( b  =  B  ->  (
( ( A  .-  d )  =  ( x  .-  w )  /\  ( b  .-  d )  =  ( y  .-  w ) )  <->  ( ( A 
.-  d )  =  ( x  .-  w
)  /\  ( B  .-  d )  =  ( y  .-  w ) ) ) )
2112, 17, 203anbi123d 1289 . 2  |-  ( b  =  B  ->  (
( ( b  e.  ( A I c )  /\  y  e.  ( x I z ) )  /\  (
( A  .-  b
)  =  ( x 
.-  y )  /\  ( b  .-  c
)  =  ( y 
.-  z ) )  /\  ( ( A 
.-  d )  =  ( x  .-  w
)  /\  ( b  .-  d )  =  ( y  .-  w ) ) )  <->  ( ( B  e.  ( A I c )  /\  y  e.  ( x I z ) )  /\  ( ( A 
.-  B )  =  ( x  .-  y
)  /\  ( B  .-  c )  =  ( y  .-  z ) )  /\  ( ( A  .-  d )  =  ( x  .-  w )  /\  ( B  .-  d )  =  ( y  .-  w
) ) ) ) )
22 oveq2 6099 . . . . 5  |-  ( c  =  C  ->  ( A I c )  =  ( A I C ) )
2322eleq2d 2510 . . . 4  |-  ( c  =  C  ->  ( B  e.  ( A I c )  <->  B  e.  ( A I C ) ) )
2423anbi1d 704 . . 3  |-  ( c  =  C  ->  (
( B  e.  ( A I c )  /\  y  e.  ( x I z ) )  <->  ( B  e.  ( A I C )  /\  y  e.  ( x I z ) ) ) )
25 oveq2 6099 . . . . 5  |-  ( c  =  C  ->  ( B  .-  c )  =  ( B  .-  C
) )
2625eqeq1d 2451 . . . 4  |-  ( c  =  C  ->  (
( B  .-  c
)  =  ( y 
.-  z )  <->  ( B  .-  C )  =  ( y  .-  z ) ) )
2726anbi2d 703 . . 3  |-  ( c  =  C  ->  (
( ( A  .-  B )  =  ( x  .-  y )  /\  ( B  .-  c )  =  ( y  .-  z ) )  <->  ( ( A 
.-  B )  =  ( x  .-  y
)  /\  ( B  .-  C )  =  ( y  .-  z ) ) ) )
2824, 273anbi12d 1290 . 2  |-  ( c  =  C  ->  (
( ( B  e.  ( A I c )  /\  y  e.  ( x I z ) )  /\  (
( A  .-  B
)  =  ( x 
.-  y )  /\  ( B  .-  c )  =  ( y  .-  z ) )  /\  ( ( A  .-  d )  =  ( x  .-  w )  /\  ( B  .-  d )  =  ( y  .-  w ) ) )  <->  ( ( B  e.  ( A I C )  /\  y  e.  ( x I z ) )  /\  (
( A  .-  B
)  =  ( x 
.-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  /\  ( ( A  .-  d )  =  ( x  .-  w )  /\  ( B  .-  d )  =  ( y  .-  w ) ) ) ) )
29 oveq2 6099 . . . . 5  |-  ( d  =  D  ->  ( A  .-  d )  =  ( A  .-  D
) )
3029eqeq1d 2451 . . . 4  |-  ( d  =  D  ->  (
( A  .-  d
)  =  ( x 
.-  w )  <->  ( A  .-  D )  =  ( x  .-  w ) ) )
31 oveq2 6099 . . . . 5  |-  ( d  =  D  ->  ( B  .-  d )  =  ( B  .-  D
) )
3231eqeq1d 2451 . . . 4  |-  ( d  =  D  ->  (
( B  .-  d
)  =  ( y 
.-  w )  <->  ( B  .-  D )  =  ( y  .-  w ) ) )
3330, 32anbi12d 710 . . 3  |-  ( d  =  D  ->  (
( ( A  .-  d )  =  ( x  .-  w )  /\  ( B  .-  d )  =  ( y  .-  w ) )  <->  ( ( A 
.-  D )  =  ( x  .-  w
)  /\  ( B  .-  D )  =  ( y  .-  w ) ) ) )
34333anbi3d 1295 . 2  |-  ( d  =  D  ->  (
( ( B  e.  ( A I C )  /\  y  e.  ( x I z ) )  /\  (
( A  .-  B
)  =  ( x 
.-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  /\  ( ( A  .-  d )  =  ( x  .-  w )  /\  ( B  .-  d )  =  ( y  .-  w ) ) )  <->  ( ( B  e.  ( A I C )  /\  y  e.  ( x I z ) )  /\  (
( A  .-  B
)  =  ( x 
.-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  /\  ( ( A  .-  D )  =  ( x  .-  w )  /\  ( B  .-  D )  =  ( y  .-  w ) ) ) ) )
35 oveq1 6098 . . . . 5  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
3635eleq2d 2510 . . . 4  |-  ( x  =  X  ->  (
y  e.  ( x I z )  <->  y  e.  ( X I z ) ) )
3736anbi2d 703 . . 3  |-  ( x  =  X  ->  (
( B  e.  ( A I C )  /\  y  e.  ( x I z ) )  <->  ( B  e.  ( A I C )  /\  y  e.  ( X I z ) ) ) )
38 oveq1 6098 . . . . 5  |-  ( x  =  X  ->  (
x  .-  y )  =  ( X  .-  y ) )
3938eqeq2d 2454 . . . 4  |-  ( x  =  X  ->  (
( A  .-  B
)  =  ( x 
.-  y )  <->  ( A  .-  B )  =  ( X  .-  y ) ) )
4039anbi1d 704 . . 3  |-  ( x  =  X  ->  (
( ( A  .-  B )  =  ( x  .-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  <->  ( ( A 
.-  B )  =  ( X  .-  y
)  /\  ( B  .-  C )  =  ( y  .-  z ) ) ) )
41 oveq1 6098 . . . . 5  |-  ( x  =  X  ->  (
x  .-  w )  =  ( X  .-  w ) )
4241eqeq2d 2454 . . . 4  |-  ( x  =  X  ->  (
( A  .-  D
)  =  ( x 
.-  w )  <->  ( A  .-  D )  =  ( X  .-  w ) ) )
4342anbi1d 704 . . 3  |-  ( x  =  X  ->  (
( ( A  .-  D )  =  ( x  .-  w )  /\  ( B  .-  D )  =  ( y  .-  w ) )  <->  ( ( A 
.-  D )  =  ( X  .-  w
)  /\  ( B  .-  D )  =  ( y  .-  w ) ) ) )
4437, 40, 433anbi123d 1289 . 2  |-  ( x  =  X  ->  (
( ( B  e.  ( A I C )  /\  y  e.  ( x I z ) )  /\  (
( A  .-  B
)  =  ( x 
.-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  /\  ( ( A  .-  D )  =  ( x  .-  w )  /\  ( B  .-  D )  =  ( y  .-  w ) ) )  <->  ( ( B  e.  ( A I C )  /\  y  e.  ( X I z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  /\  ( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( y  .-  w ) ) ) ) )
45 eleq1 2503 . . . 4  |-  ( y  =  Y  ->  (
y  e.  ( X I z )  <->  Y  e.  ( X I z ) ) )
4645anbi2d 703 . . 3  |-  ( y  =  Y  ->  (
( B  e.  ( A I C )  /\  y  e.  ( X I z ) )  <->  ( B  e.  ( A I C )  /\  Y  e.  ( X I z ) ) ) )
47 oveq2 6099 . . . . 5  |-  ( y  =  Y  ->  ( X  .-  y )  =  ( X  .-  Y
) )
4847eqeq2d 2454 . . . 4  |-  ( y  =  Y  ->  (
( A  .-  B
)  =  ( X 
.-  y )  <->  ( A  .-  B )  =  ( X  .-  Y ) ) )
49 oveq1 6098 . . . . 5  |-  ( y  =  Y  ->  (
y  .-  z )  =  ( Y  .-  z ) )
5049eqeq2d 2454 . . . 4  |-  ( y  =  Y  ->  (
( B  .-  C
)  =  ( y 
.-  z )  <->  ( B  .-  C )  =  ( Y  .-  z ) ) )
5148, 50anbi12d 710 . . 3  |-  ( y  =  Y  ->  (
( ( A  .-  B )  =  ( X  .-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  <->  ( ( A 
.-  B )  =  ( X  .-  Y
)  /\  ( B  .-  C )  =  ( Y  .-  z ) ) ) )
52 oveq1 6098 . . . . 5  |-  ( y  =  Y  ->  (
y  .-  w )  =  ( Y  .-  w ) )
5352eqeq2d 2454 . . . 4  |-  ( y  =  Y  ->  (
( B  .-  D
)  =  ( y 
.-  w )  <->  ( B  .-  D )  =  ( Y  .-  w ) ) )
5453anbi2d 703 . . 3  |-  ( y  =  Y  ->  (
( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( y  .-  w ) )  <->  ( ( A 
.-  D )  =  ( X  .-  w
)  /\  ( B  .-  D )  =  ( Y  .-  w ) ) ) )
5546, 51, 543anbi123d 1289 . 2  |-  ( y  =  Y  ->  (
( ( B  e.  ( A I C )  /\  y  e.  ( X I z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  y )  /\  ( B  .-  C )  =  ( y  .-  z ) )  /\  ( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( y  .-  w ) ) )  <->  ( ( B  e.  ( A I C )  /\  Y  e.  ( X I z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  Y )  /\  ( B  .-  C )  =  ( Y  .-  z ) )  /\  ( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( Y  .-  w ) ) ) ) )
56 oveq2 6099 . . . . 5  |-  ( z  =  Z  ->  ( X I z )  =  ( X I Z ) )
5756eleq2d 2510 . . . 4  |-  ( z  =  Z  ->  ( Y  e.  ( X I z )  <->  Y  e.  ( X I Z ) ) )
5857anbi2d 703 . . 3  |-  ( z  =  Z  ->  (
( B  e.  ( A I C )  /\  Y  e.  ( X I z ) )  <->  ( B  e.  ( A I C )  /\  Y  e.  ( X I Z ) ) ) )
59 oveq2 6099 . . . . 5  |-  ( z  =  Z  ->  ( Y  .-  z )  =  ( Y  .-  Z
) )
6059eqeq2d 2454 . . . 4  |-  ( z  =  Z  ->  (
( B  .-  C
)  =  ( Y 
.-  z )  <->  ( B  .-  C )  =  ( Y  .-  Z ) ) )
6160anbi2d 703 . . 3  |-  ( z  =  Z  ->  (
( ( A  .-  B )  =  ( X  .-  Y )  /\  ( B  .-  C )  =  ( Y  .-  z ) )  <->  ( ( A 
.-  B )  =  ( X  .-  Y
)  /\  ( B  .-  C )  =  ( Y  .-  Z ) ) ) )
6258, 613anbi12d 1290 . 2  |-  ( z  =  Z  ->  (
( ( B  e.  ( A I C )  /\  Y  e.  ( X I z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  Y )  /\  ( B  .-  C )  =  ( Y  .-  z ) )  /\  ( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( Y  .-  w ) ) )  <->  ( ( B  e.  ( A I C )  /\  Y  e.  ( X I Z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  Y )  /\  ( B  .-  C )  =  ( Y  .-  Z ) )  /\  ( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( Y  .-  w ) ) ) ) )
63 oveq2 6099 . . . . 5  |-  ( w  =  W  ->  ( X  .-  w )  =  ( X  .-  W
) )
6463eqeq2d 2454 . . . 4  |-  ( w  =  W  ->  (
( A  .-  D
)  =  ( X 
.-  w )  <->  ( A  .-  D )  =  ( X  .-  W ) ) )
65 oveq2 6099 . . . . 5  |-  ( w  =  W  ->  ( Y  .-  w )  =  ( Y  .-  W
) )
6665eqeq2d 2454 . . . 4  |-  ( w  =  W  ->  (
( B  .-  D
)  =  ( Y 
.-  w )  <->  ( B  .-  D )  =  ( Y  .-  W ) ) )
6764, 66anbi12d 710 . . 3  |-  ( w  =  W  ->  (
( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( Y  .-  w ) )  <->  ( ( A 
.-  D )  =  ( X  .-  W
)  /\  ( B  .-  D )  =  ( Y  .-  W ) ) ) )
68673anbi3d 1295 . 2  |-  ( w  =  W  ->  (
( ( B  e.  ( A I C )  /\  Y  e.  ( X I Z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  Y )  /\  ( B  .-  C )  =  ( Y  .-  Z ) )  /\  ( ( A  .-  D )  =  ( X  .-  w )  /\  ( B  .-  D )  =  ( Y  .-  w ) ) )  <->  ( ( B  e.  ( A I C )  /\  Y  e.  ( X I Z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  Y )  /\  ( B  .-  C )  =  ( Y  .-  Z ) )  /\  ( ( A  .-  D )  =  ( X  .-  W )  /\  ( B  .-  D )  =  ( Y  .-  W ) ) ) ) )
69 brafs.o . . 3  |-  O  =  (AFS `  G )
70 brafs.p . . . 4  |-  P  =  ( Base `  G
)
71 brafs.d . . . 4  |-  .-  =  ( dist `  G )
72 brafs.i . . . 4  |-  I  =  (Itv `  G )
73 brafs.g . . . 4  |-  ( ph  ->  G  e. TarskiG )
7470, 71, 72, 73afsval 26995 . . 3  |-  ( ph  ->  (AFS `  G )  =  { <. e ,  f
>.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. x  e.  P  E. y  e.  P  E. z  e.  P  E. w  e.  P  ( e  =  <. <. a ,  b
>. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  e.  ( a I c )  /\  y  e.  ( x I z ) )  /\  ( ( a 
.-  b )  =  ( x  .-  y
)  /\  ( b  .-  c )  =  ( y  .-  z ) )  /\  ( ( a  .-  d )  =  ( x  .-  w )  /\  (
b  .-  d )  =  ( y  .-  w ) ) ) ) } )
7569, 74syl5eq 2487 . 2  |-  ( ph  ->  O  =  { <. e ,  f >.  |  E. a  e.  P  E. b  e.  P  E. c  e.  P  E. d  e.  P  E. x  e.  P  E. y  e.  P  E. z  e.  P  E. w  e.  P  (
e  =  <. <. a ,  b >. ,  <. c ,  d >. >.  /\  f  =  <. <. x ,  y
>. ,  <. z ,  w >. >.  /\  ( (
b  e.  ( a I c )  /\  y  e.  ( x I z ) )  /\  ( ( a 
.-  b )  =  ( x  .-  y
)  /\  ( b  .-  c )  =  ( y  .-  z ) )  /\  ( ( a  .-  d )  =  ( x  .-  w )  /\  (
b  .-  d )  =  ( y  .-  w ) ) ) ) } )
76 brafs.1 . 2  |-  ( ph  ->  A  e.  P )
77 brafs.2 . 2  |-  ( ph  ->  B  e.  P )
78 brafs.3 . 2  |-  ( ph  ->  C  e.  P )
79 brafs.4 . 2  |-  ( ph  ->  D  e.  P )
80 brafs.5 . 2  |-  ( ph  ->  X  e.  P )
81 brafs.6 . 2  |-  ( ph  ->  Y  e.  P )
82 brafs.7 . 2  |-  ( ph  ->  Z  e.  P )
83 brafs.8 . 2  |-  ( ph  ->  W  e.  P )
8410, 21, 28, 34, 44, 55, 62, 68, 75, 76, 77, 78, 79, 80, 81, 82, 83br8d 25942 1  |-  ( ph  ->  ( <. <. A ,  B >. ,  <. C ,  D >. >. O <. <. X ,  Y >. ,  <. Z ,  W >. >. 
<->  ( ( B  e.  ( A I C )  /\  Y  e.  ( X I Z ) )  /\  (
( A  .-  B
)  =  ( X 
.-  Y )  /\  ( B  .-  C )  =  ( Y  .-  Z ) )  /\  ( ( A  .-  D )  =  ( X  .-  W )  /\  ( B  .-  D )  =  ( Y  .-  W ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   E.wrex 2716   <.cop 3883   class class class wbr 4292   {copab 4349   ` cfv 5418  (class class class)co 6091   Basecbs 14174   distcds 14247  TarskiGcstrkg 22889  Itvcitv 22897  AFScafs 26993
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-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-iota 5381  df-fun 5420  df-fv 5426  df-ov 6094  df-afs 26994
This theorem is referenced by:  tg5segofs  26997
  Copyright terms: Public domain W3C validator