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

Theorem 2pthon 25380
Description: A path of length 2 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
Assertion
Ref Expression
2pthon  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/= 
C ) )  -> 
( ( i  =/=  j  /\  ( E `
 i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C }
)  ->  { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( A ( V PathOn  E ) C ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } ) )

Proof of Theorem 2pthon
StepHypRef Expression
1 vex 3059 . . . . . . . . 9  |-  i  e. 
_V
2 vex 3059 . . . . . . . . 9  |-  j  e. 
_V
31, 2pm3.2i 461 . . . . . . . 8  |-  ( i  e.  _V  /\  j  e.  _V )
4 eqid 2461 . . . . . . . 8  |-  { <. 0 ,  i >. , 
<. 1 ,  j
>. }  =  { <. 0 ,  i >. , 
<. 1 ,  j
>. }
5 eqid 2461 . . . . . . . 8  |-  { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. }  =  { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. }
63, 4, 5constr2trl 25377 . . . . . . 7  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V ) )  -> 
( ( i  =/=  j  /\  ( E `
 i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C }
)  ->  { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( V Trails  E ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } ) )
763adant3 1034 . . . . . 6  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/= 
C ) )  -> 
( ( i  =/=  j  /\  ( E `
 i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C }
)  ->  { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( V Trails  E ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } ) )
87imp 435 . . . . 5  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  ->  { <. 0 ,  i
>. ,  <. 1 ,  j >. }  ( V Trails  E ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. } )
9 trliswlk 25317 . . . . 5  |-  ( {
<. 0 ,  i
>. ,  <. 1 ,  j >. }  ( V Trails  E ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. }  ->  { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( V Walks  E ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } )
108, 9syl 17 . . . 4  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  ->  { <. 0 ,  i
>. ,  <. 1 ,  j >. }  ( V Walks 
E ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. } )
11 c0ex 9662 . . . . . . . . 9  |-  0  e.  _V
1211jctl 548 . . . . . . . 8  |-  ( A  e.  V  ->  (
0  e.  _V  /\  A  e.  V )
)
13123ad2ant1 1035 . . . . . . 7  |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  ( 0  e.  _V  /\  A  e.  V ) )
14 0ne1 10704 . . . . . . . 8  |-  0  =/=  1
15 0ne2 10849 . . . . . . . 8  |-  0  =/=  2
1614, 15pm3.2i 461 . . . . . . 7  |-  ( 0  =/=  1  /\  0  =/=  2 )
17 fvtp1g 6137 . . . . . . 7  |-  ( ( ( 0  e.  _V  /\  A  e.  V )  /\  ( 0  =/=  1  /\  0  =/=  2 ) )  -> 
( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  0
)  =  A )
1813, 16, 17sylancl 673 . . . . . 6  |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  ( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  0
)  =  A )
19183ad2ant2 1036 . . . . 5  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/= 
C ) )  -> 
( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  0
)  =  A )
2019adantr 471 . . . 4  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  0
)  =  A )
21 ax-1ne0 9633 . . . . . . . . 9  |-  1  =/=  0
2221nesymi 2692 . . . . . . . 8  |-  -.  0  =  1
2311, 1opth1 4688 . . . . . . . . 9  |-  ( <.
0 ,  i >.  =  <. 1 ,  j
>.  ->  0  =  1 )
2423necon3bi 2661 . . . . . . . 8  |-  ( -.  0  =  1  ->  <. 0 ,  i >.  =/=  <. 1 ,  j
>. )
2522, 24ax-mp 5 . . . . . . 7  |-  <. 0 ,  i >.  =/=  <. 1 ,  j >.
26 opex 4677 . . . . . . . 8  |-  <. 0 ,  i >.  e.  _V
27 opex 4677 . . . . . . . 8  |-  <. 1 ,  j >.  e.  _V
28 hashprg 12603 . . . . . . . 8  |-  ( (
<. 0 ,  i
>.  e.  _V  /\  <. 1 ,  j >.  e. 
_V )  ->  ( <. 0 ,  i >.  =/=  <. 1 ,  j
>. 
<->  ( # `  { <. 0 ,  i >. ,  <. 1 ,  j
>. } )  =  2 ) )
2926, 27, 28mp2an 683 . . . . . . 7  |-  ( <.
0 ,  i >.  =/=  <. 1 ,  j
>. 
<->  ( # `  { <. 0 ,  i >. ,  <. 1 ,  j
>. } )  =  2 )
3025, 29mpbi 213 . . . . . 6  |-  ( # `  { <. 0 ,  i
>. ,  <. 1 ,  j >. } )  =  2
3130fveq2i 5890 . . . . 5  |-  ( {
<. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  ( # `  { <. 0 ,  i
>. ,  <. 1 ,  j >. } ) )  =  ( { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. } `  2 )
32 2z 10997 . . . . . . . . . 10  |-  2  e.  ZZ
3332jctl 548 . . . . . . . . 9  |-  ( C  e.  V  ->  (
2  e.  ZZ  /\  C  e.  V )
)
34333ad2ant3 1037 . . . . . . . 8  |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  ( 2  e.  ZZ  /\  C  e.  V ) )
35 1ne2 10850 . . . . . . . . 9  |-  1  =/=  2
3615, 35pm3.2i 461 . . . . . . . 8  |-  ( 0  =/=  2  /\  1  =/=  2 )
37 fvtp3g 6139 . . . . . . . 8  |-  ( ( ( 2  e.  ZZ  /\  C  e.  V )  /\  ( 0  =/=  2  /\  1  =/=  2 ) )  -> 
( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  2
)  =  C )
3834, 36, 37sylancl 673 . . . . . . 7  |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  ( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  2
)  =  C )
39383ad2ant2 1036 . . . . . 6  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/= 
C ) )  -> 
( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  2
)  =  C )
4039adantr 471 . . . . 5  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  2
)  =  C )
4131, 40syl5eq 2507 . . . 4  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  ( # `
 { <. 0 ,  i >. ,  <. 1 ,  j >. } ) )  =  C )
