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

Theorem brafs 28377
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 6302 . . . . 5  |-  ( a  =  A  ->  (
a I c )  =  ( A I c ) )
21eleq2d 2537 . . . 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 6302 . . . . 5  |-  ( a  =  A  ->  (
a  .-  b )  =  ( A  .-  b ) )
54eqeq1d 2469 . . . 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 6302 . . . . 5  |-  ( a  =  A  ->  (
a  .-  d )  =  ( A  .-  d ) )
87eqeq1d 2469 . . . 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 1299 . 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 2539 . . . 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 6303 . . . . 5  |-  ( b  =  B  ->  ( A  .-  b )  =  ( A  .-  B
) )
1413eqeq1d 2469 . . . 4  |-  ( b  =  B  ->  (
( A  .-  b
)  =  ( x 
.-  y )  <->  ( A  .-  B )  =  ( x  .-  y ) ) )
15 oveq1 6302 . . . . 5  |-  ( b  =  B  ->  (
b  .-  c )  =  ( B  .-  c ) )
1615eqeq1d 2469 . . . 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 6302 . . . . 5  |-  ( b  =  B  ->  (
b  .-  d )  =  ( B  .-  d ) )
1918eqeq1d 2469 . . . 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 1299 . 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 6303 . . . . 5  |-  ( c  =  C  ->  ( A I c )  =  ( A I C ) )
2322eleq2d 2537 . . . 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 6303 . . . . 5  |-  ( c  =  C  ->  ( B  .-  c )  =  ( B  .-  C
) )
2625eqeq1d 2469 . . . 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 1300 . 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 6303 . . . . 5  |-  ( d  =  D  ->  ( A  .-  d )  =  ( A  .-  D
) )
3029eqeq1d 2469 . . . 4  |-  ( d  =  D  ->  (
( A  .-  d
)  =  ( x 
.-  w )  <->  ( A  .-  D )  =  ( x  .-  w ) ) )
31 oveq2 6303 . . . . 5  |-  ( d  =  D  ->  ( B  .-  d )  =  ( B  .-  D
) )
3231eqeq1d 2469 . . . 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 1305 . 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 6302 . . . . 5  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
3635eleq2d 2537 . . . 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 6302 . . . . 5  |-  ( x  =  X  ->  (
x  .-  y )  =  ( X  .-  y ) )
3938eqeq2d 2481 . . . 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 6302 . . . . 5  |-  ( x  =  X  ->  (
x  .-  w )  =  ( X  .-  w ) )
4241eqeq2d 2481 . . . 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 1299 . 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 2539 . . . 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 6303 . . . . 5  |-  ( y  =  Y  ->  ( X  .-  y )  =  ( X  .-  Y
) )
4847eqeq2d 2481 . . . 4  |-  ( y  =  Y  ->  (
( A  .-  B
)  =  ( X 
.-  y )  <->  ( A  .-  B )  =  ( X  .-  Y ) ) )
49 oveq1 6302 . . . . 5  |-  ( y  =  Y  ->  (
y  .-  z )  =  ( Y  .-  z ) )
5049eqeq2d 2481 . . . 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 6302 . . . . 5  |-  ( y  =  Y  ->  (
y  .-  w )  =  ( Y  .-  w ) )
5352eqeq2d 2481 . . . 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 1299 . 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 6303 . . . . 5  |-  ( z  =  Z  ->  ( X I z )  =  ( X I Z ) )
5756eleq2d 2537 . . . 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 6303 . . . . 5  |-  ( z  =  Z  ->  ( Y  .-  z )  =  ( Y  .-  Z
) )
6059eqeq2d 2481 . . . 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 1300 . 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 6303 . . . . 5  |-  ( w  =  W  ->  ( X  .-  w )  =  ( X  .-  W
) )
6463eqeq2d 2481 . . . 4  |-  ( w  =  W  ->  (
( A  .-  D
)  =  ( X 
.-  w )  <->  ( A  .-  D )  =  ( X  .-  W ) ) )
65 oveq2 6303 . . . . 5  |-  ( w  =  W  ->  ( Y  .-  w )  =  ( Y  .-  W
) )
6665eqeq2d 2481 . . . 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 1305 . 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 28376 . . 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 2520 . 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 27286 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 973    = wceq 1379    e. wcel 1767   E.wrex 2818   <.cop 4039   class class class wbr 4453   {copab 4510   ` cfv 5594  (class class class)co 6295   Basecbs 14507   distcds 14581  TarskiGcstrkg 23691  Itvcitv 23698  AFScafs 28374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-iota 5557  df-fun 5596  df-fv 5602  df-ov 6298  df-afs 28375
This theorem is referenced by:  tg5segofs  28378
  Copyright terms: Public domain W3C validator