42 simpl1 1017 . . . . . 6  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( V  e.  X  /\  E  e.  Y
) )
43 prex 4655 . . . . . . . 8  |-  { <. 0 ,  i >. , 
<. 1 ,  j
>. }  e.  _V
44 tpex 6616 . . . . . . . 8  |-  { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. }  e.  _V
4543, 44pm3.2i 461 . . . . . . 7  |-  ( {
<. 0 ,  i
>. ,  <. 1 ,  j >. }  e.  _V  /\ 
{ <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  e.  _V )
4645a1i 11 . . . . . 6  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( { <. 0 ,  i >. ,  <. 1 ,  j >. }  e.  _V  /\  { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. }  e.  _V )
)
47 3simpb 1012 . . . . . . . 8  |-  ( ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  ->  ( A  e.  V  /\  C  e.  V
) )
48473ad2ant2 1036 . . . . . . 7  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/= 
C ) )  -> 
( A  e.  V  /\  C  e.  V
) )
4948adantr 471 . . . . . 6  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( A  e.  V  /\  C  e.  V
) )
5042, 46, 493jca 1194 . . . . 5  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( ( V  e.  X  /\  E  e.  Y )  /\  ( { <. 0 ,  i
>. ,  <. 1 ,  j >. }  e.  _V  /\ 
{ <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  e.  _V )  /\  ( A  e.  V  /\  C  e.  V
) ) )
51 iswlkon 25310 . . . . 5  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( { <. 0 ,  i >. ,  <. 1 ,  j
>. }  e.  _V  /\  {
<. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  e.  _V )  /\  ( A  e.  V  /\  C  e.  V
) )  ->  ( { <. 0 ,  i
>. ,  <. 1 ,  j >. }  ( A ( V WalkOn  E ) C ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. }  <->  ( { <. 0 ,  i >. , 
<. 1 ,  j
>. }  ( V Walks  E
) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  /\  ( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  0 )  =  A  /\  ( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  ( # `  { <. 0 ,  i
>. ,  <. 1 ,  j >. } ) )  =  C ) ) )
5250, 51syl 17 . . . 4  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( A ( V WalkOn  E ) C ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  <->  ( { <. 0 ,  i >. , 
<. 1 ,  j
>. }  ( V Walks  E
) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  /\  ( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  0 )  =  A  /\  ( { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } `  ( # `  { <. 0 ,  i
>. ,  <. 1 ,  j >. } ) )  =  C ) ) )
5310, 20, 41, 52mpbir3and 1197 . . 3  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  ->  { <. 0 ,  i
>. ,  <. 1 ,  j >. }  ( A ( V WalkOn  E ) C ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. } )
543, 4, 5constr2pth 25379 . . . 4  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/= 
C ) )  -> 
( ( i  =/=  j  /\  ( E `
 i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C }
)  ->  { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( V Paths  E ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } ) )
5554imp 435 . . 3  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  ->  { <. 0 ,  i
>. ,  <. 1 ,  j >. }  ( V Paths 
E ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. } )
56 ispthon 25354 . . . 4  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( { <. 0 ,  i >. ,  <. 1 ,  j
>. }  e.  _V  /\  {
<. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  e.  _V )  /\  ( A  e.  V  /\  C  e.  V
) )  ->  ( { <. 0 ,  i
>. ,  <. 1 ,  j >. }  ( A ( V PathOn  E ) C ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. }  <->  ( { <. 0 ,  i >. , 
<. 1 ,  j
>. }  ( A ( V WalkOn  E ) C ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  /\  { <. 0 ,  i >. ,  <. 1 ,  j
>. }  ( V Paths  E
) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } ) ) )
5750, 56syl 17 . . 3  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  -> 
( { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( A ( V PathOn  E ) C ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  <->  ( { <. 0 ,  i >. , 
<. 1 ,  j
>. }  ( A ( V WalkOn  E ) C ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. }  /\  { <. 0 ,  i >. ,  <. 1 ,  j
>. }  ( V Paths  E
) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } ) ) )
5853, 55, 57mpbir2and 938 . 2  |-  ( ( ( ( V  e.  X  /\  E  e.  Y )  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C
) )  /\  (
i  =/=  j  /\  ( E `  i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C } ) )  ->  { <. 0 ,  i
>. ,  <. 1 ,  j >. }  ( A ( V PathOn  E ) C ) { <. 0 ,  A >. , 
<. 1 ,  B >. ,  <. 2 ,  C >. } )
5958ex 440 1  |-  ( ( ( V  e.  X  /\  E  e.  Y
)  /\  ( A  e.  V  /\  B  e.  V  /\  C  e.  V )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/= 
C ) )  -> 
( ( i  =/=  j  /\  ( E `
 i )  =  { A ,  B }  /\  ( E `  j )  =  { B ,  C }
)  ->  { <. 0 ,  i >. ,  <. 1 ,  j >. }  ( A ( V PathOn  E ) C ) { <. 0 ,  A >. ,  <. 1 ,  B >. ,  <. 2 ,  C >. } ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1454    e. wcel 1897    =/= wne 2632   _Vcvv 3056   {cpr 3981   {ctp 3983   <.cop 3985   class class class wbr 4415   ` cfv 5600  (class class class)co 6314   0cc0 9564   1c1 9565   2c2 10686   ZZcz 10965   #chash 12546   Walks cwalk 25274   Trails ctrail 25275   Paths cpath 25276   WalkOn cwlkon 25278   PathOn cpthon 25280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-map 7499  df-pm 7500  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-card 8398  df-cda 8623  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-2 10695  df-n0 10898  df-z 10966  df-uz 11188  df-fz 11813  df-fzo 11946  df-hash 12547  df-word 12696  df-wlk 25284  df-trail 25285  df-pth 25286  df-wlkon 25290  df-pthon 25292
This theorem is referenced by:  2pthoncl  25381
  Copyright terms: Public domain W3C validator